In my recent post at the n-Category Café, I described a notion of “higher modality” in type theory, which semantically ought to represent a left-exact-reflective sub--category of an -topos — once we can prove that homotopy type theory has models in -toposes. I’ve since realized that this theory may also be useful in proving that latter fact itself. For if we have a set-theoretic model which contains such a modality , then we ought to be able to show that the resulting left-exact-reflective subcategory of the model also supports such a model. If this works, it should simplify the search for models of univalence in -toposes, since any -topos is a left-exact localization of an -category of presheaves, and the latter can be presented by model categories that are easier to understand concretely.

Moreover, given a suitable inductive definition of type theory inside of type theory, we ought to be able to carry through the following argument purely internally as well. Steve Awodey has pointed out that this can be regarded as a stability theorem for a putative notion of “elementary -topos” under passage to lex-reflective subcategories.

Here’s how I think the argument should go. First of all, even though a “reflective subcategory” axiomatized in this way is only reflective in the -sense, not in the 1-categorical sense, we can still prove that it is closed under type-theoretic operations including identity types, dependent sums, and dependent products. Thus, if we simply restrict the original model by allowing only objects of the subcategory to interpret types, we will still have all this categorical structure. The subcategory will not, in general, be closed under formation of (higher) inductive types, but I would expect that we can obtain “inductive” types with the right universal property in the subcategory by just applying the reflector to the inductive types constructed in the original category. I think this ought to work as long as the eliminator for satisfies its computation rules definitionally (otherwise the reflected inductive types may only satisfy their computation rules propositionally).

Now, with all this structure in place, Voevodsky’s argument shows that all we need in order to obtain a model of type theory in the subcategory is to find a universe there — meaning a fibration of which every other “small” fibration is a pullback (where “small” denotes some class of fibrations which is closed under all the relevant category-theoretic operations). We then intepret types not by objects but by “names” for objects (i.e. maps into the universe). By performing all the categorical operations (such as dependent product, sums, identity types, etc.) once in the universal case, we can represent them by maps acting on the universe; then their action on names is just given by composition, which satisfies strict substitution. Finally, if the universe is univalent, then our type theory will model the univalence axiom. (Perhaps we’ll need to find a hierarchy of universes, but in practice if we can find one universe we should be able to find plenty.)

Now, working internally and assuming a left-exact-reflective subcategory, there is an obvious candidate for such a universe: namely the type

Rsctype := { A : Type & in_rsc A }.

This is the “subtype” of the original universe Type containing those types that lie in the subcategory. Note that this is different from the universe that played a role in the other post. The latter is the universe of original types viewed from the subcategory; while Rsctype is the universe of “types in the subcategory”, but does not obviously lie in the subcategory itself.

However, it turns out that it does. The easiest way I found to prove this was to use the stable factorization system (E,M), and the characterization that a type lies in the subcategory just when it is orthogonal to all the E-maps. Since Rsctype classifies fibrations whose fibers all lie in the subcategory (that is, M-fibrations), this orthogonality would mean that if is an E-map, then any M-fibration is the pullback of some M-fibration over B. We can prove this by (E,M)-factoring and using known facts about how E behaves with respect to fibrations; the full proof is at the end of this file. As expected, it requires the full structure of a lex-reflective subcategory (a stable factorization system isn’t sufficient).

Now, in general Rsctype classifies M-fibrations, but all maps in the subcategory are M-maps. Thus, when Rsctype is regarded as an object of the subcategory, it classifies all fibrations there (or, rather, all those that are small relative to the universe Type in the original model). Moreover, since in_rsc is an h-proposition, the identity types of Rsctype are the same as those of Type; thus Rsctype is also univalent.

Of course, all this is really just a homotopical/higher-categorical version of the fact that if j is a Lawvere-Tierney topology on a 1-topos, then the classifier of closed subobjects is itself a j-sheaf, and hence a subobject classifier for the category of j-sheaves.

Then there is the question of finding left-exact reflective subcategories, especially ones whose reflector has a definitional computation rule. But that’s a subject for another post.