Formalizing the graph model of type theory, part 2

The most basic construction of higher inductive types can be formulated as a ‘left adjoint’ to the canonical homomorphism of models \Delta : U \to \mathsf{Graph}, 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 \Gamma in homotopy type theory consists of a type \Gamma_0:U, and a binary type-valued relation \Gamma_1:\Gamma_0\to{}\Gamma_0\to{}U. We can use this data to describe a higher inductive type \mathsf{colim}(\Gamma), in which the point constructors come from \Gamma_0, and the path constructors come from \Gamma_1. More precisely, there will be a graph morphism \eta : \Gamma\to\Delta(\mathsf{colim}(\Gamma)), where the data of such a morphism corresponds precisely to the data of the point and the path constructor of \mathsf{colim}(\Gamma). Here, given a type X, the graph \Delta(X) is defined as (X,\mathsf{Id}_X).

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 P:\mathsf{colim}(\Gamma)\to{}U be a family over \mathsf{colim}(\Gamma). Recall that, since \Delta is a morphism of models of type theory, it has an action on families. More precisely, we have a family \Delta(P) of graphs over \Delta(\mathsf{colim}(\Gamma)). We can now substitute \eta:\Gamma\to\Delta(\mathsf{colim}(\Gamma)) in \Delta(P) to obtain a family \Delta(P)\circ\eta over \Gamma, which we may call the transpose of P. The induction principle asserts that we get a section of P from a section of \Delta(P)\circ\eta.

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 s of P, using the action on terms of \Delta, so that it becomes a section \Delta(s)\circ\eta of \Delta(P)\circ\eta. Suppose the induction principle gave us the section s of P, from a section f of \Delta(P)\circ\eta. The computation rule now says that we have an equality \Delta(s)\circ\eta = f of sections of \Delta(P)\circ\eta.

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 \mathsf{colim}(\Gamma) is determined uniquely up to equivalence. In a univalent world this means that the type of all types X with a morphism f : \Gamma\to{}\Delta(X) satisfying an induction principle and a typal computation rule, is a mere proposition. In still other words, the ‘left adjoint’ to \Delta 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


Leave a Reply

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

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

Google+ photo

You are commenting using your Google+ 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 )

Connecting to %s