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.

Being the 100th stargazer of TypOS

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

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

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

Calling intLoop

Commutative (+) is hot!

Definitional equality that does not satisfy transitivity

Aye.

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