## July 26, 2022

### Identity Types in Context

#### Posted by Emily Riehl

guest post by Shreya Arya and Greta Coraglia

The relation between mathematicians and the notion of identity has been an interesting one. Even what is arguably the first mathematical text (that we know of) in history, Euclid’s Elements (c. 300 BC), deals with the problem of equality. In Book I, after Definitions and Postulates, Euclid details five Common Notions:

1. Things equal to the same thing are also equal to one another.
2. And if equal things are added to equal things then the wholes are equal.
3. And if equal things are subtracted from equal things then the remainders are equal.
4. And things coinciding with one another are equal to one another.
5. And the whole [is] greater than the part.

On one hand, such notions are considered “common”, so that they are trivial enough that everyone ought to agree with them; on the other, they are not so trivial that one can avoid writing them down. Moreover, Euclid feels the need to pin-point the effect that equality must have on operations involving such objects: the underlying principle here is that two entities that are equal should share the same properties and behaviours.

What mathematicians really use is a bit stronger than that…1

The opposite formulation of such principle is sometimes called Leibniz’s law or identity of indiscernibles, and states that any two objects that share the same properties must be equal, or, in the notation of symbolic logic, $\forall\;F\,(Fx \leftrightarrow Fy) \;\to\; x=y \,.$ Of course the assumption of such principle, or even those deemed “common” by Euclid, is entirely debatable. In fact, these represent just a glimpse into the non-triviality of the treatment of equality and identity in mathematics.

The aim of this post is to compile a (non-exhaustive) survey on the different approaches that mathematicians have applied to the problem of identity throughout the centuries. Our goal is presenting some ideas - old and new - in order to better understand identity types.

First order logic and lattice-valued models

Even in a field as well established as first-order logic there is no precise convention as to whether equality should be considered as a primitive symbol satisfying certain axioms, or if it should be a treated as a non-logical symbol and introduced as a binary predicate. Still, in both versions equality is intended to be:

1. binary, so that it pertains pairs of terms;
2. reflexive, so that for each term $t$ one has $t=t$;
3. substitutional (w.r.t. both to formulas and function symbols), so that it satisfies Leibniz’s law.

Substitutionality implies, amongst others, symmetry and transitivity of “=”.

For the categorical logic people: equality as a left adjoint!2

Not only it is not trivial how an equality predicate should be defined, it is not trivial how it should be interpreted. It is particularly interesting to notice how the shift from a binary, $\{0,1\}$ interpretation, to a multi-valued approach to models of first-order theories affected our notion of equality. Following Cohen’s proof of the independence of the continuum hypothesis from ZFC, different works aimed to provide new models witnessing it. In a paper from (1967), Scott first introduces a different way of comparing elements of a set. It is no longer the case that either two elements are equal, or they are not, but they might be to some extent or with a certain probability. We here present a slightly different version involving a generic complete Boolean algebra $B$, in the original work the author considers the case where $B= \mathcal{F}/[P=0]$ with $\mathcal{F}$ a space of events for probability measure $P$. A Boolean-valued model of a theory with an equality predicate, then, matches to each formula some value $b\in B$, and in particular it must satisfy the following inequalities

\begin{aligned} ||a=a|| &= 1\\ ||a=b|| &= ||b=a||\\ ||a=b|| \wedge ||b=c|| &\leq ||a=c||\\ \bigwedge_{i \leq n-1} ||a_i = b_i|| \wedge ||R(a_1,\dots,a_{n-1})|| &\leq ||R(b_1,\dots,b_{n-1})|| \end{aligned}

which encode the basic properties described above. The interested reader can find a detailed explanation in Higgs (1970).

Equality and existence: what should $||a=a||$ be?3

In type theory

In the context of type theory we have two very different kinds of identities.

1. Judgemental, or definitional: you can think of it as an identity you can reason with. It might pertain terms or types, and it is part of the basic syntax of types. In Martin-Löf’s first work on intuitionistic type theory, we have four kinds of judgements, $\Gamma \vdash A \qquad \Gamma\vdash a:A \qquad\Gamma\vdash A=B\qquad \Gamma\vdash a=b:A\,.$ The fact that equality here is a judgement, instead of a proposition (a type), is a first key difference between type theory and set theory. Traditional reflexivity, symmetry, and transitivity are encoded in the form of rules added to the system. They look precisely how you think.4 Moreover, we ask that its influence is, again, propagated throughout the computation when applied to the basic features of the theory (typing and substitution), so that we require the following additional three rules. $\frac{ \Gamma \vdash a:A \quad \Gamma \vdash A=B} { \Gamma \vdash a:B} \qquad \frac{ \Gamma \vdash a=a':A \quad \Gamma, x:A\vdash B} { \Gamma \vdash B[a]=B[a'\!]}\qquad \frac{ \Gamma \vdash a:A \quad \Gamma, x:A\vdash B=B'} { \Gamma \vdash B[a]=B'\![a]}$

2. Propositional, or provable: you can think of it as an identity you can reason about. It only pertains pairs of terms of a type, and each pair produces a new type, called the identity type. Intuitively its terms are meant to be interpreted as proofs or witnesses of the identity of the two terms. In fact, it is no coincidence that it was first introduced in the context of intuitionistic logic - see Martin-Löf, “An Intuitionistic Theory of Types: Predicative Part” (1975).

Now, while the first kind of equality is considered a sort of “built-in” of type theory, there are many proposals regarding the second kind. Most of the literature agrees on the what the Formation and Introduction rule should look like, $\frac{ \Gamma\vdash A \quad \Gamma \vdash a:A \quad \Gamma \vdash a':A} { \Gamma \vdash \mathsf{Id}_A(a,a')} \qquad \frac{ \Gamma \vdash a:A } { \Gamma \vdash r_a:\mathsf{Id}_A(a,a)}$ The first depicts what the ingredients of the identity type are, the second says that there is at least one term in $\mathsf{Id}_A(a,a)$, so that reflexivity is always provable. Elimination (and therefore Computation), instead, is the one that can be treated the most differently. We describe a few variations below, forgoing writing a possible context $\Gamma$ across-the-board.

The J-rule

Chronologically, the first proposal is the eliminator $J$, introduced in Martin-Löf (1975). $\frac{ x,y:A,u:\mathsf{Id}_A(x,y) \vdash C \quad x:A\vdash d:C[r_x] \quad \vdash a:A \quad \vdash b:A \quad \vdash p: \mathsf{Id}_A(a,b) }{ \vdash J(a,b,p):C[a,b,p] }$ Intuitively, it is saying that $\mathsf{Id}$ is defined inductively out of its behaviour at $r_x$, and, in fact, when applied at $r_x$ must yield the identity: its associated Computation rule is the following. $\frac{ x,y:A,u:\mathsf{Id}_A(x,y) \vdash C \quad x:A\vdash d:C[r_x] \quad \vdash a:A }{ \vdash J(a,a,r_a)=d[a]:C[a,a,r_a] }$ Notice that here we first see the two different identities interacting.

The reflection rule

One might want to more tightly link the two notions of identity. For example, one could ask that two terms that are provably equal must be judgementally equal, hence that the following holds. $\frac{ \vdash p : \mathsf{Id}_A(a,b)} { \vdash a=b:A}$ This is sometimes called the Reflection rule - not to be mistaken with reflexivity of the equality predicate - and it too is a possible choice for elimination of $\mathsf{Id}$. A type theory with reflection is called extensional, while if it requires the J-rule it is said to be intensional. Intensional and extensional theories have different expressiveness, and in general are very different as computational tools: the main reason is that propositional equality is undecidable, hence the reflection rule makes provable equality undecidable, as well, while it is decidable in the intensional case. This is a good reference for comparisons.

The K-rule

One might also wonder whether two proofs of identities should be identified or not, or that given $u,v : \mathsf{Id}_A(a,b)$ whether there should be a term in $\mathsf{Id}_{\mathsf{Id}_A(a,b)}(u,v).$ This is usually called the Uniqueness of Identity Proofs principle (UIP). In “The groupoid interpretation of type theory” Hofmann and Streicher prove that it does not in fact follow from the $J$-rule because it does not hold (for all types $A$) in their proposed model - which will be discussed in the following section. In his habilitation thesis, the second author then proposes the following alternative Elimination rule, $\frac{ x:A,u:\mathsf{Id}_A(x,x) \vdash C \quad x:A\vdash d:C[r_x] \quad \vdash a:A \quad \vdash p: \mathsf{Id}_A(a,a) }{ \vdash K(a,p):C[a,p] }$ and shows that it is equivalent to UIP. It is closely related to using $u$ as pattern matching for $\mathsf{Id}$. This is currently the way Agda automatically implements identity types.

All in all, dealing with identity is hard. “It is no wonder that twenty years passed from Martin-Löf’s proposed identity type (1975) to the interpretation in the Hofmann-Streicher paper (1996).” 5

As it is the case for fuzzy interpretations of the equality predicate in first order logic, models are precious tools we can use to better undertand the syntax we might have built for very good reasons. The following sections introduce the groupoid model of Martin-Löf’s type theory with identity types.

The Groupoid Interpretation of Identity types

We work in the setting of Martin Löf’s type theory. From now on, we write the identity type $Id_A(x,y)$ as $x=_A y$. A term of the type $x=_A y$ for $x,y: A$ is called an identification or path from $x$ to $y$.

We can think of the identity $=_A$ as an “equivalence relation.” More precisely, we have the following:

1. Reflexivity: There is a term $r_x: x=_A x$ for all $x: A$.

2. Symmetry: If $p:x=_A y$ is a path from $x$ to $y$, we have an inverse path $p^{-1}:y=_A x$.

This can be seen by defining the inverse operation $\mathrm{inv}: \prod_{(x,y:A} (x=_A y) \to (y=_A x)$ where we let $\mathrm{inv}(p)=p^{-1}$. By path induction (J-rule) it is suffices to construct $\mathrm{inv}(r_x) : x=_A x.$ Define $\mathrm{inv}(r_x) \coloneqq r_x.$

3. Transitivity: We can concatenate paths $p:x=_A y$ and $q:y=_A z$ to produce a new path $p\circ q:x=_A z$.

This can be seen by the concat operation: $\mathrm{concat}: ∏_{(x,y,z:A} (x=_A y) \to (y=_A z) \to (x=_A z).$ Denote $\mathrm{concat}(p,q) = p\circ q$. Again, by path induction it suffices to construct $\mathrm{concat}(r_x): ∏_{(z:A} (x=_A z) \to (x=_A z).$ Define $\mathrm{concat}(r_x)_z \coloneqq id_{(x=_A z)}$

Exercise 1: Show that concatenation is associative and satisfies $p\circ p^{-1} = r_x$ and $p^{-1}\circ p =r_y$. In other words construct a term $\alpha_{pqr}: (p\circ q)\circ r = p \circ (q\circ r)$ and $\lambda_x: p\circ p^{-1} = r_x$ and $\lambda_y: p^{-1}\circ p =r_y$.

${\color{#008B00} Upshot:}$ We can interpret types as groupoids!

A groupoid is category in which every morphism is invertible. In other words, every arrow in a groupoid can be inverted. The objects of the category are terms of a type $A$ and the morphisms between two terms $x,y :A$ are paths between $x$ and $y$. Every morphism is invertible because of the existence of inverse paths. An explicit construction of this can be seen in this paper.

Towards an $\infty$- groupoid structure of type theory

The first thing to observe is that $x=_A y$ is also a type and so it can be recognised as a groupoid. The morphisms in this groupoid are paths $p: \alpha =_{x=_A y} \beta$. There is no reason to stop here as we can also model the type $\alpha =_{x=_A y} \beta$ as a groupoid. The arrows in this groupoid are now the higher dimensional paths $\eta: p =_{\alpha =_{x=_A y} \beta} q$. We can continue this process “up to infinity.”
As a result of the iterated application of J-rule, these “higher” types satisfy some nice coherence properties. These coherence properties allow us to the package this into an infinity groupoid.

An infinity groupoid can be thought of as a family of sets $G_n$ for $n=0,1,2,...$ with additional structure: compositions, identity morphisms and inverse elements that satisfy unit, inverse and associativity laws “up to the next level.” Here is what “up to the next level” means in context of composition and associativity:

To summarise, $G_0$ is the set of points, $G_1$ is the set of 1-dimensional arrows between the points, $G_2$ is the set of 2-dimensional arrows (or the 2-cells) from any parallel pair of 1-dimensional arrows and so on.

Types can be packaged as infinity groupoids in the following sense:

The iterated application of J-rule for identity types gives us the coherence relations for free.
For example, in Exercise 1 we constructed a proof of associativity $\alpha_{pqr}: (p\circ q)\circ r = p \circ (q\circ r).$ Here $\alpha_{pqr}$ is a 2-cell and can be seen as term of $G_2$. Similarly $\lambda_x$ and $\lambda_y$ are also 2-cells.

There are other models of type theory.6 Voevodsky observed that the groupoid and simplicial models of type theory satisfies a key property- called univalence. Univalence makes the relation between homotopy theory and type theory very clear. This is an extremely humble introduction to univalence, the true genuis of univalence can be seen here.

Univalence

In traditional set theory, any proof of $x=y$ should be equal. Following an example from Grayson, in classical set theory the following sentence is false. $\mathbb{N} = \{x\in \mathbb{Z}| x \ge 0\}.$ This is because, if $\mathbb{Z}$ is defined as a certain quotient of $\mathbb{N}\times \mathbb{N}$, their elements are different. If you’d ask any mathematician, though, they would say that there is really no problem in treating them as if they were the same, and in fact there is an isomorphism - actually more than one. Univalence is meant to implement this “as if” into a formal system. Before we state the axiom, we give a few definitions:

Let $f$ and $g$ be two functions. A homotopy from $f$ to $g$ is a function of type $f\sim g \coloneqq \prod_{x:A}(f(x)=g(x)).$

A type $A$ is contractible when there is a point in $\sum_{(x:A)} \prod_{(y:A)} x=_A y$. This means that there is some $x:A$ such that $x=y$ for every $y:A$.7

The fiber of a function $f:A\to B$ over a point $y:B$ is $\mathrm{fib}_y(f) \coloneqq \prod_{x:A} (f(x)=y).$

The function $f:A \to B$ is an equivalence of types if the fiber of $f$ is contractible over all points $y:B$. We say $f$ is a term of type $A\cong B$.

Example: A contractible type $A$ is equivalent to 1 (the type with one term $\star$). This can be seen by the equivalence $f:A \to$ 1 sending $a \mapsto \star$ for evry $a:A$.

We are now ready to define the Univalence Axiom.

${\color{#EE1289} \text{Univalence Axiom (UA):}}$ For any two types $A$ and $B$, $(A = B) \cong (A\cong B).$

Equivalent types maybe identified.

Here, we haven’t specified in which type ‘=’ holds. There is a notion of types of types called universes and so we say more precisely, a universe $U$ is univalent if $(A =_U B) \cong (A\cong B)$ for all types $A,B: U$.

The power of the univalence axiom will be given in the next section and for now we content the reader with an example. The UA states that at element of $A=B$ can be thought of as providing a way to identify $A$ with $B$.

In the presence of univalence, we no longer need to abuse notation to write $\mathbb{N} = \{x\in \mathbb{Z}| x \ge 0\}.$

H-levels

Voevodsky observed that types can be stratified according to homotopy levels or h-levels. The h-level expresses the homotopy level of a type $A$ in following sense:

${\color{#008B00} \text{h-level 0}:}$ Contractible types $A$

${\color{#008B00} \text{h-level n+1}:}$ Types $A$ such that $x=_A y$ has h-level $n$.

Note: In modern notation, h-level 0 is written as h-level -2 so that sets have homotopy level 0.
We now describe types of h-levels 1 and 2.
A type A is a proposition if any two terms of A are equal. In other words, $\mathrm{isProp}(A) \coloneqq\prod_{(x,y:A)} x=_A y.$ This is in accordance with our intuition that any two proofs of a proposition are equal. By definition of h-levels, the h-level of propositions is 1.

A type A is a set if for all $x,y:A$ and all $p,q:x=y$, we have $p=q$. In other words, any two terms of a set are propositions. Formally,

$\mathrm{isSet}(A) \coloneqq\prod_{(x,y:A)}\prod_{(p,q:x=y)} p=q.$

Intuitively, we want a set to be a type that does not contain any higher homotopical information. This coincides with our intuition of sets- proofs of equality of sets are equal.

Example: $\mathbb{N}$ is a set.
Non-Example: The type Group is not a set.

In the presence of UA, for any two groups $G$ and $H$ we have an equivalence, $f: (G=H) \to (G\cong H).$ There may be multiple isomorphisms from $G$ to $H$ and so $(G\cong H)$ may have more than one element. So, the UA implies that $(G=H)$ may have more than one element which means that Group is NOT a set! But, the group isomorphisms $(G\cong H)$ type is a set and so under UA, the type $(G=H)$ is a set. This gives groups a h-level of 3. More generally, groupoids have h-level 3.

As you may guess, $n$-groupoids have h-level $n$. We end with a schematic view of the homotopy levels of types.

We have touched on different approaches and facets to identity in maths in general, and in type theory in particular. Pursuing a better understanding of it is not only the first step in the direction of a complete formalisation of mathematics, but a continuous source of inspiration.

1 … and can be made precise with the name of Equivalence Principle (EP). It intuitively states that two objects which are the same according to some notion of sameness share the same properties, if one only consider those that are relevant to that notion. A first attempt at relating this to univalence, introduced below, can be found here.

2 In “Equality in hyperdoctrines and the comprehension schema as an adjoint functor” (1970) Lawvere shows that in the language of doctrines such properties fit into the description of a left adjoint: consider a functor $P:\mathcal{C}^{op}\to\mathbf{Cat}$ (in loc.cit. the author assumes $\mathcal{C}$ and $P(C)$ to be cartesian closed for all $C$ in $\mathcal{C}$). We can think of $\mathcal{C}$ as the category of contexts or lists of sorts, and its morphisms as terms, then $P$ maps to each context the Lindenbaum-Tarski algebra of well-formed formulae in such context. Such a functor (called a doctrine) is said to be elementary if the image of the (parametrized) diagonal $id_{C \times \Delta_A}: P(C\times (A\times A)) \to P(C\times A)$ has a left adjoint $=^C_A$ satisfying Frobenius reciprocity and Beck-Chevalley. The unit of such an adjoint pair, for example, describes the reflexivity of this so called “equality”.

3 Again, such interpretetation is merely a choice, for example in Identity and existence in intuitionistic logic (1979) Scott even questions the fact that $||a=a||$ should be the top element in the Boolean (in this case, Heyting) algebra, so that the one element should be equal to itself not with maximum “probability” or “certainty”, but only to the extent is exists in the system.

4 $\frac{ \Gamma \vdash A} { \Gamma \vdash A=A} \qquad \frac{ \Gamma \vdash A=B} { \Gamma \vdash B=A} \qquad \frac{ \Gamma \vdash A=B \quad \Gamma\vdash B=C} { \Gamma \vdash A=C}$   $\frac{ \Gamma \vdash a:A} { \Gamma \vdash a=a:A} \qquad \frac{ \Gamma \vdash a=b:A} { \Gamma \vdash b=a:A} \qquad \frac{ \Gamma \vdash a=b:A \quad \Gamma\vdash b=c:A} { \Gamma \vdash a=c:A}$

5 This is from a very nice PhD course held by F. Dagnino and J. Emmenegger in Genova in the spring of 2022.

6 Historically, there have been many definitions of $\infty$-groupoids- globular sets, quasi categories (or Kan complexes) and topological categories. The model described above uses the globular sets defintion of $\infty$-groupoids follwowing Berg and Garner.The Grothendieck homotopy hypothesis says

“Any topological space up to homotopy is essentially the same as an $∞$-groupoid”.

In the Kan complex definition of $∞$-groupoids, this hypothesis is true. There is a model of type theory in Kan complexes given by Veovodsky & Streicher (2006/2009). This allows us to interpret “types as topological spaces.” This was generalised to model structures in abstract homotopy theory by Awodey and Warren in 2006.

7 Construct a type that checks if $A$ is contractible as follows: $\mathrm{isContractible}(A) \coloneqq \sum_{(x:A)} \prod_{(y:A)} x=_A y$

Posted at July 26, 2022 5:51 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3410

### Re: Identity types in context

Elimination (and therefore Computation), instead, is the one that can be treated the most differently. We describe a few variations below, forgoing writing a possible context $\Gamma$ across-the-board.

There is also the variant of the J-rule which is only valid up to a path, rather than judgmental equality; these are frequently found in cubical type theories for path types.

### Re: Identity types in context

Minor error here:

As you may guess, $n$-groupoids have h-level $n$.

It should be

As you may guess, $n$-groupoids have h-level $n + 2$.

### Re: Identity types in context

In modern notation, h-level 0 is written as h-level -2 so that sets have homotopy level 0.

While I am all for the “modern” indexing convention (which is actually the much older one in classical homotopy theory – Voevodsky’s starting-at-0 convention, though logical in the abstract, was a break with tradition), I think it’s too confusing to use the same word “h-level” for both of them. Usually people talk about “$n$-types” instead of “types of h-level $n$” when using the $(-2)$-based convention. So a set is a 0-type and has h-level 2, a proposition is a (-1)-type and has h-level 1, and so on.

Posted by: Mike Shulman on July 30, 2022 5:20 AM | Permalink | Reply to this

### Re: Identity types in context

I don’t know of any recent existing sources in the HoTT literature which defines “h-level” starting from -2.

On the other hand, there is at least one fairly recent source in the HoTT literature which defines “h-level” to begin from zero: Ayberk Tosun’s thesis on formal topology in univalent foundations from 2020.

Yes, that’s exactly my point. When it starts from $-2$ (which is, in my opinion, the better convention, for strong historical and sociological reasons), we don’t use the word “h-level”, and conversely.