A Groupoid Model Refutes Uniqueness of Identity Proofs

Martin Hofmann Dept. of Computer Science, Univ. of Edinburgh, Scotland mxh@dcs.ed.ac.uk

Thomas Streicher Ludwig-Maximilian-Universität, München, Germany streiche@informatik.uni-muenchen.de

March 21, 1994

Abstract

We give a model of intensional Martin-Löf type theory in which there can be more than one proof for a certain equality. This shows that uniqueness of equality proofs is not derivable in the syntax.

1 Motivation and Main Result

When representing logic via the Curry-Howard paradigm of propositions-as-types one is forced to introduce a so-called identity type Id_{A}(a, b) consisting of all proof objects for the proposition “the objects a and b of type A are equal”. In extensional type theory propositional equality Id_{A}(a, b) is identified with judgemental equality a = b : A via the identity reflection rule, which allows to conclude judgemental equality from propositional equality, cf. [4]. Unfortunately, this identification leads to the non-confluence of the rewrite system determining the operational semantics of the term language [8]. Even worse, type-checking and thus proof-checking becomes undecidable.

Therefore — in order to keep the computational meaning of proofs — one has to restrict oneself to intensional constructive type theory where for any type A the identity type is introduced as an inductively defined family of types x : A, y : A ⊢ Id_{A}(x, y) with constructor x : A ⊢ refl_{A}(x) : Id_{A}(x, x) and eliminator J whose meaning is given by the following rules

\begin{matrix}Γ, x : A, y : A, z : Id_{A}(x, y) ⊢ C(x, y, z) \\ Γ, x : A ⊢ d : C(x, x, refl_{A}(x)) \end{matrix}

\begin{matrix}Γ, x : A, y : A, z : Id_{A}(x, y) ⊢ J_{A,C}(d, x, y, z) : C(x, y, z) \\ Γ, x : A ⊢ J_{A,C}(d, x, y, z) = d : C(x, x, refl_{A}(x)) \end{matrix}

Surprisingly enough, the J-eliminator is sufficient for constructing terms refl, symm, trans and subst inhabiting the types corresponding to the propositions expressing reflexivity, symmetry, transitivity and replacement. However, in a proof term the application of the replacement rule is always mentioned and cannot be eliminated in general. This means that in the situation x, y : A , p : Id_{A}(x, y) , b : B(x) we have subst_{A,B}(p, b) : B(y) but not b : B(y) like in extensional type theory. For the definition of these combinators from J see e.g. [6].

Notice the absence of an η-rule for J which would in fact allow to derive the identity reflection rule, cf. [8], and therefore destroy the operational semantics of the term language. A further manifestation of the a priori unexpected strength of the eliminator J is that one can derive proof terms for the types corresponding to the propositions expressing in terms of propositional equality the η-rules for various inductively defined types, cf. [6]. For example we can find an inhabitant of the type

Πp : Σa : A.B(a).Id_{Σx:A.B(x)}(p , ⟨p.1, p.2⟩)

thus “surjective pairing” holds propositionally. Similarly, the type

Πn : N.Id_{N}(n, 0) + Σn′ : N.IdN(n, S(n′))

is inhabited. The intuitive meaning of these η-rules is that “any object of an inductive type is propositionally equal to an object in constructor form”.

The main result of this paper is that a corresponding property does not hold for the identity type itself. Indeed, below in Section 3 we will prove

Theorem 1 There exists a type A in the empty context such that the type

x : A , p, q : Id_{A}(x, x) ⊢ Id_{Id_{A}(x,x)}(p, refl_{A}(x))

is not inhabited.

A similar principle for Id_{A}(x, y) where x and y are not assumed to be necessarily equal is

x : A, y : A, p, q : Id_{A}(x, y) ⊢ Id_{Id_{A}(x,y)}(p, q)

One can show using J that this type is inhabited iff the latter type is. Henceforth we say that the principle UIP (uniqueness of identity proofs) holds for some type A if either of the above types is inhabited for that type. Similarly, we say that UIP holds in a model of type theory, if either of the above types receives nonempty interpretation in the model.

For example, the principle UIP is intuitively valid according to the naive set-theoretic semantics where Id_{A}(x, y) is empty if x and y are different objects of A and is a singleton set otherwise. The principle UIP has some practical relevance because it is equivalent to the derivability of Id_{Σx:A.B(x)}(y, z) from Id_{Σx:A.B(x)}(⟨x, y⟩, ⟨x, z⟩) as shown in [8].

It is known that UIP can be derived using pattern-matching, cf. [1]. Thus according to the result of this paper pattern-matching is a non-conservative extension of intensional constructive type theory. A syntactic proof of the nonderivability of UIP is not known and — if it exists — probably too complicated to be presented in a transparent way. Therefore, in this paper we use a semantic method to establish independence of UIP. Now almost all known models are extensional in the sense that the identity reflection rule is validated and therefore UIP holds trivially. Even in the non-extensional models studied in [8] UIP always holds. A syntactic argument shows that whenever UIP holds for some interpretation of the Id-type then UIP holds for all possible interpretations of the Id-type in the same model. Thus in order to disprove UIP we must look for a model which does not admit any interpretation of the extensional identity types. We will show that such a model can be obtained by interpreting types as groupoids.

2 The Groupoid Model

Although by lack of UIP not any two identity proofs are propositionally identified various equational laws do hold which induce a natural groupoid structure on every type A. For example for appropriately typed p, q, r the following two types are always inhabited

Id(trans(p, trans(q, r)) , trans(trans(p, q), r) Trans-Assoc
Id(trans(p, symm(p)) , refl(x))  Symm-Inv-R

More generally we can show using J that the identity type Id_{A} endows every type A with a groupoid structure where the groupoid laws are satisfied up to propositional equality. This suggests to construct a model where types are interpreted as groupoids and where Id_{A}(x, y) intuitively does not mean equality but “being isomorphic”, i.e. Id_{A}(x, y) will be interpreted as the discrete groupoid whose objects are the morphisms from the interpretation of x to the interpretation of y. In this model the interpretations of Id_{A}, refl, symm, and trans endow a type A with a groupoid structure satisfying the corresponding equational laws up to actual and not only up to propositional equality.

First we recall some basic definitions.

Groupoids and fibrations of groupoids. A groupoid is a category where all morphisms are isomorphisms. A functor p : Δ → Γ between groupoids Δ and Γ is a fibration iff for any f : γ → γ′ in Γ and δ in the fibre over γ, i.e. p(δ) = γ, there exists a morphism ϕ : δ → δ′ (for some δ′ over γ′) over f, i.e. p(ϕ) = f. Equivalently, for every δ′ above γ′ there exists a morphism ψ : δ → δ′ above f. A fibration of groupoids is split if there is a given choice of these morphisms compatible with the groupoid structure, i.e. the chosen morphism above the identity is the identity and the chosen morphism above a composition is the composition of chosen morphisms.

If S is a covariant functor from groupoid Γ to the category of groupoids then the Grothendieck construction associates with S a split fibration gr(S) : Gr(S) → Γ. The groupoid Gr(S) has as underlying class of objects the pairs ⟨γ, s⟩ with γ ∈ |Γ| and s ∈ |S(γ)| and morphisms from ⟨γ, s⟩ to ⟨γ′, s′⟩ are pairs ⟨f, ϕ⟩ such that f : γ → γ′ and ϕ : S(f)(s) → s′. Composition of morphisms is given by ⟨g, ψ⟩ ∘⟨f, ϕ⟩ = ⟨g ∘ f, ψ ∘ S(f)(ϕ)⟩. The fibration gr(S) itself is the projection on the first component.

Categories with attributes. As an abstract frame of model we use the by now well-established notion of “category with attributes”. Recall from [7, 5] that such a structure is given by

• a category Con with terminal object 1

• a presheaf Fam : Con^{op} → Set with morphism part written Fam(f)(S) =_{abbr} S[f]

• an operation p which to each S ∈ Fam(Γ) associates a Con-morphism p_{S} : Γ · S → Γ — the canonical projection of S

• An operation · which to each Con-morphism f : Γ → Δ and S ∈ Fam(Δ) associates a morphism f · S : Γ · S[f] → Δ · S such that ^{1}

[figure: Γ · S[f]; f · S; Δ · S; Γ; ^{p^{S[f]}}; f; Δ; ^{p^{S}}]

is a pullback and the coherence conditions id_{Δ}·S = id_{Δ·S[f]} and (f ∘ g)·S = (f · S) ∘(g · S[f]) for g : Θ → Γ are satisfied.

Provided that suitable interpretations of base types and type constructors are given, a partial interpretation function can be defined by structural induction in such a way that every context is interpreted as a Con-object, every type is interpreted as an element of Fam at the interpretation of its context and finally terms are interpreted as sections (right inverses) of the canonical projections associated to their types. This interpretation is sound in the sense that the interpretation of all derivable judgements is defined and that all equality judgements are validated w.r.t. the actual equality in the model.

1This and the following diagrams have been typeset using Paul Taylor’s diagram macros.

We now turn to the definition of a particular category with attributes based on the category of groupoids. Let Con denote the category of all not necessarily small groupoids and functors between them. We put Fam := Func(−, Con), i.e. for Γ ∈ |Con| the set Fam(Γ) is the set of functors from Γ viewed as a category to the category of groupoids, and if in addition f : Δ → Γ then S[f] is the functor S ∘ f : Δ → Con. The canonical projection p_{S} : Γ · S → Γ is the fibration of groupoids associated to S by the Grothendieck construction and finally f · S : Δ · S[f] → Γ · S is the second projection of the canonical pullback of p_{S} along f. Its effect on objects is Δ · S[f] ∋ (δ, s) ↦ (f(δ), s) ∈ Γ · S.

Proposition 1 The above data define a category with attributes.

Now we will describe the interpretation of the type constructors.

2.1 Dependent Products and Sums of Families of Types

Proposition 2 The groupoid model can be endowed with dependent products and sums of families.

We sketch the construction for the case of dependent products. Let Γ ∈ |Con|, S ∈ Fam(Γ) and T ∈ Fam(Γ · S). First we need some auxiliary notation. Let p_{γ} : T_{γ} → S(γ) be the fibration associated by the Grothendieck construction to the family S(γ) → Con obtained by restricting T along the inclusion of S(γ) into Γ · S. For a : γ → γ′ let T_{a} : T_{γ} → T_{γ′} denote the functor defined by T_{a}(s, t) = (S(a)(s), T (a, id_{S(a)(s)})(t) and T_{a}(b, c) = (S(a)(b), T (a, id_{S(a)(s)})(c).

Then Π(S, T) ∈ Fam(Γ) is given as follows. For γ ∈ |Γ| we define Π(S, T)(γ) as the groupoid of all functors M : S(γ) → T_{γ} such that p_{γ} ∘ M = id_{(}γ). Whenever a : γ → γ′ then Π(S, T)(a) : Π(S, T)(γ) → Π(S, T)(γ′) is defined by putting Π(S, T)(a)(M) = T_{a} ∘ M ∘ S(a^{−1}) and the morphism part is defined analogously.

2.2 The Interpretation of the Identity Type

Let Γ ∈ |Con| and S ∈ Fam(Γ). Then Id_{S} ∈ Fam(Γ · S · S[p_{S}]) is defined as follows. For γ ∈ |Γ| and s, t ∈ |S(γ)| let Id_{S}(γ, s, t) be the discrete groupoid with S(γ)(s, t) as underlying set of objects. The unique element of a homset Id_{S}(γ)(s, s) is denoted ⋆. If furthermore a : γ → γ′, b : S(a)(s) → s′ in S(γ′) and c : S(a)(t) → t′ in S(γ′) (i.e. the triple (a, b, c) is a morphism from (γ, s, t) to (γ′, s′, t′) in Γ · S · S[p_{S}]) then for i ∈ Id_{S}(γ, s, t) we put Id_{S}(a, b, c)(i) = c ∘ S(a)(i) ∘ b^{−1}. The action on morphisms is defined analogously. Notice that the total object I_{S} := Γ·S·S[p_{S}]·Id_{S} of this family is the fibrewise arrow category of S or equivalently the inserter of the two projections from Γ·S ·S[p_{S}] to Γ·S.

I_{S}  \overline{^{p_{Id_{S}}} ▷} Γ · S · S[p_{S}]  \overline{p_{S} · S  ▷} ; \overline{_{p_{S[p_{S}]}}} Γ · S

Recall from [2] that the inserter is a 2-categorical generalisation of the concept of equalizer in which equality is replaced by natural transformation.

Reflexivity. In order to interpret the constructor refl we define a section of the canonical projection of Id_{S}[Δ_{S}] where Δ_{S} : Γ · S → Γ · S · S[p_{S}] is the fibrewise diagonal. We define refl_{S}(γ)(t) := (γ, t, t, id_{t}) which extends uniquely to a morphism. Using the presentation of Id as an inserter we get refl (or rather its composition with Δ_{S} · Id_{S}) as the unique fill-in w.r.t the identity 2-cell in

I_{S}  \overline{^{p_{Id_{S}}} ▷} Γ · S · S[p_{S}]  \overline{p_{S} · S} ; \overline{_{_{p_{S[p_{S}]}}  ▷}} Γ · S

[figure: Δ_{S}]

Γ · S^{r^{S}} . . . . . . . . .

Identity elimination. Finally in order to interpret the eliminator J assume that C ∈ Fam(I_{S}) and that d is a section of the canonical projection of the family C[Δ_{S} · Id_{S}][refl_{S}] ∈ Fam(Γ · S). The we define the section J(d) of p_{C} by putting J(d)(γ, s, t, p) = C(id_{γ}, id_{s}, p, ⋆)(d(γ, s)). Notice here that (id_{γ}, id_{s}, p, ⋆) is a morphism in I_{S} from (γ, s, s, id_{s}) — an object in the domain of d, to (γ, s, s′, p)

— a most general object of I_{S}. The morphism part is defined similarly. Notice that although this interpretation is somewhat arbitrary (it depends on the choice of the morphism parts of the involved presheaves S and C) the whole situation is nevertheless stable under reindexing of Γ. More categorically, the interpretation of J gives us a canonical (stable under pullback) factorisation of morphisms d : Γ · S → C with p_{C} ∘ d = r_{S} through r_{S}.

C

[figure: d]

[figure: Γ · S; r_{S}; I_{S}; ^{p^{C}}^{▽}; .; .; .; .; .; .; .; .; .; J(d)]

such that moreover J(d) is a section. It is possible to derive this property from the characterisation of Id as an inserter alone. It is of course important and a distinctive feature of the groupoid model that this inserter arises as a canonical projection (is a split fibration).

Intensionality of the groupoid model. This interpretation of the identity type is intensional in the sense that in the model the identity reflection rule is not validated as in the model propositional equality only means isomorphism, but not actual equality. For the same reason unlike in the intensional models studied in [8] (and in fact in the term model) the equality reflection rule is not even valid in the empty context (i.e. for global elements). On the other hand in the groupoid model the type

f, g : A → B ⊢ (Πa : A.Id_{B}(f a, g a)) → Id_{A→B}(f, g)

is inhabited (by the identity!) which is a rather extensional feature.

2.3 The Other Type Constructors

The type N of natural numbers gets interpreted as the discrete groupoid whose underlying set of objects is the set of natural numbers. The (first) universe U gets interpreted as the non-small discrete groupoid whose underlying set is the set of all small groupoids. The generic family gets interpreted as the embedding functor from U to the category of all small groupoids.

We conjecture that all other type formers considered e.g. in [6] can be interpreted as well.

3 The Independence Result

Suppose Γ is a groupoid with an object γ with a nontrivial endomorphism a ∈ Γ(γ, γ). Now if UIP could be derived uniformly using J its interpretation in the model would give rise to an object in Id_{Id_{Γ}(γ,γ)}(refl_{Γ}(γ), b). But since Id_{Γ}(γ, γ) is discrete this entails that a = refl_{Γ}(γ) contradicting the assumption. This does not contradict UIP for certain specific types as e.g. N, List(N) etc. which in our model get interpreted as discrete groupoids for which UIP trivially holds as any homset contains at most one element. Indeed, for the latter two types UIP is actually syntactically derivable in the presence of a universe. It is still an open problem whether UIP holds for N → N which in our model is discrete, too.

A syntactically definable type for which UIP fails is ΣX : U.El(X) as there is a small groupoid containing an object admitting two different endomorphisms. Thus we have proved Theorem 1. Again it is an open problem whether there exists a type definable without universe for which UIP fails. Our model cannot solve this problem since the interpretations of all such types are discrete.

3.1 Another identity elimination rule

In [8] it has been shown that the validity of UIP is equivalent to the existence of a further eliminator K for Id-types (independently found by Th. Altenkirch) whose meaning is given by the following rules:

\begin{matrix}Γ, x : A, z : Id_{A}(x, x) ⊢ C(x, z) \\ Γ, x : A ⊢ d : C(x, refl_{A}(x)) \end{matrix}

\begin{matrix}Γ, x : A, z : Id_{A}(x, x) ⊢ K_{A,C}(d, x, z) : C(x, z) \\ Γ, x : A ⊢ K_{A,C}(d, x, z) = d : C(x, refl_{A}(x)) \end{matrix}

Intuitively, K is the eliminator for the inductive family x : A ⊢ Id_{A}(x, x) where the inductive structure is inherited from the family x : A, y : A ⊢ Id_{A}(x, y). We will now give a direct proof of the fact that the eliminator K cannot be interpreted in the groupoid model. (There is an indirect proof because employing K we can derive UIP!). In this proof we are a bit less formal and in this way try to highlight the main intuitive idea behind the identity type in the groupoid model.

We use the syntax informally to denote objects in the groupoid model. Moreover, we only consider Id for a groupoid (viewed as an element of Fam(1)) and not for arbitrary families. For any groupoid G the fibration associated to the family x, y : G ⊢ Id_{G}(x, y) is given by the functor ⟨∂_{0}, ∂_{1}⟩ : G^{→} → G × G where G^{→} is the arrow category of G and ∂_{0}, ∂_{1} are the domain and codomain functors. The constructor refl_{G} gives a functor R making

G^{→}

[figure: R]

[figure: G; Δ_{G}; G × G; ⟨∂_{0}, ∂_{1}⟩]

commute. R sends g ∈ |G| to id_{g}. If q : C → G^{→} is a (split) fibration associated to a family as in the premise of J then from a morphism d : G → C such that q ∘ d = R we get a section J(d) of q. Its construction hinges on the fact that in G^{→} every object p : g → g′ is connected to an identity morphism as follows.

[figure: g; id_{g}; g; g; ^{id^{g}}; p; g′; p]

As shown above in Section 2.2 we get J(d) from d by reindexing (in q) along this morphism.

Now in the premise to K the situation is entirely different. The diagonalised family g : G ⊢ Id_{G}(g, g) is the pullback of U : G^{→} → G along the diagonal Δ_{G}.

More explicitly it is the fibration V : G^{endo} → G where G^{endo} is the category with objects (g, p) where g ∈ |G| and p : g → g and a morphism from (g, p) to (g′, p′) is a G-morphism f : g → g′ such that p′ ∘ f = f ∘ p. V is the first projection. Unlike in the category G^{→} in G^{endo} the identities are isolated. If there is a morphism from (g, id_{g}) to (g′, p) then p = id_{g′}. Now if we had an interpretation of the eliminator K in the groupoid model then for any split fibration q : C → G^{endo} and functor d : G → C with q ∘ d = refl_{G} (here refl_{G} is meant to have codomain G^{endo} !) we would get a section K(d) of q. But now since the identities are isolated in G^{endo}, the morphism refl_{G} is such a fibration itself! So we get a section of refl_{G} which is a contradiction in case G has an object with a nontrivial endomorphism.

4 Conclusion and Open Problems

In this paper we have shown that the current formulation of intensional constructive type theory is incomplete w.r.t. the intuitive understanding of identity types. Namely, it is possible to construct a model where not all proof objects of an identity type are necessarily propositionally equal (that they are not always judgementally equal is a characteristic feature of intensional type theory anyway). For this purpose we have constructed a model where types are interpreted as groupoids, functions as morphisms of groupoids and propositional equality as “being isomorphic” where the proof objects in type Id_{A}(t, s) are exactly the isomorphisms of the interpretations of t and s, respectively. As the basic types which can be defined without a universe get interpreted by discrete groupoids in our model for them the principle UIP (= Unicity of Identity Proofs) holds nevertheless. But our result shows that for each such type — in order to prove UIP for it — requires a new idea, i.e. it cannot be done uniformly.

Supposedly, UIP is not provable for the type N → N. It might be the case that this can be proved in a semantical way by synthesizing the groupoid model of this paper with the modified realizability model described in Chapter 3 of [8].

Our work suggests that the intensional identity type can be used as an “internal language” for groupoid-like structures. In particular it seems worthwhile to investigate whether the intensional identity type facilitates the monstruous bookkeeping requirements needed when dealing with coherent isomorphism instead of actual equality. This idea ties in with the approach of [3] where, however, the rules for the intensional identity type are not used.

References

[1] Thierry Coquand. Pattern Matching with Dependent Types. In Workshop on Logical Frameworks, Båstad, 1992. Preliminary Proceedings.

[2] Gregory Maxwell Kelly and Ross Street. Review of the elements of 2categories. In Proceedings of the Category Seminar, Sydney, pages 75–103. Springer, LNM 420, 1972/73.

[3] François Lamarche. A Proposal about Foundations I. Manuscript.

[4] Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis·Napoli, 1984.

[5] Eugenio Moggi. A category-theoretic account of program modules. Math Struct. in Comp. Sci., 1(1):103–139, 1991.

[6] B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löfs Type Theory, An Introduction. Clarendon Press, Oxford, 1990.

[7] Andrew Pitts. Categorical logic. In Handbook of Theoretical Computer Science. Elsevier Science, 199? to appear.

[8] Thomas Streicher. Investigations into Intensional Type Theory. Habilitationsschrift, LMU München, 1993.