> > Universes in type theory correspond to inaccessible cardinals/Grothendieck universes in ZFC or object classifiers in elementary toposes, at least informally (I doubt there is published work here).

There is quite a bit of published work. For the connection between CZF and type theory (choice and excluded middle are orthogonal on both sides) see Benjamin Werner "Sets in types, types in sets" and Bruno Barras' (still unpublished but available) habilitation thesis. There is more work here, but the equivalence between universes in type theory and universes in set theory should be clear from these references.

Maybe I've read "Sets in types, types in sets" wrong, but there seems to be no equivalence result in there, in the sense that "the category of models of type theory with universes is equivalent to the category of toposes with object classifiers and logical functors". Rather, it says that the metatheory of ZFC can be encoded in Coq, and conversely. The two are different. For example, it makes sense to talk about "internal topos objects" in every finitely complete category, because one can axiomatize the operations and their equations in partial horn logic/essentially algebraic theory/cartesian theories/whatever. But not every finitely complete category is a topos.

> As for the "equivalence" between object classifiers in Topoi and universes in type theory, which definition of object classifier are you referring to? There is a notion of universe in a (pre-)sheaf topos and indeed such universes can model universes in type theory. See the work by Hofmann, Streicher, and many others.

I'm referring to the definition given in Streicher's work, "Universes in toposes", in the "generic" sense, i.e. isomorphic morphisms need not have the same "code" morphism.

> On the other hand, the "internal" definition of an object classifier in a topos is a higher-categorical concept. The statement that a universe is an object classifier is equivalent to the statement that a universe is univalent in type theory.

Yes, universes in ordinary toposes are usually only "generic", not classifying. And never classifying in the very strong sense defined in some of Joyal's notes. (There, not only the lower horizontal morphism in a "decoding" pullback square is unique, but also the upper one.)

> To be clear, one can treat 1-categorical extensionality principles in an extensional type theory, see for example observational type theory which has functional and propositional extensionality as well as quotient types without compromising the computational character of type theory.

Haven't heard about observational type theory before, thanks. Unfortunately, "Towards Observational Type theory" bombards me with a huge amount of syntax, and I've ploughed through enough of these papers only to find that there is nothing behind it at all, so I'm going not going to read this. Are models of observational type theory exactly elementary toposes?

Also, I distinctly remember reading in some of a respected researcher's slides somewhere that Voevodsky has supposedly found the right formulation for function extensionality in the univalence axiom. This sounds completely insane to me.

> As for your question, think of it like this: You can easily treat 1-categorical concepts within an infinity-topos, but the other way around is very complicated and involves quite some encoding overhead. If you are in homotopy type theory you can model ordinary extensional type theory (with some caveats about the universes) by restricting yourself to working with sets. The other way around is, again, just as crazy as in set theory.

Say I want to program a computer (we're on HN after all), and would like do that via some kind of intuitionistic proof assistant. I use one based on HoTT, and want to use quotients. Quotients are constructively (in the sense of computationally) OK because they exist in the effective topos, which is a topos after all. In HoTT, I need to use higher inductive types to construct these and the univalence axiom to do anything useful with them. But the effective topos doesn't validate the univalence axiom, it is a 1-topos after all. How is this practical?

I realize there is work on the "cubical model", which looks a little like an effective infinity topos (or the internal infinity topos of spaces in 1-topos, in particular in the effective topos). But why on earth would I want to deal with the complexity that is homotopy coherent diagrams when all I want is a quotient?

I'd like to have a rough idea what's going on in the tools I'm using. If I want to use a quotient, I don't want to have to also read up about the indicdental complexity of homotopy coherent diagrams. "Just treat it as a black box" is unacceptable to me, and I'm sure many others. I want the tools I'm using to be as complex as necessary, no further, and I'd like to have a rough idea about what's going on so I'm not completely screwed if things break.

> And progress in type theory and logic is not about proving things with less assumptions - you may have been thinking of reverse mathematics. Homotopy type theory is considered progress since it fully explains the behavior of intentional identity types, which already existed in traditional Martin-Löf type theory.

No, HoTT doesn't explain anything, it asserts an axiom. An "explanation" for the identity type would be to relate them to other developments, for example proving that models of intensional type theory (+ function extensionality) are precisely locally cartesian closed infinity categories. And that this equivalence restricts to one of TT with univalence and elementary infinity toposes.

To me, it still doesn't answer why TT is the most convenient axiomatization though. The internal language. This is of course not a formal statement, but things like "1 + n" and "n + 1" not behaving the same although they are equal (homotopic, whatever) makes me very pessimistic that this is true. Especially because TT was arrived at from the IMO wrong angle, namely by coming up with a syntax first and its meaning second.