I have just posted the following preprint, which presents new set-theoretic models of univalence in categories of simplicial diagrams over inverse categories (or, more generally, diagrams over inverse categories starting from any existing model of univalence).
For completeness, I also included a sketch of how to use a universe object to deal with coherence in the categorical interpretation of type theory, and of the meaning of various basic notions in homotopy type theory under categorical semantics in homotopy theory.
An inverse category is one that contains no infinite composable strings of nonidentity arrows. An equivalent, but better, definition is that the relation “x receives a nonidentity arrow from y” on its objects is well-founded.
This means that we can use well-founded induction to construct diagrams, and morphisms between diagrams, on an inverse category. Homotopy theorists have exploited this to define the Reedy model structure for diagrams indexed on an inverse category in any model category. The Reedy cofibrations and weak equivalences are levelwise, and a diagram is Reedy fibrant if for each , the map from to the limit of the values of on “all objects below ” is a fibration. The Reedy model structure for simplicial sets is a presentation of the -presheaf topos .
For example, if is the arrow category , then a diagram is Reedy fibrant if the following two conditions hold.
- is a fibration (i.e. is fibrant). Here 1 is the limit of the empty diagram (there being no objects below )
- is a fibration. Here is the limit of the corresponding singleton diagram, since 0 is the unique object below .
The central observation which makes this useful for modeling type theory is that
Reedy fibrant diagrams on an inverse category can be identified with certain contexts in type theory.
For instance, in a Reedy fibrant diagram on the arrow category, we have firstly a fibrant object , which represents a type, and then we have a fibration , which represents a type dependent on . Thus the whole diagram can be considered as a context of the form
Similar interpretations are possible for all inverse categories (possibly involving “infinite contexts” if the category is infinite). This view of contexts as diagrams appears in Makkai’s work on “FOLDS”, and seems likely to have occurred to others as well.
Using this observation, we can inductively build a (Reedy fibrant) universe in out of a universe in . For instance, suppose is a fibrant object representing a universe in , and let be the arrow category . Then the universe we obtain in is the fibration that is the universal dependent type. Regarded as a dependent type in context, this fibration is
We can then prove, essentially working only in the internal type theory of , that the objects of classified by this universe are closed under all the type forming operations, and moreover that this universe inherits univalence from the universe we started with in . In particular, starting with Voevodsky’s universal Kan fibration for simplicial sets, we obtain a model of univalence in simplicial diagrams on , hence in the -presheaf topos .
Combining this with my previous idea, we should be able to get models in -toposes of sheaves for any topology on an inverse category. But unfortunately, inverse categories don’t seem likely to support very many interesting topologies.
So far, I haven’t been able to generalize this beyond inverse categories. The Reedy model structure exists whenever is a Reedy category, which is more general than an inverse category. But in the general case, the cofibrations are no longer levelwise, and the dependent products seem to involve equalizers, and I haven’t been able to get a handle on things. A different idea is to use diagrams on inverse categories to “bootstrap” our way up to other models, but I haven’t been able to get anything like that to work yet either.