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.

Modeling Univalence in Inverse Diagrams | Homotopy Type Theory

Modeling Univalence in Inverse Diagrams

Recommend

A direct proof of Hedberg’s theorem | Homotopy Type Theory

A type theoretical Yoneda lemma | Homotopy Type Theory

Reducing all HIT’s to 1-HIT’s | Homotopy Type Theory

Homotopy equivalences are equivalences: take 3 | Homotopy Type Theory

π₁(S¹) is Z

Running Spheres in Agda, Part I | Homotopy Type Theory

A master thesis on homotopy type theory | Homotopy Type Theory

truncated higher inductive type

Positive h-levels are closed under W | Homotopy Type Theory

All Modalities are HITs | Homotopy Type Theory

About Joyk