Formalizing the graph model of type theory, part 1

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 U which is closed under pushouts the image of a function f : A \to{} X from a small type A into a locally small type X. This fact can then be used to take \infty-quotients. For the rest of this post, we suppose a univalent universe U.

A graph \Gamma in U consists of a type \Gamma_0 of vertices, and a binary, type-valued relation \Gamma_1 : \Gamma_0 \to{} \Gamma_0 \to{} U. 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 \Gamma. A dependent graph A over \Gamma consists of a type family A_0 : \Gamma_0 \to{} U and a fiberwise binary relation A_1 : \Pi_{(i,j : \Gamma_0)} \Gamma_1(i,j)\to{} (A_0(i) \to{} A_0(j) \to{} U). Thus, we have formalized what we mean by a judgment of the form \Gamma \vdash A~\mathrm{Type} in the graph model. We should also formalize what we mean by a judgment of the form \Gamma \vdash a : A in the graph model. A term a:A of a dependent graph A over \Gamma consists of a term a_0 : \Pi_{(i:\Gamma_0)}~A_0(i), and a term a_1 : \Pi_{(i,j:\Gamma_0)}\Pi_{(e:\Gamma_1(i,j))}~A_1(e,a_0(i),a_0(j)). 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 A over \Gamma, we can form a new graph, which we denote by \Gamma.A. The type of vertices of \Gamma.A is defined to be the type (\Gamma.A)_0 := \Sigma_{(i:\Gamma_0)}~A_0(i). Then, for two vertices (i,x) and (j,y) of \Gamma.A, the type of edges of \Gamma.A is defined to be the type (\Gamma.A)_1((i,x),(j,y)) := \Sigma_{(e:\Gamma_1(i,j))}~A_1(e,x,y). 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 \Gamma.A \vdash{} P we get a type family \Gamma \vdash{} \Pi(A,P). Moreover, the introduction and elimination rules say that we can freely translate back and forth between terms of P in context \Gamma.A, and terms of \Pi(A,P) in context \Gamma. Thus, we have to formalize in the graph model the operation \Pi in accordance with the formation rule, such that we get an equivalence between the type type of terms of P in context \Gamma.A, and the type of terms of \Pi(A,P) in context \Gamma.

Let P be a graph family over the graph \Gamma.A. Then we define the type of vertices of the dependent function graph \Pi(A,P) at i:\Gamma_0 to be \Pi(A,P)_0(i) := \Pi_{(x:A_0(i))} P_0(i,x). Now let e : \Gamma_0(i,j) be an edge from i to j in the graph \Gamma, and let f : \Pi(A,P)_0(i) and g : \Pi(A,P)_0(j). Then we define the type of edges from f to g over e to be the type

\Pi(A,P)_1(e,f,g):=\Pi_{(x:A_0(i))}\Pi_{(y:A_0(j))}\Pi_{(s:A_1(e,x,y))}~ P_1((e,s),f(x),g(y)).

Now it is an easy exercise to show that the type of terms of P is equivalent to the type of terms of \Pi(A,P) in a canonical way.

To model type constructors like \Sigma, \mathsf{W} 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 A in context \Gamma) allows us to obtain a dependent type \Gamma.A \vdash{} \langle A\rangle B from a dependent type \Gamma \vdash{} B. The substitution operation (by a term x:A in context \Gamma), allows us to obtain a type \Gamma \vdash{} P[x] from a dependent type \Gamma.A \vdash{} P. 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 \Gamma.A\vdash{} P, we get a dependent type \Gamma \vdash{} \Sigma(A,P). The introduction rule then tells us that there is a term

(\Gamma.A).P \vdash \mathsf{pair}^{A,P} : \langle P\rangle\langle A\rangle \Sigma(A,P).

The induction principle then says that for any dependent type \Gamma.\Sigma(A,P) \vdash{} C, from a term (\Gamma.A).P \vdash t : (\langle P\rangle\langle A\rangle C)[\mathsf{pair}^{A,P}], one gets a term \Gamma.\Sigma(A,P)\vdash{} \mathsf{ind}_{\Sigma(A,P)}(t) : C, so that

{}(\Gamma.A).P \vdash{} (\langle{} P\rangle{}\langle{} A\rangle{} (\mathsf{ind}_{\Sigma(A,P)} (t)))[\mathsf{pair}^{A,P}] = t : (\langle{} P\rangle{}\langle{} A\rangle{} C)[\mathsf{pair}^{A,P}]

The above rule may look a bit intimidating, but it is just the computation rule, saying that if you compute the inductively defined term \mathsf{ind}_{\Sigma(A,P)}(t) at the canonical values of \Sigma(A,P), 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 \Sigma(A,P), 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

Advertisements

One thought on “Formalizing the graph model of type theory, part 1

  1. Pingback: What I learned this summer about coinductive types | Egbert RIJKE

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