This semester I’m doing a formalization project with Jeremy Avigad, based on work that I did mostly with Bas Spitters, back when I was a research assistant in Nijmegen. The goal of my project is to formalize several aspects of the graph model of type theory, using the Lean proof assistant. In this series of blog posts, I will try to explain what the graph model is, and how I will go about my formalization. The project itself may be found in the GraphModel github repository.
The graph model, and all its variations, is a model of type theory which one may use to study a theory of non-recursive higher inductive types. These include first of all homotopy coequalizers. Combining them with Σ-types one may use them to describe homotopy pushouts, and combining them with the natural numbers object one may use them to describe colimits of type sequences indexed by the natural numbers. Higher inductive types that can be constructed using the graph model include the spheres, CW-complexes such as the real and complex projective spaces, and with a bit more effort one can construct in a univalent universe which is closed under pushouts the image of a function from a small type into a locally small type . This fact can then be used to take -quotients. For the rest of this post, we suppose a univalent universe .
A graph in consists of a type of vertices, and a binary, type-valued relation . Now we may take advantage of the notion of type dependency which is already present in our setting to describe what it means to be a dependent graph over a given graph . A dependent graph over consists of a type family and a fiberwise binary relation . Thus, we have formalized what we mean by a judgment of the form in the graph model. We should also formalize what we mean by a judgment of the form in the graph model. A term of a dependent graph over consists of a term , and a term . This formalizes the absolute basics of type dependency: contexts, dependent types, and terms.
Of course, the graph model has a notion of context extension, which is modeled using Σ-types. Given a dependent graph over , we can form a new graph, which we denote by . The type of vertices of is defined to be the type . Then, for two vertices and of , the type of edges of is defined to be the type . We don’t yet need any axioms about context extension. Instead, let us haste to define dependent function graphs!
The formation rule for dependent function types says that for any type family we get a type family . Moreover, the introduction and elimination rules say that we can freely translate back and forth between terms of in context , and terms of in context . Thus, we have to formalize in the graph model the operation in accordance with the formation rule, such that we get an equivalence between the type type of terms of in context , and the type of terms of in context .
Let be a graph family over the graph . Then we define the type of vertices of the dependent function graph at to be . Now let be an edge from to in the graph , and let and . Then we define the type of edges from to over to be the type
Now it is an easy exercise to show that the type of terms of is equivalent to the type of terms of in a canonical way.
To model type constructors like , or identity types, we need a bit more of the structure of type dependency. In particular, we need weakening and substitution. The weakening operation (more precisely, weakening by a type in context ) allows us to obtain a dependent type from a dependent type . The substitution operation (by a term in context ), allows us to obtain a type from a dependent type . Both of these are pretty straightforward to model in the graph model, and both can be given an action on `further’ dependent types and their terms.
Back to the type constructors. The formation rule for dependent pair types tells us that for any dependent type , we get a dependent type . The introduction rule then tells us that there is a term
The induction principle then says that for any dependent type , from a term , one gets a term , so that
The above rule may look a bit intimidating, but it is just the computation rule, saying that if you compute the inductively defined term at the canonical values of , then you get back the original term. It will of course be no surprise that in the graph model, we use Σ-types to define the graph , and that this induction principle then holds.
It is now a good moment to remark on how we will treat judgmental equalities in internal models. All equalities will be modeled by typal equality, using the identity types. Eventually, it will be our aim to formulate a notion of `Rezk completeness’ for internal models, blurring the distinction between the interpretation of the judgmental equality of the theory, and the equality in the types of contexts, families and terms in such a way that internally (in the model) equivalent types become externally (from the point of view of the model) equal types. This is something to worry about later, but not at this stage.
The next post about the formalization of the graph model:
Formalizing the graph model of type theory, part 2