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.
This is very nice work, Mike!
One thing we can do with presheaf models in (1-) topos theory is violate (or satisfy) logical conditions that hold (or fail) in constant models, like, most simply, excluded middle or the axiom of choice. I wonder if we can do the same sort of thing with these models? But what sort of logical conditions should we consider? Maybe excluded middle for hProps?
Thanks! Yes, that’s a good thing to think about. Excluded middle for hProps was the first thing that came to my mind as well. That must be violated already in the Sierpinski topos, yes? And I guess with the inverse category we can violate De Morgan’s law too (I’m looking at D4.6.3 in Sketches of an Elephant) — it seems that for violating logical principles that talk only about hProps we should be able to use the same sorts of examples we use in 1-topos theory. But the restriction to inverse categories (or even sheaves on them) seems fairly limiting.
So, I’m looking at Fabio Bellissima’s description of the free Heyting algebra on n generators (Finitely generated free Heyting algebras, J. Symbolic Logic 51 (1986), no. 1, 152–165) , which proceeds by embedding it in a co-well-founded Kripke model. A co-well-founded Kripke model is precisely the propositional logic of diagrams on an inverse poset. That seems to imply that with diagrams on inverse categories, we can violate any finitary propositional formula that is not an intuitionistic tautology.
By the way, the (oo,1)-Sierpinski topos is also a very simple but maybe instructive example of a non-trivial cohesive (oo,1)-topos ( we had long had a remark on that here http://ncatlab.org/nlab/show/cohesive+topos#FamiliesOfSets ). So I suppose you have constructed the first non-trivial univalent model for cohesive homotopy type theory.
A nice point, thanks!