# Formalizing the graph model of type theory, part 3

In the induction principle for the graph quotient $\mathsf{colim}(\Gamma)$, we have seen that terms of a type family $P : \mathsf{colim}(\Gamma)\to\mathsf{Type}$ are equivalently described by terms of the transposed family $\Delta(P)\circ\eta$ of graphs over $\Gamma$. This family is no ordinary family, and in this post I’d like to discuss its special properties, and what other choices to model the notion of ‘type family’ exist in the graph model.

Let us first explicitly describe the transposed family $\Delta(P)\circ\eta$. First, the family $\Delta(P)$ over $\Delta(\mathsf{colim}(\mathsf{\Gamma}))$ is given on vertices by $\Delta(P)_0:=P$. Then, for an edge $p:x=y$ in $\Delta(\mathsf{colim}(\Gamma))$ and $u:P(x)$ and $v:P(y)$, we have the type $\Delta(P)_1(e,u,v):= (\mathsf{trans}(p,u)=v)$ of edges.

Note that the type $\Sigma_{(v:P(y))}~\Delta(P)_1(e,u,v)$ is contractible. In other words, the relation $\Delta(P)_1(e) : \Delta(P)_0(x) \to{} \Delta(P)_0(y) \to{} U$ is functional. Similarly, since transport over $p:x=y$ is an equivalence, the relation $\Delta(P)_1(e)$ is also functional in the opposite direction, i.e. as a function from $\Delta(P)_0(y)$ to $\Delta(P)_0(y)$.

A relation $R : X \to{} Y\to{} U$ which is functional is the same thing as a function from $X$ to $Y$, and a relation $R:X\to{}Y\to{}U$ which is functional in both directions is the same thing as an equivalence from $X$ to $Y$.

Thus, given a family $A$ of graphs over $\Gamma$, we can ask whether each of the relations $A_1(e) : A_0(i) \to{} A_0(j) \to{}U$ is either (i) functional, or (ii) functional in the opposite direction, or (iii) functional in both directions. These conditions on a family of graphs $A$ over $\Gamma$ are conditions of cartesianness, for they are (respectively) equivalent to (i) the left square being a pullback, (ii) the right square being a pullback, or (iii) both squares being pullback, in the following diagram

We see that we get four notions of type dependency on a graph. We have the original notion of a dependent graph, and by putting conditions of cartesianness in play we get three more:

(i) Diagrams. A (covariant) diagram $D$ over a graph $\Gamma$ consists of a type family $D_0 : \Gamma_0\to{}U$, and an indexed family of functions $D_1 : \Pi_{(i,j:\Gamma_0)}\Pi_{(e:\Gamma_1(i,j))}~D_0(i)\to D_0(j)$. A term $x$ of a diagram $D$ over $\Gamma$ consists of a section $x_0 : \Pi_{(i:\Gamma_0)}~D_0(i)$, in which is compatible with the edges by $x_1 : \Pi_{(i,j:\Gamma_0)}\Pi_{(e:\Gamma_1(i,j))}~D_1(e,x_0(i))={}x_0(j)$. Note that the type of all terms of a diagram $D$ can be given the structure of a cone on $D$, and indeed this is the limiting cone for $D$, as we saw in my earlier post about coinductive types.

(ii) Contravariant Diagrams. A contravariant diagram $D$ over a graph $\Gamma$ consists of a type family $D_0 : \Gamma_0\to{}U$, and an indexed family of functions $D_1 : \Pi_{(i,j:\Gamma_0)}\Pi_{(e:\Gamma_1(i,j))}~D_0(j)\to D_0(i)$. A term $x$ of a contravariant diagram $D$ over $\Gamma$ consists of a section $x_0 : \Pi_{(i:\Gamma_0)}~D_0(i)$, in which is compatible with the edges by $x_1 : \Pi_{(i,j:\Gamma_0)}\Pi_{(e:\Gamma_1(i,j))} D_1(e,x_0(j))=x_0(i)$.

(iii) Equifibered Families. An equifibered family $E$ over a graph $\Gamma$ consists of a type family $E_0:\Gamma_0\to{}U$, and an indexed family of equivalences $E_1 : \Pi_{(i,j:\Gamma_0)}\Pi_{(e:\Gamma_1(i,j))}~E_0(i)\simeq{}E_0(j)$. A term $x$ of an equifibered family $E$ over $\Gamma$ consists of a section $x_0 : \Pi_{(i:\Gamma_0)}~E_0(i)$, in which is compatible with the edges by $x_1 : \Pi_{(i,j:\Gamma_0)}\Pi_{(e:\Gamma_1(i,j))} E_1(e,x_0(i))=x_0(j)$.

Using these varying notions of families, we can nicely detect the variances of the different type operations. For instance, if $D$ is a contravariant diagram over $\Gamma$, and $E$ is a (covariant) diagram over $\Gamma.D$, then $\Pi(D,E)$ is again a (covariant) diagram over $\Gamma$. If $D$ was contravariant and $E$ covariant, then $\Pi(D,E)$ would be contravariant. Similarly for the W-graphs. If $D$ is contravariant and $E$ is covariant, then $W(D,E)$ is contravariant, while if $D$ is covariant and $E$ contravariant, then $W(D,E)$ is covariant. When you try to take $\Pi(D,E)$ where both $D$ and $E$ are covariant, you still get a family of graphs, but it will be a general one.

On the other hand, the model in which the families are the equifibered families is a full model of type theory with dependent function types and W-types. Moreover, an equifibered family over a graph $\Gamma$ prescribes precisely the descent data that is needed to get a type family over $\mathsf{colim}(\Gamma)$. Indeed, the descent theorem states that the type of [type families over $\mathsf{colim}(\Gamma)$] is equivalent to the type of [equifibered families over $\Gamma$]. Even more: the descent theorem can be extended to a ‘slice-wise’ equivalence between models. In other words, locally the univalent universe is as a model of type theory precisely the same thing as the graph model with equifibered families.

We see that, even if we attempt to formalize just several aspects of the graph model of type theory in order to study higher inductive types, we run into various different models with varying amounts of structure beyond type dependency. The situation really calls for us to also formalize an abstract notion of model in homotopy type theory of which all the models we have encountered so far, including the univalent universe, are instances. This should be useful even if we cannot find a completely satisfactory notion of model (because it might be lacking higher coherences), just because it will force us to be formal about what we mean by having implemented a model of type theory as a structure of unrestricted truncation level.

Previous posts about formalizing the graph model:
Formalizing the graph model of type theory, part 1
Formalizing the graph model of type theory, part 2