The groupoid model of intensional type theory

(working notes)

Steve Awodey^{∗}

June 28, 2001

Abstract

This note explains the groupoid model of intensional type theory, originally given by Hofmann and Streicher in [HS98].

The intensional identity type Id in Martin-Löf type theory, also called “propositional identity”, is governed by the following rules (cf. [Nor00]):

Introduction

\frac{a : A}{r(a) : Id_{A}(a, a)}  (1)

Elimination

\frac{c : Id_{A}(a, b)  x : A ⊢ d(x) : C(x, x, r(x))}{J(c, d) : C(a, b, c)}  (2)

Conversion

J(r(a), d) = d(a) : C(a, a, r(a))  (3)

The sign of equality in the above (“β”) conversion rule represents definitional equality, which is in general stronger than propositional identity, and in particular warrants all substitutions. The two notions coincide in case propositional identity is further assumed to be extensional, which can be characterized either by the following additional (“η”) conversion,

J(c, (x)d(x, x, r(x))) = d(a, b, c) : C(a, b, c)

∗Department of Philosophy, Carnegie Mellon University, Pittsburgh, USA, e-mail:

awodey@cmu.edu

or, equivalently, by replacing the single elimination rule above with the following two elimination rules (cf. [Jac99]).

Extensional elimination

\frac{c : Id_{A}(a, b)}{a = b : A}  \frac{c : Id_{A}(a, b)}{c = r(a) : Id_{A}a, b}  (4)

The system of dependent type theory with Σ, Π, and extensional propositional identity (as in [ML98]) can be modelled in a now well-known way in locally cartesian closed categories (modulo some technical fine points regarding substitution and coherence of pullbacks, cf. [Hof95]). It is shown in this note that no such interpretation of the intensional theory is possible. An alternative interpretation that does work is then presented. Technically, the main point is that the usual interpretation using the codomain fibration includes “too many objects in each fiber”, and the solution is to cut down to a subfibration.

1 Naive semantics

Let us try to model the rules above for identity types in the usual way, using the slice categories of an LCCC, and see what goes wrong.

For each type A (possibly depending on a context of types Γ), we have a new type Id_{A}(x, y) depending on (Γ and) two new variables x, y : A. If A is modelled as A → Γ, then Id_{A}(x, y) will be modelled as some object π : Id_{A}(x, y) → A ×_{Γ} A in the slice over (the domain of) A ×_{Γ} A.

We now omit reference to the type A in the notation Id_{A}(x, y), as well as to the context Γ. For the introduction rule, we pull Id(x, y) back along the diagonal δ : A → A × A, and require the resulting type over A to have a section r(x) : Id(x, x), as indicated below.

Id(x, x) \overline{}Id(x, y)
[figure: r]
[figure: A; = = = = = = = = =; A; δ; A × A]

Such a section r corresponds uniquely to a map A → Id(x, y) over A × A, also denoted r.

Id(x, y)
[figure: r]
[figure: A; δ; A × A]

For the elimination rule, we assume given a type γ : C(x, y, z) → Id(x, y) over Id(x, y) and a section d(x) : A → C(x, x, r(x)) of its pullback along r. As indicated in the following diagram, there is then supposed to be an associated section J_{d} of C(x, y, z) making everything commute.

C(x, x, r(x))  \overline{}C(x, y, z)
[figure: d; J_{d}]
[figure: A; = = = = = = = = = =; A; r; Id(x, y); γ; = = = =; Id(x, y)]
[figure]
A × A

In other words, given d : A → C(x, y, z) over Id(x, y) we need J_{d} such that

γ ∘ J_{d} = 1 and J_{d} ∘ r = d  (5)

as indicated in:

C(x, y, z)
[figure: d; J_{d}]
[figure: A; r; Id(x, y); γ; = = = =; Id(x, y)]

Briefly, every partial section of C over r : A → Id should extend to a global one.

But now observe that if this condition were satisfied, one could take A for C and r for γ to get a map J_{r} : Id → A which by the equations (5) would be an inverse to r. So we would have an isomorphism:

[figure: A; ≅; Id; A × A; δ; = = = = =; A × A; π]

This would in particular force the identity type Id to be extensional, in the sense that the rules (4) would be validated.

In sum,

1. intensional identity cannot be modelled in the slices of an LCCC in the usual way, i.e. as some structure on each (dependent) type, and

2. specifically, the map r : A → Id interpreting reflexivity must not be allowed to occur as (the structure map of) a dependent type, else the resulting elimination term J_{r} will force the identity type to be extensional.

2 The groupoid model

The key idea behind the groupoid interpretation is to endow each type with additional structure which is respected by forming dependent types, and then to require elimination only with respect to such structured types. Specifically, types are to be interpreted as groupoids^{1} and terms as (groupoid) homomorphisms. A dependent type x : A ⊢ B is interpreted as a homomorphism B → A that is furthermore a fibration of categories. Moreover, the identity type Id_{A} is then interpreted as the arrow category A^{→}.

Remark 2.1 The use of groupoids here is not essential; indeed, it’s likely that other structures would serve as well. Since identity types are not determined by a universal property, their interpretation is not fixed. One could perhaps use Quillen model categories to axiomatize the requirements for an interpretation.

1A groupoid is a category in which every arrow has an inverse. Thus a groupoid is a generalized group, in which the composition x · y of two elements is not always defined.

On the other hand, the groupoid model is quite natural, since the intensional identity type Id_{A} provides the type A with a groupoid structure in a very direct way. Specifically, one takes terms for reflexivity, symmetry, and transitivity as the identity, inverse, and composition operations respectively. Indeed, this fact can be used to prove semantic completeness by constructing a groupoid model in the syntactic category of an intensional type theory.

Let E be an LCCC, and consider the category Gpd(E) of groupoids in E, which is a CCC (is it an LCCC?). For any groupoid G in E, the category E^{G} of (internal) functors G → E is again an LCCC, and so Gpd(E^{G}) is again a CCC. Thus the functor category

Gpd(E)^{G} ≃ Gpd(E^{G})

is always a CCC and can be used to interpret the dependent types over G. Actually, we shall use instead the equivalent category of fibrations of groupoids in E, retaining the terminology and notation of the functor category Gpd(E)^{G} when convenient.

Observe that the condition for a homomorphism of groupoids π : H → G to be a categorical fibration (cf. [Jac99]) reduces to this:

For every g : a → b ∈ G and y ∈ H with π(y) = b,
there is some x ∈ H and h : x → y ∈ H with π(h) = g.

[figure: H; x; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; h; y; G; π; a; g; b]

Remark 2.2 To interpret the above condition internally in a LCCC, one can use the “BHK-interpretation” of the quantifiers, as presented in [Pal01]. Categorically, this amounts to requiring the fibration to be cloven. In fact, we shall assume the fibrations involved to be split.

Lemma 2.3 For any groupoid homomorphism α : H → G, the “precomposition” (i.e. pullback) functor

α^{∗} : E^{G} → E^{H}

preserves groupoids, as does its right adjoint α^{∗} ⊣ α_{∗}. Moreover, if α is a fibration, then the left adjoint α_{!} ⊣ α^{∗} preserves groupoids, too.

Proof. As right adjoints, both α^{∗} and α_{∗} are left exact, and so preserve all algebraic structure. For α_{!}, we regard a groupoid J in E^{H} as a fibration of groupoids β : J → H. If α : H → G is also a fibration, then so is α ∘ β : J → G, making it a groupoid in E^{G}.

In light of the previous lemma, we can interpret substitution of terms into dependent types by pullback as usual, and the dependent type forming operations Σ and Π can also be interpreted as usual as the left and right adjoints to (certain) pullbacks. Specifically, given closed types A and B and x : A ⊢ b : B and y : B ⊢ C type, the interpretation of x : A ⊢ C[b/y] type is the pullback C[b/y] = b^{∗}C,

[figure: (A, C[b/y]); (B, C); A; b; B .]

To interpret x : A ⊢ Σ_{B}C, we have the situation:

(A, B, C)
[figure: (A ⊢ Σ_{B}C)]
[figure: (A, B); (A, B ⊢ C); (A ⊢ B); A]

Since each side of the triangle is a fibration, the diagonal composite is also one. The interpretation of x : A ⊢ Π_{B}C is similarly straight-forward, using the right adjoint of pullback along (A ⊢ B) rather than the left.

For the interpretation of the identity type Id_{A}, we use the groupoid A^{→} of arrows in (the interpretation of) A. Recall that the objects of A^{→} are arrows c : a → b in A, and an arrow f from c : a → b to another object c′ : a′ → b′ is a pair of arrows (f_{0}, f_{1}) making a commutative square:

[figure: a; f_{0}; a′; b; c; f_{1}; b′; c′]  (6)

The interpretation of the dependent type x:A, y:A ⊢ Id_{A}(x, y) is the arrow:

\begin{matrix}A^{→} \\ A × A & \begin{aligned}π \\ & \end{aligned} \end{matrix}

given by:

π = (d_{0}, d_{1})

i.e. the domain and codomain projections. To see that π is a fibration, take an arrow in A × A, consisting of a pair (c : a → b, c′ : a′ → b′), and let f_{1} : b → b′ be an object over (b, b′). Then one finds f_{0} as in (6) just by putting:

f_{0} = (c′)^{−1} ∘ f_{1} ∘ c

Verifying the rules for Id, the interpretation of the reflexivity term x:A ⊢ r(x) : Id_{A}(x, x) is the identity homomorphism,

r : A → A^{→}

taking a ∈ A to the identity arrow r(a) = 1_{a} : a → a. For the elimination rule, suppose given a fibration γ : C → A^{→} and a section d : A → C over r : A → A^{→}. To define J_{d} : A^{→} → C, take an object c : a → b in A^{→} and consider the arrow (c, 1_{b}) : c → 1_{b},

[figure: a; c; b; b; c; 1_{b}; b .; 1_{b}]

We have d(b) in the fiber of γ over 1_{b} = r(b), so by the fibration condition there is an arrow (c, 1_{b})^{∗}(d(b)) → d(b) over (c, 1_{b}). Let:

J_{d}(c) = (c, 1_{b})^{∗}(d(b)) .  (7)

This assignment is easily seen to be functorial, and one plainly has γ(J_{d}(c)) = c and J_{d}(r(a)) = a, as required.

Finally, let us check that the reflexivity arrow r : A → A^{→} will generally not occur as a dependent type over A^{→}. This is so because it is not a fibration. Indeed, given an arrow in A^{→} as in (6) if there is an object over (b, b′) then b = b′. But it may still be the case that a ≠ a′, in which case there will be no object over (a, a′).

References

[Hof95] M. Hofmann. On the interpretation of type theory in locally cartesian closed categories. In L. Pacholski and J. Tiuryn, editors, Computer Science Logic 1994, volume 806 of Lecture Notes in Computer Science. Springer, 1995.

[HS98] M. Hofmann and T. Streicher. The groupoid interpretation of type theory. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, August 1998. Proceedings of a Congress held in Venice, Italy, October 1995.

[Jac99] B. Jacobs. Categorical Logic and Type Theory. Elsevier Science, 1999.

[ML98] P. Martin-Löf. An intuitionistic theory of types. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, August 1998. Proceedings of a Congress held in Venice, Italy, October 1995.

[Nor00] B. Nordstrom, K. Peterson, and J. Smith. Programming in Martin-Löf’s Type Theory. Oxford University Press, 1990.

[Pal01] E. Palmgren. A categorical version of the BHK-interpretation. Technical report, Institut Mittag-Leffler, The Royal Swedish Academy of Sciences, 2001.