Tesla Zhang @ice1000@types.pl
I impwement dependent type theory.
Joined Sep 2021
Tesla Zhang
boosted
@andrejbauer @amy @jonmsterling @ltchen
I was going to say something in a similar direction.
You can imagine a professor in a maths class (no proof assistants) and all students trying to figure out the omitted subscripts in the blackboard.
Except that only the professor knows them, and they are not going to reveal to the students how they resolved them and what they are.
And also it is perfect for publishing maths papers on the basis that they have been formalized: the author of the paper may resolve them in a way that is different from what the proof assistant did, intentionally or unintentionally. And also the readers of the paper.
Tesla Zhang
boosted
@ahfrom @andrejbauer @ltchen The point here is not the specific wording, but rather Andrej’s suggestion that syntactic properties are not emphasized anymore and that everything will become a heuristic. That’s the thing i was arguing against. No need to get caught up in minor details that don’t pertain to the overall point.
HoTT '23 was 🔥🔥🔥🔥🔥🔥🔥🔥🔥🔥🔥🔥🔥
Gradual dependent type is so interesting!
Copower functor
Tesla Zhang
boosted
This is the shortest and most comprehensible overview of dependent types that I've ever read: it's it's like a single screenful: https://agda.readthedocs.io/en/v2.6.3/getting-started/what-is-agda.html
Cooltt is really cool. The more I think about it, the cooler I think it is.
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?
I impwement dependent type theory.
Joined Sep 2021
