re: shop talk 

which pretentious asshole wrote this concluding sentence

(it was this pretentious asshole)

Show thread

re: shop talk 

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

Show thread

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

Show thread

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)

LaTeX 

\newcommand{\opcitt}[1]{\defcitealias{#1}{\emph{op. cit.}}\citetalias{#1}\xspace}
\newcommand{\opcitp}[1]{\defcitealias{#1}{\emph{op. cit.}}\citepalias{#1}\xspace}

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

Show thread
Show older
types.pl

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