Tesla Zhang @ice1000@types.pl

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?

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....

https://mathstodon.xyz/@MartinEscardo/109480609080455395

Calling `intLoop`

Commutative (+) is hot!

Definitional equality that does not satisfy transitivity

I'm https://twitter.com/OwoTizusa

Aye.