[EtDybNuvCu]

This makes me feel much better. While I think that MLTT and HoTT are valid lines of maths inquiry on their own, for their own merits, I'm not sure what's gained over the topos-based view of foundations.

In particular, the article claims that the Curry-Howard-Lambek correspondence can be used to recover logical sentences from MLTT sentences. Then surely MLTT universes each form a topos of some sort? I suppose that a few hours on nCat would clear this up for me.

[mbid]

EDIT: What follows is true for extensional MLTT. If you add univalence to intensional MLTT, all of this goes out the window. It is conjectured that you can replace "locally cartesian closed category" with "locally cartesian closed infinity categeory" and similarly for toposes and everything will work out.

It can be proved that every topos is locally cartesian closed, and that models of MLTT are precisely the locally cartesian closed categories. The syntactical model of MLTT, i.e. the model built from well-formed types and terms, is the initial model of MLTT, and hence also the initial locally cartesian closed category. The unique functor induced by initiality assigns each valid term in MLTT a morphism in some given locally cartesian categor, which can be seen as recovering intuitionistic proofs from MLTT because toposes are locally cartesian closed.

It is not true that MLTT universes are always toposes though. They are not always cocomplete and need not have a subobject classifier. A consequence is that MLTT does not have proper existential quantifiers (despite what the article claims) because Σ_(x : A) B(x) carries proofs of B(x) along with elements x. It is thus not true that Σ_(x : A) B(x) is a subset of A, which one would expect from existential quantification.

MLTT corresponds to a weaker logic than the more usual intuitionistic one: Sequents in the former make sense in the latter, but not necessarily conversely.

Oh, and maybe there is a slight misconception in your last paragraph: Universes in MLTT are not the same thing as models of MLTT. Models of MLTT are something you talk about from externally of MLTT, from a metatheoretical viewpoint. The universes in the HoTT sense are internal to the logic.

[pacala]

Dilettante here: What's interesting about *TT is that people have built mechanical theorem checkers [Coq, Agda, Lean, ...], and people are working on building automated theorem provers based on those programatic foundations.

[EtDybNuvCu]

Check out Metamath; we can do this for any serious foundations: http://us.metamath.org/downloads/metamath.pdf

[pacala]

Have somebody done it for the more general foundations based on category theory? If I understand correctly, Metamath is a set of tools enabling such a formulation, but not the formulation itself. See ML vs. theorem prover implemented in ML.

[mbid]

There are some developments, for example "Globular": https://arxiv.org/abs/1612.01093

I don't think there is a proof assistant that's really based on categorical foundations. I'd love to see something like that though.