The groupoid interpretation of type theory

Martin Hofmann and Thomas Streicher

August 27, 1996

1 Introduction

Many will agree that identity sets are the most intriguing concept of intensional Martin-Löf type theory. For instance, it may appear surprising that their axiomatisation as an inductive family allows one to deduce the usual properties of equality, notably the replacement rule (Leibniz’ principle) which allows one to conclude P (a′) from P (a) and a proof that a equals a′. Here, unlike in other logical systems, this holds for arbitrary families of sets P not necessarily corresponding to a predicate. This is not in conflict with decidability of type checking since if a equals a′ and p : P (a) then one does not in general have p : P (a′), but only subst(s, p) : P (a′) where s is the proof that a equals a′ and subst is defined from the eliminator for identity sets.

It is now a natural question to ask whether these translation functions subst(s, ) actually depend upon the nature of the proof s or, more generally, the question whether any two elements of an identity set are equal. We will call UIP(A) (U niqueness of I dentity Proofs) the following property. If a_{1}, a_{2} are objects of type A then for any two proofs p and q of the proposition “a_{1} equals a_{2}” there is another proof establishing equality of p and q. More generally, UIP will stand for UIP(A) for all types A. Notice that in traditional logical formalism a principle like UIP cannot even be sensibly expressed as proofs cannot be referred to by terms of the object language and thus are not within the scope of propositional equality.

The question whether UIP is valid in intensional Martin-Löf type theory was open for a while though it was commonly believed that UIP is underivable as any attempt for constructing a proof has failed (Coquand 1992; Streicher 1993; Altenkirch 1992). On the other hand, the intuition that a type is determined by its canonical objects might be seen as evidence for the validity of UIP as the identity sets have at most one canonical element corresponding to a proof of reflexivity. Indeed, UIP is derivable in an extension of type theory based on this intuition, namely type theory augmented with pattern matching as implemented in the Alf system (Coquand 1992; Altenkirch et al. 1994).

In this paper we answer the question of derivability of UIP in pure type theory in the negative by exhibiting a counter model. By the above, this model does not validate pattern matching thereby providing a proof that the latter is not conservative over traditional type theory.

The model we give stands in sharp contrast to the abovementioned intuition of types being determined by their canonical inhabitants. In the model a type A will consist of a set |A| of objects together with (possibly empty) sets A(a_{1}, a_{2}) of “proofs” that a_{1}, a_{2} ∈ |A| are propositionally equal. Although a closed term of type A will be modelled as an object of A an open term will not only map objects to objects but also equality proofs to equality proofs. Thus, an open term is not fully determined by its behaviour on closed terms. The principle UIP can then be refuted by including a type in which the set A(a_{1}, a_{2}) has more than one element for some a_{1}, a_{2} ∈ |A|.

The hard work consists of demonstrating that these mathematical objects can indeed interpret all of Martin-Löf’s type theory. It turns out that various additional structure has to be imposed for that purpose. In particular, we need for each type a composition, identities, and inverses; that is to say functions

∘ : A(a_{2}, a_{3}) × A(a_{1}, a_{2}) → A(a_{1}, a_{3})
id : A(a_{1}, a_{1})
( )^{−1} : A(a_{1}, a_{2}) → A(a_{2}, a_{1})

for all objects a_{1}, a_{2}, a_{3} witnessing that propositional equality is an equivalence relation. In order to interpret the various type and term formers it turns out that these operations must satisfy certain equations. Namely, composition must be an associative operation with neutral element id with inverses given by ( )^{−1}. In other words every type will be a groupoid, i.e. a category with isomorphisms only. Open terms and dependent types will then be interpreted as certain functors taking account of the fact that propositional equality is preserved by function application.

A posteriori this justifies a view of propositional equality in type theory as a notion of isomorphism. We exploit this view by exhibiting non-standard axioms for propositional equality on universes which contradict UIP and pattern matching. These axioms are put to use in a new formalisation of categories in type theory in which isomorphic objects are propositionally equal.

Independently, François Lamarche (1991) has investigated the logical structure of the category of groupoids with the motivation of finding a logical system in which classes of mathematical structures appear as types. He observed that a theory with type dependency arises as a natural candidate for an internal language of the category of groupoids. He gives interpretations of dependent function spaces and sums which agree essentially with ours.

Parts of the material presented in this article have already been published by the authors in (1993, 1994, 1995). The main purpose of the current version is to make the material accessible to a wider audience and to serve as future reference. As opposed to the extended abstract (Hofmann and Streicher 1994) the model construction is described here in full detail and also in more elementary terms. Furthermore, the syntactic extensions to pure type theory which have been sketched in (Hofmann 1995) are worked out here in detail. The application to formalisation of basic category theory and the analysis of interpretations of universes are altogether new.

Acknowledgements

We are indebted to Thorsten Altenkirch, Thierry Coquand, Peter Dybjer, Per Martin-Löf for numerous discussions on equality in type theory and to François Lamarche for explanations and discussions about the groupoid model. The diagrams have been typeset using Paul Taylor’s Latex package.

2 Syntax

We work in Martin-Löf’s type theory formulated inside a Logical Framework as defined in Ch. 19 & 20 of (Nordström, Petersson, and Smith 1990). However, we will use a slightly different notation as will be explained below. This type theory derives judgements of the following forms:

• A type to mean that A is a type,

• a : A to mean that a is an object of type A

• A = B to mean that types A and B are definitionally equal,

• a = a′ : A to meant that a and a′ are definitionally equal objects of type A.

All judgements are relative to a list of variable declarations of the form x_{1}: A_{1}, …, x_{n}: A_{n} where the variables x_{1}, …, x_{n} are distinct and A_{i} type holds under the assumption x_{1}: A_{1}, …, x_{i−1}: A_{i−1}. Such lists of assumptions are called contexts and are ranged over by capital Greek letters Γ, Δ, . . .. One writes J [Γ] (alternatively Γ ⊢ J) to indicate that judgement J holds in context Γ. In the formal presentation (which we include as an appendix) the valid judgements in context, i.e. under assumptions, are defined inductively; context validity is included as an auxiliary judgement. In the informal presentation below we only indicate the relevant part of a context.

If A type and B type under [x: A] then the dependent function space (x: A)B is a type. If b : B [x: A] then [x: A]b : (x: A)B. Conversely, if f : (x: A)B and a: A then f(a) : B[x:=a]. This typed abstraction constitutes the main difference to the presentation in loc.cit.

We have β-equality

([x: A]b) (a) = b[x:=a] : B[x:=a]

and also η-equality

[x: A]b(x) = b : (x: A)B

provided x is not free in b.

Iterated applications of the form f(a_{1})(a_{2}) ⋯ (a_{n}) are written as f(a_{1}, …, a_{n}) where we take the freedom of omitting arguments which can be inferred from later ones.

There is a special type Set containing names for certain types, the so-called sets, as objects. Whenever A : Set then we have El(A) type, in particular, we can form the “generic” family El(A) type [A: Set]. It is common to omit the El operator, thus writing a: A instead of a: El(A). Nordström et al. write a ∈ A for a : El(A). We want to reserve the ∈-symbol for membership in the metatheory.

This machinery allows one to introduce set formers and term forming operations (be they constructors or eliminators) simply as constants together with their definitional equalities. For example, the intensional identity sets are given by the following constants.

Id : (A: Set)(a_{1}, a_{2}: A)Set

refl : (A: Set)(a: A)Id(A, a, a)

J : (A: Set)(C: (a_{1}, a_{2}: A)(s: Id(A, a_{1}, a_{2}))Set)(d : (a: A)C(a, a, refl(A, a))) (a_{1}, a_{2}: A)(s: Id(A, a_{1}, a_{2}))C(a_{1}, a_{2}, s)

In addition, we impose the definitional equality

J(A, C, d, a, a, refl(A, a)) = d(a) : C(a, a, refl(A, a)) Id-C

for A, C, d, a of appropriate type. Note that J is called idpeel in loc.cit.. According to our convention on omitting redundant arguments we will usually write Id(a_{1}, a_{2}) and refl(a) instead of Id(A, a_{1}, a_{2}) and refl(A, a), respectively.

In addition to identity sets we also use Π-sets, Σ-sets, disjoint union, natural numbers, and a universe. See the appendix for their formal definition. Following common practice, we write A → B for Π(A, [a: A]B) and and A × B for Σ(A, [a: A]B) if A and B are types or sets (in the case of ×).

The notion of equality induced by identity sets is called propositional equality (as opposed to definitional equality). That is to say, two objects a_{1}, a_{2} : A are propositionally equal if Id(a_{1}, a_{2}) is inhabited. The main purpose of propositional equality is that it can be assumed in contexts and thus allows for hypothetical equality reasoning. In particular, propositional equality can be established by induction.

Definitional equality, on the other hand, can only be established by pure equational reasoning, i.e. corresponds to the equational theory generated by the postulated equality judgements.

Accordingly, definitional equality is (at least in traditional cases) decidable, whereas propositional equality is not, as soon as one includes natural numbers and Π-sets.

By the congruence rules for definitional equality the latter always entails the propositional one, but not necessarily vice versa.

3 Syntactic considerations on identity sets

The elimination operator J is motivated by the view of Id(A, , ) as an inductively defined family with constructor refl. Accordingly, J permits one to define an object of type (a_{1}, a_{2}: A)(s: Id(A, a_{1}, a_{2})C(a_{1}, a_{2}, s) by prescribing its behaviour for arguments of canonical form, i.e. a_{1} = a_{2} = a and s = refl(A, a).

In the presence of Π-sets, this elimination operation J allows one to derive the following replacement rule in the presence of Π-sets.

subst : (A: Set)(P: (a: A)Set)(a_{1}, a_{2}: A)(s: Id(a_{1}, a_{2}))P (a_{1}) → P (a_{2})

satisfying subst(refl(a), p) = p

See loc.cit. for the definition of subst.

From subst one easily derives symmetry and transitivity of propositional equality as well as congruence with respect to function application:

sym : (A: Set)(a_{1}, a_{2}: A)Id(a_{1}, a_{2}) → Id(a_{2}, a_{1})
trans : (A: Set)(a_{1}, a_{2}, a_{3}: A)
Id(a_{2}, a_{3}) → Id(a_{1}, a_{2}) → Id(a_{1}, a_{3})
resp : (A: Set)(B: Set)(u: (a: A)B)
(a_{1}, a_{2}: A)Id(a_{1}, a_{2}) → Id(u(a_{1}), u(a_{2}))

Notice that we supply arguments to trans in the applicative order.

We also have the following dependent version of resp.

resp′ : (A: Set)(B: (a: A)Set)(u: (a: A)B(a))
(a_{1}, a_{2}: A)(s: Id(a_{1}, a_{2}))Id(subst(s, u(a_{1})), u(a_{2}))

To derive resp′ the full power of J is needed; subst alone does not suffice.

3.1 Uniqueness of identity proofs (UIP )

For most inductive sets it is possible show that arbitrary objects are propositionally equal to canonical ones. For example, the following types are inhabited

(n: N)Id(n, 0) + Id(n, succ(pred(n))) (f: Π(A, B))Id(f, fun([x: A]apply(f, x)))

There are several ways of stating an analogous property for identity sets. We introduce the following abbreviations.

UIP =^{def} (A: Set)(a_{1}, a_{2}: A)(s_{1}, s_{2}: Id(a_{1}, a_{2}))Id(s_{1}, s_{2})

UIP refl =^{def} (A: Set)(a: A)(s: Id(a, a))Id(s, refl(a))

UIP tuple =^{def} (A: Set)(a_{1}, a_{2}: A)(s: Id(a_{1}, a_{2}))

Id(Σ([a_{1}: A]Σ([a_{2}: A]Id(a_{1}, a_{2}))) , ⟨a_{1}, a_{2}, s⟩ , ⟨a_{1}, a_{1}, refl(a_{1})⟩)

Using J, one can show that UIP tuple is inhabited and that UIP refl(A) and UIP(A) are equivalent for each A: Set. See (Streicher 1993) for the proofs. He also explains that in the presence of UIP the eliminator J can be defined in terms of the derived operator subst thereby allowing for a very intuitive axiomatisation of propositional equality in terms of a uniqueness property of identity proofs and a type-theoretic pendant of Leibniz’ principle stating that replacement of equal objects preserves validity.

It is also known (Coquand 1992) that an object of UIP can be constructed by pattern-matching.

The main result of this paper consists of an interpretation of type theory in which UIP (Uniqueness of Identity Proofs) is not inhabited. A fortiori, UIP is not derivable and, therefore, pattern-matching is not a conservative extension of Martin-Löf type theory.

3.2 Definability of instances of UIP

Although UIP is not derivable in general, instances UIP(A) for certain sets A are inhabited. Hedberg (1995) has shown that this is in particular the case if A admits a decidable equality, that is to say, if there is a function eq : A → A → N such that Id(eq(a_{1}, a_{2}), 0) and Id(a_{1}, a_{2}) are equivalent. One can also show that UIP is preserved by the set formers Σ and disjoint union. It is also preserved by the identity set former itself, provided one further assumes that UIP applied to proofs by reflexivity gives back a proof by reflexivity. Below we will demonstrate that UIP(Π(A, B)) follows from UIP(A) and (a: A)UIP(B(a)) under the assumption of an extensionality axiom. This gives UIP for all sets definable without universes.

3.3 Alternatives to UIP

Streicher (1993) gives another principle equivalent to UIP which in its formulation does not mention propositional equality of identity proofs:

cong snd =^{def} (A: Set)(B: (a: A)Set)(a: A)(b, b′: B(a))
(s: Id(Σ(A, B), ⟨a, b⟩ , ⟨a, b′⟩))Id(B, b, b′)

He also introduces an eliminator K for the family Id(A, a, a) [a: A]:

K : (A: Set)(C: (a: A)(s: Id(A, a, a))Set)(d : (a: A)C(a, refl(A, a)))
(a: A)(s: Id(A, a, a))C(a, s)

satisfying K(d, refl(a)) = d(a). Using K an inhabitant of UIP may be constructed.

Both alternatives can be directly defined using pattern matching. It is an open problem whether the converse is also true, i.e. whether pattern matching forms a conservative extension of type theory augmented by K (or a constant of type UIP together with an appropriate conversion rule).

3.4 Propositional equality as isomorphism

It has been argued in (Hofmann 1995) that intensional type theory augmented by UIP together with an extensionality axiom for Π-sets can simulate extensional type theory whilst retaining decidability of type checking.

On the other hand, we will demonstrate below that Martin-Löf’s original formulation of identity sets allows for the addition of axioms (inconsistent with UIP) expressing a view of propositional equality as a generalised notion of isomorphism. Intuitively, these axioms state that for a universe U and A, B : U the identity set Id(U , A, B) corresponds to the set of isomorphisms between A and B. Such version of identity sets may be useful for a formulation of category theory inside type theory providing a formal underpinning for the common practice of considering isomorphic objects as equal.

4 The groupoid interpretation

Although the principle UIP turns out as being non-derivable, certain propositional equalities between objects of identity sets can be established using J. If A : Set and a_{1}, a_{2} : A and s_{1}, s_{2} : Id(a_{1}, a_{2}) then we write s_{1} =_{prop} s_{2} to mean that Id(Id(a_{1}, a_{2}), s_{1}, s_{2}) is inhabited.

Proposition 4.1 1. If a_{1}, a_{2} : A and s : Id(a_{1}, a_{2}) then

trans(s, refl(a_{1})) =_{prop} s
trans(refl(a_{2}), s) =_{prop} s
trans(sym(s), s) =_{prop} refl(a_{1})
trans(s, sym(s)) =_{prop} refl(a_{2})

2. If a_{1}, a_{2}, a_{3}, a_{4} : A and s_{1} : Id(a_{1}, a_{2}) and s_{2} : Id(a_{2}, a_{3}) and s_{3} : Id(a_{3}, a_{4})

then

trans(s_{3}, trans(s_{2}, s_{1})) =_{prop} trans(trans(s_{3}, s_{2}), s_{1})

3. If A, B : Set and a_{1}, a_{2}, a_{3} : A and f : (a: A)B and s_{1} : Id(a_{1}, a_{2}) and s_{2} : Id(a_{2}, a_{3}) then

resp(f, refl(a_{1})) =_{prop} refl(f(a_{1}))
resp(f, trans(s_{2}, s_{1})) =_{prop} trans(resp(f, s_{2}), resp(f, s_{1}))

Proof. All of these follow straightforwardly using J. As an example we derive trans(sym(s), s) =_{prop} refl(a_{1}) where s : Id(A, a_{1}, a_{2}). We put

C =^{def} [a_{1}, a_{2}: A][s: Id(a_{1}, a_{2})]Id(trans(sym(s), s) , refl(a_{1}))

We have

J(A, C, d, a_{1}, a_{2}, s) : Id(trans(sym(s), s) , refl(a_{1}))

where

d =^{def} [a: A]refl(Id(A, a, a), refl(A, a))

The object d(a) has the required type C(a, a, refl(A, a)) because both sym(refl(a)) and trans(refl(a), refl(a)) are definitionally equal to refl(a). This in turn follows from the definition of sym and trans in terms of subst. □

These propositional equalities suggest that one can view a set as a category having as objects the objects of A and in which a morphism from a_{1} to a_{2} is an object of Id(A, a_{1}, a_{2}), or rather an equivalence class of such objects by propositional equality. Composition is then given by transitivity and reflexivity gives the identities. Symmetry, on the other hand, establishes that every such morphism is actually an isomorphism.

A category in which every morphism is an isomorphism is called a groupoid. So the identity sets endow every set with a groupoid structure in a natural way. Furthermore, the equations under 4.1 (3) establish that a function f from A to B extends to a functor from A to B with morphism part given by resp(f, ).

Under this view the principle UIP translates into the statement that every such groupoid is in fact a trivial one with at most one morphism between any two objects. This suggests that a refutation of the principle UIP can be obtained by way of an interpretation of type theory in which types are interpreted as arbitrary groupoids, provided one succeeds in ascribing appropriate meaning to the type and set formers. We will do exactly this in the rest of this section.

Our metalanguage for the construction of the interpretation is informal set theory augmented with Grothendieck universes or inaccessible cardinals. We use set theory merely for convenience; all our definitions can also be carried out in extensional Martin-Löf type theory with universes which shows that our constructions do not depend upon the consistency of large cardinals. We assume some basic knowledge of category theory, notably the concepts of category, functor, and natural transformation, see (Mac Lane 1971).

4.1 Groupoids

A groupoid^{1} is a category Γ where all morphisms are isomorphisms.The groupoids together with functors between them form a (large) category GPD.

4.1.1 Examples

The products and exponentials of groupoids qua categories are groupoids again so that GPD is cartesian closed. Recall that the objects of Γ×Δ are pairs (γ, δ) where γ ∈ Γ and δ ∈ Δ and that the objects of Γ ⇒ Δ are functors from Γ to Δ.

For every set X the discrete category △(X) with only identities as morphisms is a groupoid—the discrete groupoid over X. If x ∈ X we write ⋆ rather than id_{x} for the △(X)-morphism from x to x. Notice that we have ⋆ : x → y iff x = y. We remark that △{⟨⟩} is a terminal object in GPD denoted []. More generally, a groupoid will be called discrete if all its morphisms are identities. Note that up to isomorphism discrete groupoids are of the form △(X).

1In universal algebra the term groupoid is sometimes used for a set with a binary operation.

Our use of the term groupoid is in accordance with homotopy theory and category theory, cf. (Brown 1988).

Every group G can be viewed as a one-object groupoid in the obvious way.

Types (at least non-dependent ones) will be interpreted as groupoids, their closed terms as objects of groupoids. The rôle of the morphisms in a groupoid is to give meaning to propositional equality. Composition of these morphisms accounts for transitivity, identity corresponds to reflexivity, and the inverses to symmetry.

Open terms are interpreted as functors between groupoids where the morphism part witnesses the preservation of propositional equality.

Notation. We notationally identify a groupoid with its underlying set of objects thereby writing γ ∈ Γ to mean that γ is an object of Γ. We write p^{−1} for the inverse of morphism p.

4.2 Families of groupoids

To obtain a full-fledged interpretation of type theory we need to account for type dependency, that is we have to define a notion of a family of groupoids indexed over a groupoid. This notion should be such that the usual type formers can receive appropriate meaning and in particular such that the homset Γ(−, −) arises as a family of groupoids indexed over Γ × Γ thus providing meaning for the identity types.

Fortunately, category theory provides us with such a notion of dependency. A family of groupoids indexed over groupoid Γ is a functor A : Γ → GPD.

Notice that such a functor yields a groupoid A(γ) for each γ ∈ Γ and moreover a functor A(p) : A(γ) → A(γ′) whenever p : γ → γ′. This will serve as interpretation of replacement and more generally of identity elimination. The fact that A itself is a functor ensures that the functors A(p) are compatible with the groupoid structure of Γ, in particular, we have A(p) ∘ A(p^{−1}) = id_{A(γ′)} and A(p^{−1}) ∘ A(p) = id_{A(γ)}, thus all the functors A(p) are actually isomorphisms of groupoids.

4.2.1 Notation

If p : γ → γ′ and a ∈ A(γ) then we write p · : A(γ) → A(γ′) for the functor A(p).

We write Ty(Γ) for the collection of families of groupoids indexed over Γ. When f : Δ → Γ is a morphism in GPD and A ∈ Ty(Γ) then the composition A ∘ f is an element of Ty(Δ). We use the notation A{f} for this family. In this way Ty extends to a contravariant “collection-valued” functor on GPD.

4.2.2 Example

If Γ is a groupoid then a family of groupoids I_{Γ} indexed over Γ × Γ is defined by I_{Γ}(γ_{1}, γ_{2}) = △(Γ(γ, γ′)) and I_{Γ}((p_{1}, p_{2}))(q) = p_{2} ∘ q ∘ p_{1}^{−1} where p_{i} : γ_{i} → γ′_{i} and q ∈ I_{Γ}(γ_{1}, γ_{2}). Notice that

I_{Γ} = hom_{Γ}(( )^{−1}, )

where ( )^{−1} : Γ^{op} → Γ is the obvious isomorphism between Γ^{op} and Γ. Notice that the restriction to groupoids is the minimal requirement for making hom covariant in both arguments.

This family I_{Γ} will be the interpretation of the family of identity set when Γ is the interpretation of a closed type. Below, we will generalise I_{Γ} to families of groupoids.

4.3 Objects of families

Let A ∈ Ty(Γ) be a family of groupoids over Γ. A (dependent) object M of A consists of the following data

• an A(γ)-object M(γ) for each γ ∈ Γ,

• for each morphism p : γ → γ′ an A(γ′)-morphism M(p) : p ·(M(γ)) → M(γ′)

such that

M(id_{γ}) = id_{M(γ)}

and

M(p′ ∘ p) = M(p′) ∘ (p′ · M(p))

Apart from the “adjustment” p′ · in the second equation required to make the right-hand side typecheck these laws express functoriality of M. After having defined the semantic counterpart of context formation we will be able to identify dependent objects as corresponding to certain functors.

We write Tm(A) for the collection of dependent objects of A. For functor f : Δ → Γ the operation {f} : Ty(Γ) → Ty(Δ) extends to dependent objects. If A ∈ Ty(Γ) and a ∈ Tm(A) then a{f} ∈ Ty(A{f}) is given by composing the components of a with f in the obvious way.

4.4 Category-theoretic semantics

Our plan is to organise groupoids and families of groupoids into a model of dependent type theory, namely a category with families (CwF). This notion of model was invented by Dybjer, see (Dybjer 1996), and subsequently used by Martin-Löf (Per Martin-Löf 1995). Our reference for CwFs is the survey article (Hofmann 199). Let us review here that a CwF consists of the following data.

• A category C of contexts and substitutions with terminal object [] corresponding to the empty context.

• A collection-valued functor Ty : C^{op} → Set associating with each context Γ the collection of types depending on it. If f : Δ → Γ and A ∈ Ty(Γ) one writes A{f} for Ty(f)(A). The type A{f} corresponds to the substitution of f into A.

• For each Γ ∈ C and A ∈ Ty(Γ) a collection of terms Tm(Γ, A) together with a substitution function Tm(f, A) : Tm(Γ, A) → Tm(Δ, A{f}) functorial in f : Δ → Γ in the obvious sense.

• For each A ∈ Ty(Γ) a so-called context extension Γ.A which has the property that the homset C(Δ, Γ.A) and {(f, M) | f : Δ → Γ and M ∈ Tm(Δ, A{f})} are isomorphic naturally in Δ.

• Operations corresponding to the desired type, set, and term formers.

We have already defined the category of contexts, namely GPD, and the collections Ty and Tm together with the required substitution operations.

4.5 Context extension

If A ∈ Ty(Γ) is a family of groupoids the context extension Γ.A is the total category of the co-fibration obtained by applying the Grothendieck construction to A. In more explicit terms the groupoid Γ.A takes the following form.

The objects of Γ.A are pairs (γ, a) where γ ∈ Γ and a ∈ A(γ). A morphism in Γ.A from (γ, a) to (γ′, a′) is a pair (p, q) where p ∈ Γ(γ, γ′) and q ∈ A(γ′)(p · a, a′). The composition of (p, q) : (γ, a) → (γ′, a′) and (p′, q′) : (γ′, a′) → (γ′′, a′′) is defined as (p′ ∘ p, q′ ∘ (p · q)). The identity at (γ, a) is (id_{γ}, id_{a}). The inverse of (p, q) : (γ, a) → (γ′, a′) is (p^{−1}, p^{−1} · q^{−1}) : (γ′, a′) → (γ, a). The verifications are left to the reader.

The projection sending (γ, a) to γ and (p, q) to p is a morphism of groupoids from Γ.A to Γ. It is called the canonical projection associated to A and is denoted p_{A} : Γ.A → Γ.

In order that Γ.A indeed captures context extension we need a bijective correspondence between the set

{(f, M) | f : Δ → Γ and M ∈ Tm(A{f})}

and the homset GPD(Δ, Γ.A). Given f : Δ → Γ and M ∈ Tm(A{f}) we define ⟨f, M⟩_{A} : Δ → Γ.A by

\begin{matrix}⟨f, M⟩_{A}(δ) = (f(δ), M(δ)) \\ ⟨f, M⟩_{A}(p) = (f(p), M(p)) \end{matrix}

To obtain an inverse we first define a semantic analogue to the sequent Γ, x: A ⊢ x : A as follows. A dependent object v_{A} ∈ Tm(A{p_{A}}) is given by

\begin{matrix}v_{A}(γ, a) = a \\ v_{A}(p, q) = q \end{matrix}

Notice that A{p_{A}} ∈ Ty(Γ.A).

Now, if h : Δ → Γ.A then we have p_{A}∘h : Δ → Γ and v_{A}{h} ∈ Tm(A{p_{A}∘h}) It is routine that these data establish the required bijective correspondence

natural in Δ.

We have established that groupoids and families of groupoids form an instance of a CwF.

It remains to identify dependent function spaces and an appropriate universe Set, as well as, interpretations of the set formers, in particular the identity sets. We treat these issues in order.

4.6 Dependent function space

To each dependent object M ∈ Tm(A) we can associate a functor \overline{M} : Γ → Γ.A by \overline{M}(γ) = (γ, M(γ)) and \overline{M}(p) = (p, M(p)). We have p_{A} ∘ S = id_{Γ}. Conversely, given a section f : Γ → Γ.A of p_{A}, i.e. p_{A} ∘ f = id_{Γ} then we have f(γ) = (γ, M(γ)) and f(p) = (p, M(p)) for a uniquely determined M ∈ Tm(A).

This correspondence enables us to view Tm(A) (for A ∈ Ty(Γ)) not merely as a set, but as a groupoid. A morphism τ from term M to term N is an assignment of an A(γ)-morphism τ_{γ} : M(γ) → N(γ) such that the family \overline{τ}_{γ} := (id_{γ}, τ_{γ}) is a natural transformation from \overline{M} to \overline{N}, i.e. for every p : γ → γ′ the following diagram commutes

[figure: \overline{M}(γ); \overline{M}(p); \overline{M}(γ′); \overline{N}(γ); ^{\overline{τ}^{γ}}; \overline{N}(p); \overline{N}(γ′); ^{\overline{τ} ′γ}]

Now suppose that A ∈ Ty(Γ) and B ∈ Ty(Γ.A). We wish to define a family Π_{LF}(A, B) ∈ Ty(Γ) together with additional structure to interpret application and abstraction. In order to avoid lengthy and rather unreadable calculations we will only give the definitions and leave the straightforward verifications to the reader.

If γ ∈ Γ let B_{γ} ∈ Ty(A(γ)) be the family of groupoids over the groupoid A(γ) given by

\begin{matrix}B_{γ}(a) = B(γ, a) \\ B_{γ}(p)( ) = (id_{γ}, p) · \end{matrix}

Notice that B_{γ} = B{γ̂} where γ̂ : A(γ) → Γ.A is the functor sending a to (γ, a) and p : a → a′ to (id_{γ}, p).

Now we put

Π_{LF}(A, B)(γ) = Tm(B_{γ}) considered as a groupoid

If p : γ → γ′ and M ∈ Tm(B_{γ}) then (p · M) ∈ Tm(B′_{γ}) is given by

\begin{matrix}(p · M)(a ∈ A(γ′)) = (p, id ) · M(p^{−1} · a) \\ (p · M)(q : a → a′) = (p, id ) · M(p^{−1} · q) \end{matrix}

If M, M′ ∈ Tm(B_{γ}) and τ : M → M′ is a natural transformation then p · τ : p · M → p · M′ is defined by

(p · τ)_{a} = (p, id ) · τ_{p^{−1} · a}

for a ∈ A(γ′).

4.6.1 Abstraction and application

Suppose that M ∈ Tm(B). We define its abstraction λ_{A,B}(M) ∈ Tm(Π_{LF}(A, B)) on objects by

\begin{matrix}λ_{A,B}(M)(γ)(a) = M(γ, a) \\ λ_{A,B}(M)(γ)(q) = M(id_{γ}, q) \end{matrix}

If p : γ → γ′ then we need a natural transformation

λ_{A,B}(M)(p) : p · λ_{A,B}(M)(γ) → λ_{A,B}(M)(γ′)

At object a ∈ A(γ′) it is given by M(p, id_{a}).

Conversely, if M ∈ Tm(Π(A, B)) we define a dependent object λ_{A,B}^{−1} ∈ Tm(B). Its object part is given by

λ_{A,B}^{−1}(M)(γ, a) = M(γ)(a)

For the morphism part assume p : γ → γ′ and q : p · a → a′. We define

λ_{A,B}^{−1}(M)(p, q) = M(γ′)(q) ∘ (id_{γ′}, q) · M(p)_{p · a}

We claim that

λ_{A,B}^{−1}(M)(p, q) : (p, q) · λ_{A,B}^{−1}(M)(γ, a) → λ_{A,B}^{−1}(M)(γ′, a′)

as required. To see this, first note that

M(γ′)(q) : (id_{γ′}, q) · M′(γ′)(p · a) → M′(γ′)(a′)

because q : p · a → a′. On the other hand M(p) : p · M(γ) → M(γ′), thus

M(p)_{p · a} : (p, id_{a′}) · M(γ)(a) → M′(γ′)(p · a)

as p^{−1} · p · a = a. The claim follows by (id_{γ′}, q) ∘ (p, id_{a′}) = (p, q).

Note that we can define application of M ∈ Tm(Π(A, B)) to N ∈ Tm(A) as λ_{A,B}^{−1}(M)\{\overline{N}\}.

Rather than defining an object of a family Π_{LF}(A, B) we will often define an object of B instead. This will be referred to as “currying”.

4.7 The universe of sets

Let V be a universe in the metalanguage which is closed under dependent function space, dependent sum, and inductive definitions. If our metalanguage is chosen to be axiomatic set theory such universe may be chosen either as a Grothendieck universe (Mac Lane 1971) or V_{κ} for κ an inaccessible cardinal (Luo 1994). If we use extensional Martin-Löf type theory as a metalanguage then V will be a type-theroetic universe with the required closure properties.

Call a groupoid Γ V-small, or small for short, if both its collection of objects and its homsets lie in V. Let us write Gpd for the groupoid which has as objects the small groupoids and only isomorphisms of groupoids as morphisms. The (non-full) inclusion from Gpd to GPD defines a family El ∈ Ty(Gpd).

The groupoid Gpd together with its associated family El serves as the interpretation of the type Set and its associated “invisible” El operator. Notice that, if A : Γ → Gpd then El{A} is actually equal to A. Therefore, it is appropriate to introduce the notation Se(Γ) for the homset Γ → Gpd where Se(Γ) ⊂ Ty(Γ).

4.8 Interpretation of the syntax

The structure exhibited so far is sufficient to interpret the Logical Framework, i.e. the dependent function spaces and the universe Set. This means that we have a unique compositional assignment [[−]] which maps

• a well-formed contexts Γ to a groupoid [[Γ]],

• a type A [Γ] to a family of groupoids [[A [Γ]]] ∈ Ty([[Γ]]),

• an object a : A [Γ] to a dependent object [[a : A [Γ]]] ∈ Tm(A [Γ]),

in such a way that derivable equality judgements are validated. More explicitly, this means that

• [[A [Γ]]] = [[A′ [Γ]]], whenever A = A′ [Γ] is derivable,

• [[a : A [Γ]]] = [[a′ : A [Γ]]], whenever a = a′ : A [Γ].

Notice that if A : Set [Γ] then we have [[A : Set [Γ]]] ∈ Se([[Γ]]) by compositionality. The same goes for dependent function spaces which are interpreted by Π_{LF}( , ,).

In order to extend this interpretation to a hierarchically^{2} structured equational theory such as in particular Martin-Löf set theory we have to assign to each constant of type A an element of [[A]] in such a way that the required definitional equalities are validated.

In defining these semantic constants we will use type-theoretic syntax to denote semantic entities, thereby omitting semantic brackets.

4.9 Dependent function spaces and sums

Since the dependent function space of a small family of groupoids over a small groupoid is again small, we immediately obtain an interpretation of Π-sets.

To interpret Σ-sets we need an element

Σ : (A: Set)(B: (a: A)Set)Set

By currying, this amounts to defining a small family over the groupoid Γ := [A: Set, B: (a: A)Set]. We will use Γ as a black box and only use the fact that its two components arise as small families A ∈ Se(Γ) and B ∈ Se(Γ.A) by projection.

2The type of a constant may depend on previously declared constants.

We have to define a small family Σ(A, B) ∈ Se(Γ). If γ ∈ Γ let B_{γ} ∈ Se(A(γ)) be defined as in Section 4.6.

The family Σ(A, B) ∈ Ty(Γ) is now defined as follows.

\begin{matrix}Σ(A, B)(γ) = A(γ).B_{γ} \\ p ·(a, b) = (p · a , (p, id_{p · a}) · b) \end{matrix}

In order to give meaning to pairing and elimination it is sufficient, albeit not necessary, to exhibit an isomorphism between Γ.Σ(A, B) and Γ.A.B. But these two groupoids are identical up to restructuring of parentheses. That is to say the isomorphism sends (γ, a, b) to (γ, (a, b)) and vice versa and similarly for morphisms.

4.10 Identity sets

Before embarking on the precise definition of identity sets we motivate the main idea by assuming that the ambient context is empty. So let A be a groupoid. The interpretation of Id(A) arises as the family I_{A} ∈ Ty(A × A) as defined in 4.2.2. Recall that I_{A}(a_{1}, a_{2}) = A(a_{1}, a_{2}) and I_{A}(q_{1}, q_{2})(s) = q_{2} ∘ s ∘ q_{1}^{−1}. Reflexivity is interpreted as the dependent object which sends a ∈ A to refl(a) := id_{a} ∈ A(a, a). If q : a → a′, then

I_{A}(q, q)(refl(a)) = q ∘ id_{a} ∘ q^{−1} = id_{a′} = refl(a′)

Therefore, refl is indeed a dependent object of the family I_{A}(a, a) [a: A]. For identity elimination let C be a family over the groupoid

Θ := [a_{1}, a_{2}: A, s: I_{A}(a_{1}, a_{2})]

The groupoid Θ has as objects triples (a_{1}, a_{2}, s) where s ∈ A(a_{1}, a_{2}). A Θmorphism from (a_{1}, a_{2}, s) to (a′_{1}, a′_{2}, s′) amounts to a pair (q_{1}, q_{2}) where q_{i} : a_{i} → a′_{i} with I_{A}(q_{1}, q_{2})(s) = s′, i.e. q_{2} ∘ s = s′ ∘ q_{1}. Notice that, therefore, Θ is (isomorphic to) the arrow category A^{→}.

In order to interpret J(A, C) one has to provide a uniform way of extending an object d of (a: A)C(a, a, refl(a)) to a dependent object J(A, C, d) of C such that J(A, C, d)(a, a, refl(a)) = d(a). The key to the interpretation of J(A, C) is the observation that for any object (a_{1}, a_{2}, s) we have

(id_{a_{1}}, s) : (a_{1}, a_{1}, id_{a_{1}}) → (a_{1}, a_{2}, s)

because

[figure: a_{1}; id_{a_{1}}; a_{1}; a_{1}; ^{id^{a_{1}}}; s; a_{2}; s]

commutes. Therefore, we can put

J(A, C, d)(a_{1}, a_{2}, s) = (id_{a_{1}}, s) · d(a_{1})

The morphism part of J is defined analogously.

For those familiar with fibrations we remark that the extension J(A, C, d) depends crucially on the morphism part of C, i.e. on the choice of a splitting of C when viewed as a fibration of groupoids. Therefore, it seems unlikely that it can be characterised by a universal property.

4.10.1 The identity set former

To interpret identity sets in full generality we need an element

Id ∈ Tm((A: Set)(a, a′: A)Set)

By currying this amounts to defining a small family over the groupoid [A: Set, a_{1}: A, a_{2}: A]. This groupoid has as objects triples (A, a_{1}, a_{2}) where A is a small groupoid and a_{1}, a_{2} are objects of A. A morphism from (A, a_{1}, a_{2}) to (A′, a′_{1}, a′_{2}) is a triple (p, q_{1}, q_{2}) where p : A → A′ is an isomorphism of groupoids, i.e. p ∈ Gpd(A, A′), and q_{i} : p(a_{i}) → a′_{i} in A′. Note that El(p)(a_{i}) = p(a_{i}) thus permitting us to write also p(x) instead of p · x.

The family Id over [A: Set, a_{1}: A, a_{2}: A] is now given by

\begin{matrix}Id(A, a_{1}, a_{2}) = △(A(a_{1}, a_{2})) \\ Id(p, q_{1}, q_{2})(s) = q_{2} ∘ p(s) ∘ q_{1}^{−1} ∈ Id(A′, a′_{1}, a′_{2}) \end{matrix}

where p : A → A′ and q_{i} ∈ A′(p(a_{i}), a′_{i}) and s ∈ Id(A, a_{1}, a_{2}) = A(a_{1}, a_{2}).

4.10.2 Reflexivity

We define a dependent object

refl : (A: Set)(a: A)Id(A, a, a))

Again, by currying this amounts to giving a dependent object of the family Id_{diag} := Id(A, a) [A: Set, a: A] (over the groupoid [A: Set, a: A]). Let us make the involved groupoids explicit. The groupoid [A: Set, a: A] has as objects pairs (A, a) where A is a small groupoid and a ∈ A. A morphism from (A, a) to (A′, a′) is a pair (p, q) where p : A → A′ and q ∈ A′(p(a), a′). Furthermore, we have Id_{diag}(A, a) = △(A(a, a)) and if s ∈ A(a, a) then (p, q) · s = q ∘ p(s) ∘ q^{−1}.

The object part of refl is now given by

refl(A, a) = id_{a} ∈ A(a, a)

Now since Id_{diag} is discrete the definition of the morphism part of refl reduces to checking that

q ∘ p(refl(A, a)) ∘ q^{−1} = refl(A′, a′)

This in turn is immediate by by functoriality of p and the fact that q^{−1} is an inverse of q.

4.10.3 Identity elimination

We seek a global element of the following groupoid.

(A: Set)(C: (a_{1}, a_{2}: A, s: Id(A, a_{1}, a_{2}))Set)(d : (a: A)C(a, a, refl(A, a)))
(a_{1}, a_{2}: A)(s: Id(A, a_{1}, a_{2}))C(a_{1}, a_{2}, s)

By currying this amounts to defining a dependent object

J ∈ Tm(C(a_{1}, a_{2}, s) [Γ, a_{1}: A, a_{2}: A, s: Id(A, a_{1}, a_{2})])

where

Γ = [A : Set, C : (a_{1}, a_{2}: A, s: Id(A, a_{1}, a_{2}))Set, d : (a: A)C(a, a, refl(A, a))]

and A, C, d refer to the respective components of Γ. Note that we have A ∈ Se(Γ), a family C ∈ Se([Γ, a_{1}, a_{2}: A, s: Id(A, a_{1}, a_{2})]), and a dependent object d of C(a, a, refl(A, a)) [Γ, a: A] via projection (and uncurrying in the case of d).

The object part of J is given as follows. Let u = (γ, a_{1}, a_{2}, s) be an object of [Γ, a_{1}, a_{2}: A, s: Id(A, a_{1}, a_{2})]. Put

f(u) := (id_{γ}, id_{a_{1}}, s, ⋆)

Notice that

f(u) : (γ, a_{1}, a_{1}, refl(A, a_{1})) → (γ, a_{1}, a_{2}, s)

as (s, id_{a_{1}}) · refl(A, a_{1}) = s ∘ refl(A, a_{1}) ∘ id_{a_{1}}^{−1} = s. Now recall that d(γ, a_{1}) ∈ C(γ, a_{1}, a_{1}, refl(A, a_{1})); so we are led to define

J(u) := f(u) · d(γ, a_{1}) ∈ C(γ, a_{1}, a_{2}, s)

We come to the morphism part. Let u = (γ, a_{1}, a_{2}, s) and u′ = (γ′, a′_{1}, a′_{2}, s′) be objects of [Γ, a_{1}, a_{2}: A, s: Id(A, a_{1}, a_{2})] and let h = (p, q_{1}, q_{2}, ⋆) : u → u′. In other words p : γ → γ′ and q_{i} : p ·(a_{i}) → a′_{i} and

q_{2} ∘ (p · s) = s′ ∘ q_{1}  (1)

We have to define a morphism J(h) : h · J(u) → J(u′) in C(u′). We claim that

J(h) := f(u′) · d(p, q_{1})

has the required property. To see this, first observe that (p, q_{1}) : (γ, a_{1}) → (γ′, a′_{1}) and therefore

d(p, q_{1}) : (p, q_{1}, q_{1}, ⋆) · d(γ, a_{1}) → d(γ′, a′_{1})  (2)

as d ∈ Tm(C(a, a, refl(A, a)) [Γ, a: A]). Notice that

(p, q_{1}, q_{1}, ⋆) : (γ, a_{1}, a_{1}, refl(a_{1})) → (γ′, a′_{1}, a′_{1}, refl(a_{1})′)

Applying the operation f(u′) · to (2) and using functoriality yields

f(u′) · d(p, q_{1}) : (f(u′) ∘ (p, q_{1}, q_{1}, ⋆)) · d(γ, a_{1}) → f(u′) · d(γ′, a′_{1})

Now we calculate as follows.

f(u′) ∘ (p, q_{1}, q_{1}, ⋆)
= (id_{γ′}, id_{a′_{1}}, s′, ⋆) ∘ (p, q_{1}, q_{1}, ⋆)
= (p, q_{1}, s′ ∘ q_{1}, ⋆)
= (p, q_{1}, q_{2} ∘ (p · s), ⋆)  by Eqn. 1
= (p, q_{1}, q_{2}, ⋆) ∘ (id_{γ}, id_{a_{1}}, s, ⋆)  since p · id_{a_{1}} = id_{a′_{1}}
= h ∘ f(u)

So J(h) : (h ∘ f(u)) · d(γ, a_{1}) → f(u′) · d(γ′, a′_{1}) and therefore J(h) : h · J(u) → J(u′) as required. The verification of the functor laws for J is tedious but straightforward.

Notice that for all γ ∈ Γ and a ∈ A(γ) we have

f(γ, a, a, refl(A, a)) = (id_{γ}, id_{a}, id_{a}, ⋆)

Therefore

J(γ, a, a, refl(A, a)) = f(γ, a, a, refl(A, a)) · d(γ, a) = d(γ, a)

and

J(p, q, q, ⋆) = f(γ′, a′, a′, refl(A, a′)) · d(p, q) = d(p, q)

whenever (p, q) : (γ, a) → (γ′, a′). This establishes the validity of the definitional equality required for J.

4.11 Other set formers

The natural numbers N ∈ Se([]) are given as the discrete groupoid △(ℕ) over the set of natural numbers. We omit the definition of the associated operations. The disjoint union set A + B is interpreted as the co-product of groupoids, which is constructed as the disjoint union of the underlying sets of objects and morphisms.

In a similar way, we can interpret lists, trees, unit set, empty set, and other datatypes.

4.12 Universes

Let V be a meta-theoretic universe contained in V. We write Gpd(V) for the groupoid of V -small groupoids with isomorphisms as morphisms.

Provided V has appropriate meta-theoretic closure properties the groupoid Gpd(V) can serve as interpretation of a universe closed under the usual set forming operations.

We call a meta-theoretic universe V impredicative, if it is closed under impredicative universal quantification, i.e. for A ∈ V and B : A → V the dependent function space Π_{a∈A}B(a) is in V. Of course, non-trivial instances of such V are possible only in an intuitionistic metatheory such as an extensional variant of Luo’s ECC (Luo 1994) whose consistency is established by various realizability models.

If V is impredicative (and has the usual closure properties) then Gpd(V) is closed under impredicative quantification as well. That is to say, if A ∈ V and B : A → Gpd(V) then Π_{LF}(A, B) ∈ Gpd(V). This is immediate from the definition of dependent function spaces in the groupoid model.

For subsequent applications it is useful to have universes of small discrete groupoids available. We write Gpd_{△}(V) for the groupoid consisting of V -small discrete groupoids with isomorphisms (or rather bijections) as morphisms. Due to the fact that discrete groupoids are closed under all set forming operations so will be a universe of the form Gpd_{△}(V). Moreover, since identity sets (even of non-discrete groupoids) are discrete, the family of groupoids Id(A) lives in Gpd_{△}(A) provided the groupoid A has V -small homsets.

Of particular interest is the situation where V is impredicative and Set is confined to groupoids with V -small homsets. Due to impredicativity of V this interpretation of Set is still closed under dependent function space as well as the remaining set forming operations. Now, Gpd(V) and Gpd_{△}(V) are impredicative universes (still contained in Set) which moreover contain all identity sets. We thus obtain an interpretation of impredicative higher-order logic in which propositional equality is proof-relevant.

Notice, that since universes of the above form are not discrete they cannot be contained in a universe of the form Gpd_{△}(V). Nevertheless, if V′ is a metatheoretic universe contained in V then Gpd_{△}(V) contains the discrete groupoid consisting of V′-small groupoids. Universes obtained in this way are still closed under all set formers, but do not contain identity sets of non-discrete groupoids.

We have not checked whether these universes can be suffiently narrowed down so as to validate universe elimination, cf. Ch. 14 of (Nordström, Petersson, and Smith 1990), but we do not see any principle obstacle.

5 Applications and extension

In this section we will exploit the benefits of the model construction carried out. We derive the promised independence results and investigate some extensions validated by the groupoid model, in particular a set of axioms expressing that equality on certain universes is isomorphism. These extension are put to use in a new type-theoretic formalisation of basic category theory in which isomorphic objects are propositionally equal.

5.1 Independence of UIP

Since for a groupoid A the identity set Id(A, a_{1}, a_{2}) is interpreted as △(A(a_{1}, a_{2})) it will contain more than one object if there is more than one A-morphism from a_{1} to a_{2}. Due to discreteness of identity sets these objects are then not even propositionally equal as propositional and definitional equality coincide for discrete groupoids. More formally, we have the following theorem.

Theorem 5.1 The type UIP is empty.

Proof. Suppose that u ∈ Tm(UIP). Let A be the group ℤ_{2} viewed as a oneobject groupoid. That is to say, we have a single object ⋆ ∈ A and two distinct morphisms id_{⋆}, p ∈ A(⋆, ⋆) where p ∘ p = id_{⋆}. Then u(A, ⋆, ⋆, p, id_{⋆}) would be an element of Id(Id(A, ⋆, ⋆), p, id_{⋆}). However, the latter set is empty as p ≠ id_{⋆} and identity sets are discrete. □

By soundness of the interpretation the following is now immediate.

Corollary 5.2 There is no syntactically definable closed term of type UIP.

5.1.1 Non-definability of K

As UIP can be proved using the eliminator K for the family Id(A, a, a) [a: A], as given in Section 3.3 it follows that the latter cannot be interpreted in the groupoid model. It is, however, instructive to see directly, why an attempt of interpreting K in the same way as J fails. Let A be a groupoid and C ∈ Se([a: A, s: Id(A, a, a)]) and d : (a: A)C(a, refl(a)). In order to construct a dependent object of C extending d in the same way as we did in the case of J we would have to come up with a morphism in [a: A, s: Id(A, a, a)] from (a, refl(a)) to (a, s) for arbitrary s : a → a. Now such a morphism would amount to a morphism q : a → a satisfying s ∘q = q ∘refl(a) = q. But this implies s = refl(a). So no such morphism exists if s ≠ refl(a).

That an interpretation of K cannot be achieved in any other way either can be seen as follows. Let A be a groupoid with an object a_{0} ∈ A such that A(a_{0}, a_{0}) contains a non-identity morphism p_{0}. Let C ∈ Se([a: A, Id(a, a)]) be the family of discrete groupoids given by

C(a, p) = △{⋆ | p = id_{a}}

So C(a, p) is empty for p ≠ id_{a}. To see that this is a family of groupoids assume that we have a morphism (q, ⋆) : (a, p) → (a′, p′), i.e. q : a → a′ and p′ ∘q = q ∘p. So p′ = id_{a′} iff p = id_{a}. Now d(a) := ⋆ is an object of (a: A)C(a, refl(a)). However, Tm(C) is empty as C(a_{0}, p_{0}) is empty.

5.1.2 Non-definability of cong snd

Finally, let us look at the congruence property cong snd. If A is a groupoid and B ∈ Se(A) and a : A and b, b′ : B(a) then

Id(Σ(A, B), ⟨a, b⟩ , ⟨a, b′⟩) = △{(p, q) | p : a → a, q : p · b → b′}

whereas

Id(B(a), b, b′) = △{q | q : b → b′}

So the two groupoids are different and one can easily construct a situation in which the first one is inhabited and the second one is empty.

5.2 Canonicity of identity types

Unlike Π-sets with η-equality or extensional identity sets, the intensional identity sets are not defined by a universal property. Therefore, it is natural to ask how interpretations of identity sets in the groupoid model look like in general.

To answer this question, assume for the moment that we enrich our type theory by another set former Id′ : (A: Set)A → A → Set together with appropriately typed constants refl′ and J′ satisfying the corresponding definitional equalities. Then using J and J′ one can exhibit terms

i : (A: Set)(a_{1}, a_{2}: A)Id(A, a_{1}, a_{2}) → Id′(A, a_{1}, a_{2})
j : (A: Set)(a_{1}, a_{2}: A)Id′(A, a_{1}, a_{2}) → Id(A, a_{1}, a_{2})

in such a way that, moroever, the following two types are inhabited

(A: Set)(a_{1}, a_{2}: A)(s: Id(A, a_{1}, a_{2}))Id(j(i(s)) , s)
(A: Set)(a_{1}, a_{2}: A)(s′: Id′(A, a_{1}, a_{2}))Id(i(j(s′)) , s′)

It follows that UIP holds with respect to Id′ if and only if it holds w.r.t. Id because the property of having at most one element is stable under propositional isomorphism. It follows that no interpretation of identity sets satisfying UIP is possible in the groupoid model, thus in particular extensional identity sets cannot be interpreted.

A more refined analysis shows that i and j establish an equivalence in the category-theoretic sense and therefore any possible interpretation of the identity set Id(A, a_{1}, a_{2}) must be a posetal groupoid whose connected components are in a 1-1 correspondence with A(a_{1}, a_{2}).

5.3 Functional extensionality

Despite the intensional character of the groupoid model propositional equality on function spaces is pointwise in the sense that the following type is inhabited in the model.

Fun Ext =^{def} (A: Set)(B: (a: A)Set)(f, g: Π(A, B))
((a: A)Id(B(a), f(a), g(a))) → Id(f, g)

To see this, let Γ denote the groupoid [A: Set, B: (a: A)Set , f, g: Π(A, B)] and let PE ∈ Se(Γ) denote the family (a: A)Id(B(a), f(a), g(a)).

Let γ ∈ Γ. The groupoid Id(f, g)(γ) is the discrete groupoid with objects the natural transformations in the sense of Section 4.6. More precisely, an object of Id(f, g)(γ) is an assignment τ mapping objects a ∈ A(γ) to B(γ, a)-morphisms τ_{a} : f(γ)(a) → g(γ)(a) such that whenever q : a → a′ then the following diagram commutes.

f(γ)(a)  \overline{τ_{a}} g(γ)(a)

(id , q) · f(γ)(a) \overline{\begin{matrix}(id , q) · τ_{a} \\  \end{matrix}}(id , q) · g(γ)(a)

[figure: f(γ)(a′); f(γ)(q); τ_{a′}; g(γ)(a′); g(γ)(q)]

Now let M be an object of PE(γ). By definition of dependent function space M(a) is a morphism from f(γ)(a) to g(γ)(a) for every a ∈ A(γ). Furthermore, if q : a → a′ then

M(q) : (id , q) · M(a) → M(a′)  (3)

where · refers to the identity set Id(f(a), g(a)). By discreteness of identity sets (3) translates into the following diagram.

f(γ)(a)  \overline{M(a)} g(γ)(a)

(id , q) · f(γ)(a) \overline{\begin{matrix}(id , q) · M(a) \\  \end{matrix}}(id , q) · g(γ)(a)

[figure: f(γ)(a′); f(γ)(q); M(a′); g(γ)(a′); g(γ)(q)]

This means that the objects of Id(f, g)(γ) and PE(γ) are the same! Being a dependent function space of a discrete family, PE is discrete itself. So Id(f, g)(γ) and PE(γ) are isomorphic. One can also show that this isomorphism is natural in γ thus establishing an isomorphism between the families PE and Id(f, g). A more refined analysis shows that one direction of this isomorphism arises as the interpretation of the following proof that equal functions are pointwise equal.

app resp =^{def} [A: Set][B: (a: A)Set][f, g: Π(A, B)][s: Id(f, g)]

[a: A]resp([h: Π(A, B)]h(a), s)

: (A: Set)(B: (a: A)Set)(f, g: Π(A, B))Id(f, g) → (a: A)Id(f(a), g(a))

This allows us to interpret the following extension of Martin-Löf’s type theory.

fun ext : Fun Ext

fun ext ax1 : (A: Set)(B: (a: A)Set)(f, g: Π(A, B)) (s: Id(f, g))Id(s, fun ext(app resp(s)))

fun ext ax2 : (A: Set)(B: (a: A)Set)(f, g: Π(A, B))

(s: (a: A)Id(f(a), g(a)))Id(s, app resp(fun ext(s)))

The special case of fun ext ax1 where s is an instance of reflexivity was proposed by Turner (Turner 1989) as a possible axiomatisation of functional extensionality. It is easy to see that this special case is equivalent to the general fun ext ax1 using J. Apparently, fun ext ax2 is independent of fun ext ax1 (and Turner’s axiom). Note that our two axioms determine the postulated object fun ext uniquely up to propositional equality. Obviously, the axioms fun ext ax1/2 are derivable from UIP.

A potential application of functional extensionality is that it allows one to derive UIP(Π(A, B)) from (a: A)UIP(B(a)). Assuming fun ext alone, does not seem to suffice for that purpose.

Notice that functional extensionality allows us to express an identity set of the form Id(Π(A, B)) in terms of identity sets of the form Id(B(a)). A similar decomposition is possible for Σ-sets without any extension to the syntax. Indeed, using Σ-elimination we can establish a canonical isomorphism between Id(Σ(A, B), ⟨u_{1}, u_{2}⟩, ⟨v_{1}, v_{2}⟩) and

Σ([p: Id(A, u_{1}, v_{1})]Id(B(v_{2}), subst(p, u_{2}), v_{2})

Analogously, we can decompose identity sets at disjoint unions and natural numbers.

5.4 Universe extensionality

In this section we want to make an extension of type theory taking account of the fact that propositional equality on a universe is isomorphism. To make this more precise we need some notation. We write Iso(A, B) for the set

Σ([f: A → B]Σ([g: B → A]Id(g ∘ f, id ) × Id(f ∘ g, id ))

where composition (∘) and identities (id ) are defined as usual in terms of abstraction and application. If h : Iso(A, B) we abbreviate its first component by h and its second component by h^{−1}. Conversely, if f : A → B and it is clear from the context that f has an inverse in the sense propositional equality then we may write f : Iso(A, B).

Now let U be a universe of discrete groupoids, i.e. of the form Gpd_{△}(V). It is then clear that if A, B : U then the interpretations of Iso(A, B) and

Id(U , A, B) are isomorphic. One direction of the isomorphism is syntactically definable as

id iso =^{def} [A, B: U ][s: Id(A, B)]subst([X: U ]Iso(A, X) , s, id_{A})
: (A, B: U )Id(A, B) → Iso(A, B)

Notice that Iso(A, B) and Id(A, B) are not isomorphic if U = Gpd(V) because then Iso(A, B) is in one-to-one correspondence with equivalences between A and B. Thus Iso(A, B) may be inhabited even if A and B are not isomorphic.

Like in the case of functional extensionality we can now syntactically postulate an inverse to the function id iso:

iso id : (A, B: U )Iso(A, B) → Id(A, B)

iso id ax1 : (A, B: U )(s: Id(A, B))Id(s, iso id(id iso(s)))

iso id ax2 : (A, B: U )(s: Iso(A, B))Id(s, id iso(iso id(s)))

By analogy to functional extensionality we refer to this extension by universe extensionality.

We remark that universe extensionality is inconsistent with UIP(U ) if U contains the natural numbers. This is so because the set Iso(N, N) contains two different definable elements f and g. UIP together with the above constants would identify f and g and therefore two different natural numbers.

5.5 A new formalisation of category theory

An application of the above extension is a new formalisation of category theory where isomorphic objects are propositionally equal. Let U be a universe of discrete groupoids. We reflect this syntactically by assuming (A: U )UIP(A).

A category with isomorphism as equality then consists of the following data.

• a set Ob : Set of objects,

• a family of sets Mor : Ob → Ob → U of morphisms,

• objects id and comp of the obvious types corresponding to identity and composition,

• proofs of the traditional axioms stated in terms of propositional equality,

• a proof that for each A, B: Ob the sets Id(Ob, A, B) and Iso(A, B) are canonically isomorphic.

This definition deserves some explanation. The set Iso(A, B) for A, B: Ob is defined analogously to Iso for members of a universe. More precisely, Iso(A, B) is

Σ[f: Mor(A, B)]Σ[g: Mor(B, A)]
Id(comp(g, f), id(A)) × Id(comp(f, g), id(B))

This set being “canonically isomorphic” to Id(A, B) means that the canonical function Id(A, B) → Iso(A, B) obtained by applying subst to id(A) is bijective.

The fact that the homsets Mor(A, B) are discrete enables us to do without further axioms qualifying the behaviour of the assumed proofs of the category equations. In other words, there is only one reason for morphisms to be equal.

If we want to consider the collections of categories as objects of Set then we have to restrict Ob to a member of a certain not necessarily discrete universe.

Of course, this formalisation of categories does not per se require universe extensionality. The point is that universe extensionality is necessary for organising U itself into a category with isomorphism as equality.

More precisely, we can define a category where Ob =^{def} U and Mor(A, B) =^{def} A → B.

Furthermore, using functional extensionality in an essential way, we can show that categories with isomorphism as equality are closed under formation of functor categories. The crucial point here is to establish a one-to-one correspondence between between natural isomorphism between two functors F and G (between categories C and D) and proofs that F and G are equal. This is achieved by decomposing the set Id(FUNC(C, D), F, G) according to the rules set out at the end of Section 5.3. Here the set of functors FUNC(C, D) is defined as usual by grouping together object and morphism part as an object of a Σ-set.

The components of a natural isomorphism now correspond to a proof that the object parts of F and G are pointwise equal, thus equal by functional extensionality. The naturality condition, on the other hand, is required for the proof that the two morphism parts are propositionally equal. The details are messy, but have been machine-checked using a proof assistant (Lego).

We emphasise that the abovementioned decomposition of Id(F, G) suggests the usual definition of isomorphism between functors. It would be interesting to see whether this analogy can be exploited for finding appropriate notions of isomorphism for other mathematical structures (e.g. models of typed lambda calculus).

Notice that, obviously, UIP(FUNC(C, D)) is not valid as there is in general more than one natural isomorphism between any two functors. This implies that categories and functors do not form a category with equality as isomorphism since its homsets are not discrete. Of course, categories and functors still can be organised into a category in the traditional sense. However, it might be interesting to view equivalent categories as propositionally equal. This, however, would require “2-level groupoids” in which we have morphisms between morphisms and accordingly the identity sets are not necessarily discrete. We do not know whether such structures (or even infinite-level generalisations thereof) can be sensibly organised into a model of type theory.

A Syntax of type theory

A.1 General rules

\overline{[] ctxt} Emp

\frac{A type [Γ]}{Γ, x: A ctxt} Compr

\frac{Γ, x: A, Δ ctxt}{x : A [Γ, x: A, Δ]} Var

In rule Compr x is a fresh variable.

Rules expressing that definitional equality is a congruence relation with respect to all subsequent type and term forming operations.

A.2 Rules for the Logical Framework

\frac{A type [Γ] B type [Γ, x: A]}{(x: A)B type [Γ]} Fun

\frac{A type [Γ] B type [Γ, x: A] t : B [Γ, x: A]}{[x: A]t : (x: A)B [Γ]} lam

\frac{A type [Γ] B type [Γ, x: A] t : (x: A)B [Γ] s : A [Γ]}{t(s) : B[x:=s] [Γ]} app

\frac{A type [Γ] B type [Γ, x: A] t : B [Γ, x: A] s : A [Γ]}{([x: A]t)(s) = t[x:=s] : B[x:=s] [Γ]} β

\frac{A type [Γ] B type [Γ, x: A] t : (x: A)B [Γ]}{[x: A] t(x) = t : (x: A)B [Γ]} η

\frac{Γ ctxt}{Set type [Γ]} Set

\frac{A : Set [Γ]}{El(A) type [Γ]} El

We henceforth omit the El-operator and use the conventions on abstraction, application, and omission of redundant arguments set out in Section 2. We abbreviate (x: A)B by A → B if x does not occur in B.

A.3 Martin-Löf’s set theory

Martin-Löf’s set theory is defined as the extension of the Logical Framework by the following constants and definitional equations understood in every valid context. The definitional equalities hold under the proviso that their components are well-typed.

A.4 Π-sets

Π : (A: Set)(A → Set) → Set
fun : (A: Set)(B: A → Set)((a: A)B(a)) → Π(A, B)
app : (A: Set)(B: A → Set)(Π(A, B)) → (a: A)B(a)
app(fun(b), a) = b(a) : B(a)
fun([x: A]app(t, x)) = t : Π(A, B)

Alternatively, we can replace app by the so-called funsplit operator (Nordström, Petersson, and Smith 1990). Then the second η-like equality only holds propositionally.

We take the freedom of writing f(a) for app(f, a).

A.5 Σ-sets

Σ : (A: Set)(A → Set) → Set
pair : (A: Set)(B: A → Set)(a: A)B(a) → Σ(A, B)
E : (A: Set)(B: A → Set)(C : Σ(A, B) → Set)
((a: A)(b: B(a))C(pair(a, b))) → (c: Σ(A, B))C(c)
E(d, pair(a, b)) = d(a, b) : C(pair(a, b))

When A, B : Set then we abbreviate Σ([x: A]B) by A × B. We also write ⟨a, b⟩ for pair(a, b).

A.6 Identity sets

Id : (A: Set)A → A → Set
refl : (A: Set)(a: A)Id(A, a, a)
J : (A: Set)(C: (a_{1}, a_{2}: A)Id(A, a_{1}, a_{2}) → Set)
((a: A)C(a, a, refl(A, a))) → (a_{1}, a_{2}: A)(s: Id(A, a_{1}, a_{2}))C(a_{1}, a_{2}, s)
J(d, refl(a)) = d(a) : C(refl(a))

A.7 Natural numbers and disjoint unions

N : Set 0 : N succ : N → N

R : (C : N → Set)C(0) → ((n: N)C(n) → C(succ(n))) → (n: N)C(n)

R(d, e, 0) = d : C(0) R(d, e, succ(n)) = e(n, R(d, e, n)) : C(succ(n))

+ : Set → Set → Set i : (A, B: Set)A → A + B j : (A, B: Set)B → A + B

D : (A, B: Set)(C: (A + B) → Set)

((a: A)C(i(a))) → ((b: B)C(j(b))) → (c: A + B)C(c) D(d, e, i(a)) = d(a) : C(i(a)) D(d, e, j(b)) = e(b) : C(j(b))

A.8 Universes

A universe U in Set is defined by two constants U : Set and T : U → Set

Closure properties of the universe under certain type and term formers are expressed by reintroducing them with Set replaced by U . If the desired type former is available for Set as well then it suffices to reintroduce the type former for U and relate it to the corresponding type former on the level of Set by an appropriate equality axiom for T. The associated term formers can then be inherited from Set. For example, closure under impredicative universal quantification is defined by

Π̂ : (A: Set)(A → U ) → U

f̂un : (A: Set)(B: A → U )((a: A)T (B(a))) → T (Π̂(B)) âpp : (A: Set)(B: A → U )(t: T (Π̂(B))) → (a: A)T (B(a)) β and η equations

If we have Π-sets then f̂un and âpp together with their equations can be replaced by the single set equation

T (Π̂(A, B)) = Π(A, [a: A]T (B(a)))

References

Altenkirch, T. (1992, January). An open question concerning inductive equality. E-mail message to the Edinburgh LEGO club.

Altenkirch, T., V. Gaspes, B. Nordström, and B. von Sydow (1994). A User’s Guide to ALF. Sweden: Chalmers University of Technology. Available under ftp://ftp.cs.chalmers.se/pub/users/alti/alf.ps.Z.

Brown, R. (1988). Topology. Ellis Horwood.

Coquand, T. (1992). Pattern matching with dependent types. In Workshop on Logical Frameworks, Båstad. Preliminary Proceedings.

Dybjer, P. (1996). Internal type theory. In Proc. BRA TYPES workshop, Torino, June 1995, Springer LNCS. To appear.

Hedberg, M. (1995). Uniqueness and internal decidability in type theory. Manuscript, Chalmers University, Gothenburg.

Hofmann, M. (199?). Syntax and semantics of dependent types. In P. Dybjer and A. M. Pitts (Eds.), Semantics and Logics of Computation. Cambridge University Press.

Hofmann, M. (1993, July). A model of intensional Martin-Löf type theory in which unicity of identity proofs does not hold. unpublished note, available on email request.

Hofmann, M. (1995). Extensional Concepts in Intensional Type Theory. Ph. D. thesis, Univ. of Edinburgh.

Hofmann, M. and T. Streicher (1994). A groupoid model refutes uniqueness of identity proofs. In Proceedings of the 9th Symposium on Logic in Computer Science (LICS), Paris.

Lamarche, F. (1991(?)). A Proposal about Foundations I. Manuscript.

Luo, Z. (1994). Computation and Reasoning. Oxford University Press.

Mac Lane, S. (1971). Categories for the Working Mathematician. Springer.

Nordström, B., K. Petersson, and J. M. Smith (1990). Programming in Martin-Löf’s Type Theory, An Introduction. Clarendon Press, Oxford.

Per Martin-Löf (1995). Tarskian semantics for type theory. Talk given at the symposium “25 years of constructive type theory”, Venice.

Streicher, T. (1993). Semantical Investigations into Intensional Type Theory. Habilitationsschrift, LMU München.

Turner, D. (1989, May). A new formulation of constructive type theory. In P. Dybjer (Ed.), Proceedings of the Workshop on Programming Logic, pp. 258–294. Programming Methodology Group, Univ. of Göteborg.