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

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

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 impwement dependent type theory.

Joined Sep 2021