The most basic construction of higher inductive types can be formulated as a ‘left adjoint’ to the canonical homomorphism of models , and my interest in formalizing the graph model originates from this idea. Also, looking at the higher inductive types in this type theoretical framework has helped me prove a few theorems about them. One of them being a type theoretic formulation of the descent property, which was joint work with Bas Spitters back at the IAS.
Recall that a graph in homotopy type theory consists of a type , and a binary type-valued relation . We can use this data to describe a higher inductive type , in which the point constructors come from , and the path constructors come from . More precisely, there will be a graph morphism , where the data of such a morphism corresponds precisely to the data of the point and the path constructor of . Here, given a type , the graph is defined as .
The ‘universal property’ of higher inductive types will be their induction principle. In an induction principle, one specifies what data they need to obtain a section of a type family. So it is about families and sections, as is everything in type theory. I will state the induction principle in a way that is also going to fit nicely with my formalization of the graph model.
Let be a family over . Recall that, since is a morphism of models of type theory, it has an action on families. More precisely, we have a family of graphs over . We can now substitute in to obtain a family over , which we may call the transpose of . The induction principle asserts that we get a section of from a section of .
To state the computation rule (which always comes with the induction principle), we can play the same game. First we observe that we can transpose any section of , using the action on terms of , so that it becomes a section of . Suppose the induction principle gave us the section of , from a section of . The computation rule now says that we have an equality of sections of .
For our purposes it does not matter so much whether this equality is strict or typal. In fact, I tend to take it to be a typal equality, but in formalization projects it is helpful if the equality is strict at least on the level of vertices. Nevertheless, the typal computation rule suffices to show that the type is determined uniquely up to equivalence. In a univalent world this means that the type of all types with a morphism satisfying an induction principle and a typal computation rule, is a mere proposition. In still other words, the ‘left adjoint’ to specified in this way, is unique once it exists.
As a final note, we observe that our description of the graph quotient, i.e. the colimit of a graph, was given in a way that doesn’t depend so much on the internals of the graph model. We could as well have taken a different model, such as the reflexive graph model. The induction principle of the reflexive graph quotient can be stated in exactly the same way.
The previous post about the formalization of the graph model:
Formalizing the graph model of type theory, part 1