Thus, the term asserting the univalence axiom corresponds to a certain morphism in an elementary topos with object classifiers. The point is, I guess, that such a morphism exists only in the degenerate topos, i.e. the one equivalent to the single object-single morphism category. Only in higher toposes/categories can non-degenerate examples of the univalence axiom be found.
It should also be noted that you can already identify isomorphic objects ("types") of 1-categories without much harm. Formally, if you have a contractible groupoid G contained in a category C, then the quotient map C -> C/G that collapses all objects of G onto a single object and all morphisms in G onto the identity at that object is an equivalence of categories. This works in particular if G is given by an isomorphism of distinct objects.
It still boggles my mind why type theorists think that "function extensionality" and quotients, two entirely 1-categorical concepts, are best treated using homotopy coherent diagrams. And it is unclear since when proving theorems in less generality (because additional axioms are assumed) is considered progress.
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.
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.
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.
> It still boggles my mind why type theorists think that "function extensionality" and quotients, two entirely 1-categorical concepts, are best treated using homotopy coherent diagrams. And it is unclear since when proving theorems in less generality (because additional axioms are assumed) is considered progress.
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.
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.
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.
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.
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.
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.
By design, the answer is no. Toposes are models of intuitionistic bounded ZF. However, in general dependent type theories, including observational type theory, don't have (and don't want!) the powerset axiom.
There has been some recentish work on predicative analogues of toposes, but I'm not sure anything really definitive has emerged. However, I'm not super familiar with this area.
> To me, it still doesn't answer why TT is the most convenient axiomatization though. The internal language. [...] Especially because TT was arrived at from the IMO wrong angle, namely by coming up with a syntax first and its meaning second.
This is a very common misconception about what is going on when doing type theory.
From the point of view of a category theorist, the way to understand type theory is that it is a methodology for giving explicit presentations of free structures, in such a way that the morphisms make no explicit reference to composition.
The basic method of categorical logic is to compute a result in a syntax corresponding to a free structure, and then sending it to whichever non-free structure you like by the universal property of that structure. Most people initially find this a bizarre thing to do, since intuitively it seems like any proof that works in a free structure should work in any structure.
Indeed, this is actually true, if we only use the free gadget's universal property. However, if we have a type-theoretic presentation of a free structure, we actually have more information than the universal property: we know properties of the syntax! So we can exploit these properties of the syntax to establish facts which hold everywhere, by means of proofs that wouldn't work in an arbitrary structure.
For example, this is why type theorists devote so much effort on properties like cut-elimination: it ensures the composition of morphisms is automatically unital and associative.
Mike Shulman has written a fantastic set of notes, "Categorical Logic from a Categorical Point of View", which is one of the best explanation of type theory for "normal" mathematicians I've seen.
Why wouldn't you want the powerset axiom? Which categories do you have in mind which are, for example, locally cartesian closed and finitely cocomplete but do not have subobject classifiers? (Apart from the initial such category.) Honestly curious here, I can't come up with one.
> From the point of view of a category theorist, the way to understand type theory is that it is a methodology for giving explicit presentations of free structures, in such a way that the morphisms make no explicit reference to composition.
The basic method of categorical logic is to compute a result in a syntax corresponding to a free structure, and then sending it to whichever non-free structure you like by the universal property of that structure. Most people initially find this a bizarre thing to do, since intuitively it seems like any proof that works in a free structure should work in any structure.
I don't find it bizarre at all, but I think this view point is not mainstream in the community. I was certainly looked at weirdly when I asked whether, for example, the "interpretation theorem" is essentially the initiality property of the syntactic model of type theory. Well, good to know that at least some people seem to have come to their senses.
I don't understand what properties about categories can be proved from properties of the syntax, e.g. canonicity. Take cartesian closed categories with natural numbers object. I can see that you can prove, for example, that 0 + n = n holds in every such category by verifying the equality in the simply typed lambda calculus. But what does canonicity tell me about these categories?
Shulman writes (p. 12 of the notes you've linked to) that it's worth knowing about canonicity and other logical properties so that one can talk with type theorists about them. That suggests to me that it really isn't worth knowing about. The question why type theory is the "best" presentation of initial XY-categories remains open. It's basically impossible to construct the terms in raw type theory needed for non-trivial proofs by hand. All proof assistants I know of still use some kind of elaboration so that you can emit some parameters of operations, and most are based on tactics. Why can't we simply use these mechanisms for the tautological presentation of initial XY-categories?
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.