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

20161013_1

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

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s