In the induction principle for the graph quotient , we have seen that terms of a type family are equivalently described by terms of the transposed family of graphs over . 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 . First, the family over is given on vertices by . Then, for an edge in and and , we have the type of edges.
Note that the type is contractible. In other words, the relation is functional. Similarly, since transport over is an equivalence, the relation is also functional in the opposite direction, i.e. as a function from to .
A relation which is functional is the same thing as a function from to , and a relation which is functional in both directions is the same thing as an equivalence from to .
Thus, given a family of graphs over , we can ask whether each of the relations is either (i) functional, or (ii) functional in the opposite direction, or (iii) functional in both directions. These conditions on a family of graphs over 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 over a graph consists of a type family , and an indexed family of functions . A term of a diagram over consists of a section , in which is compatible with the edges by . Note that the type of all terms of a diagram can be given the structure of a cone on , and indeed this is the limiting cone for , as we saw in my earlier post about coinductive types.
(ii) Contravariant Diagrams. A contravariant diagram over a graph consists of a type family , and an indexed family of functions . A term of a contravariant diagram over consists of a section , in which is compatible with the edges by .
(iii) Equifibered Families. An equifibered family over a graph consists of a type family , and an indexed family of equivalences . A term of an equifibered family over consists of a section , in which is compatible with the edges by .
Using these varying notions of families, we can nicely detect the variances of the different type operations. For instance, if is a contravariant diagram over , and is a (covariant) diagram over , then is again a (covariant) diagram over . If was contravariant and covariant, then would be contravariant. Similarly for the W-graphs. If is contravariant and is covariant, then is contravariant, while if is covariant and contravariant, then is covariant. When you try to take where both and 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 prescribes precisely the descent data that is needed to get a type family over . Indeed, the descent theorem states that the type of [type families over ] is equivalent to the type of [equifibered families over ]. 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