pray that this button remains unpressed

re: shop talk

which pretentious asshole wrote this concluding sentence

I know I just went off about inference lmao but 👀
(from pit-claudel.fr/clement/prospec)

Look how beautiful this is

I'm collecting awful and terrible words

no!! stop!!

re: shop talk

I'm tempted to say that "cofixpoints corecursively coconsume a coinductive" lmao

a n g e r y 😡

re: paths and stuff

I think something like this
If f transported across p is equal to g, then if you have an (A x), you can apply f first then transport across p, or you can transport across p then apply g, and they'll be equal
In any case, applying f and g yields equal things

hey that's a recursive type

pulling out the receipts about syntactic guard checking to make sure everyone knows they said the thing, it wasn't me
(it is also me)

someone's Agda file isn't encoded right

LaTeX


Just did a good thing
I don't regret this thing at all

Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.