> Are models of observational type theory exactly elementary toposes?
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.
>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.
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?
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.
https://mikeshulman.github.io/catlog/catlog.pdf