Modeling Univalence in Inverse Diagrams

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).

The univalence axiom for inverse diagrams.

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 $\to\;\to\;\to\;\cdots$ 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 $A\colon I\to C$ is Reedy fibrant if for each $x\in I$ , the map from $A_x$ to the limit of the values of $A$ on “all objects below $x$ ” is a fibration. The Reedy model structure for $C=$ simplicial sets is a presentation of the $(\infty,1)$ -presheaf topos $(\infty Gpd)^I$ .

For example, if $I$ is the arrow category $(1\to 0)$ , then a diagram $A_1 \to A_0$ is Reedy fibrant if the following two conditions hold.

$A_0\to 1$ is a fibration (i.e. $A_0$ is fibrant). Here 1 is the limit of the empty diagram (there being no objects below $0\in I$ )
$A_1 \to A_0$ is a fibration. Here $A_0$ is the limit of the corresponding singleton diagram, since 0 is the unique object below $1\in I$ .

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 $A_0$ , which represents a type, and then we have a fibration $A_1 \to A_0$ , which represents a type dependent on $A_0$ . Thus the whole diagram can be considered as a context of the form

$a_0\colon A_0 ,\; a_1\colon A_1(a_0)$

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 $C^I$ out of a universe in $C$ . For instance, suppose $U$ is a fibrant object representing a universe in $C$ , and let $I$ be the arrow category $(1\to 0)$ . Then the universe we obtain in $C^I$ is the fibration $U^{(1)} \to U$ that is the universal dependent type. Regarded as a dependent type in context, this fibration is

$A\colon \mathrm{Type} \;\vdash\; (A \to \mathrm{Type}) \colon \mathrm{Type}_1$

We can then prove, essentially working only in the internal type theory of $C$ , that the objects of $C^I$ 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 $C$ . In particular, starting with Voevodsky’s universal Kan fibration for $C=$ simplicial sets, we obtain a model of univalence in simplicial diagrams on $I$ , hence in the $(\infty,1)$ -presheaf topos $(\infty Gpd)^I$ .

Combining this with my previous idea, we should be able to get models in $(\infty,1)$ -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 $I$ 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.

5 Responses to Modeling Univalence in Inverse Diagrams

Steve Awodey says:

15 March 2012 at 22:02

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?

- Mike Shulman says:
  
  16 March 2012 at 00:51
  
  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 $(\cdot \leftarrow \cdot \rightarrow \cdot )$ 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.
  
- Mike Shulman says:
  
  17 March 2012 at 14:09
  
  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.
  
Urs Schreiber says:

16 March 2012 at 03:23

Nice!

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.

- Mike Shulman says:
  
  16 March 2012 at 03:36
  
  A nice point, thanks!