With the presence of ChatGPT, I find short but informative (hence more direct but less polite) emails more sincere.

I have installed a Rust tool to install updates of other Rust tools by downloading binaries instead compiling from source. Now I'm compiling the updater from source from time to time, while seeing no other tool being updated.

I'm reading Bart Jacobs. They have defined "CT-structures" to be a pair (B, T) where B is a category and T is a subset of Ob(B). A morphism between CT-structures (B, T) and (A, S) is basically a functor K: B → A such that X∈T implies K(X) ∈ S.

Is this definition used by anyone else? I think it makes sense (as a motivation of display map categories) but I don't see people using it.

I'm reading Bart Jacobs. Should I follow the proofs?

If one cannot Ford it then one probably shouldn't be able to define it as well?

Show thread

Today I tried to Ford the very dependent type in Agda and guess what

I'm getting a termination check error....

Definitional equality that does not satisfy transitivity


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