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

@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!

Joey's typesetting is really messed up on arXiv 😂

Okay so the language indicator is essentially nonsensical lol

This is the shortest and most comprehensible overview of dependent types that I've ever read: it's it's like a single screenful: agda.readthedocs.io/en/v2.6.3/

Cooltt is really cool. The more I think about it, the cooler I think it is.

How the heck am I supposed to understand a diagram like this

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
Show older
types.pl

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