pounce @pounce@types.pl

oops i need category theory

im done trying to get this mathlib commit to build on my laptop with 16gb of ram
i'll just let it build on a GH runner instead

how did the last i happen

i need to learn how to read mathematical french
i

i should just unsubscribe from the haskell café mailing list, i literally just throw all of the emails into the bin

one of these days imma write a cubical type checker for lean just you wait
and then nobody can tell me to use agda

to tired to keep filling proof holes
bed time

ok time to try to formalize the sheaf of relative kähler differentials in ​

oh shit why did nobody ever tell me the □ modality can be used to represent local properties in the internal language of a sheaf topos that's poggers

lets see if i can learn topos theory in one day ​

wayland stop putting all of your protocol extensions in xdg-desktop-portal challenge

pounce's new term for algebraic geometry: "sheaf math"*

*also applies to: algebraic topology, differential geometry, category theory.....

dang now im wishing i were doing sheaf math in cubical agda instead of lean