nLab identity type



Equality and Equivalence

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition, truth value(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
completely presented setdiscrete object/0-truncated objecth-level 2-type/set/h-set
setinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
set of truth valuessubobject classifiertype of propositions
universeobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels




The first original law of thought (WdL §875): everything is identical with itself (WdL §863), no two things are like each other (WdL §903).


In intensional type theory under the propositions as types paradigm, an identity type (or equality type) is the incarnation of equality. That is, for any type AA and any terms x,y:Ax,y:A, the type Id A(x,y)Id_A(x,y) is “the type of proofs that x=yx=y” or “the type of reasons why x=yx=y”.

To contrast with “computational” or definitional equality, inhabitation of an identity type is sometimes called propositional equality. The identity type Id A(x,y)Id_A(x,y) is sometimes written Eq A(x,y)Eq_A(x,y) or just (x=y)(x=y), but in this article we reserve the latter for definitional equality.

In set-level type theory, such as that modeled in the internal logic of a 1-category, equality is an h-proposition, and hence each Id A(x,y)Id_A(x,y) is a subsingleton. However, in higher type theories, which are the internal type theory of higher categories, identity types represent path objects and are highly nontrivial. In the internal logic of an (∞,1)-topos, one speaks of homotopy type theory. In these cases, identity types are also known as path types or path space types and are sometimes written as Path A(x,y)Path_A(x,y) instead of Id A(x,y)Id_A(x,y).

There are many different notions of identity type appearing in the type theory literature. This includes the following:

  • Martin-Löf identity types

  • cubical path types

  • Swan identity types

  • (higher) observational identity types

The key factors distinguishing these identity types from other type families is the fact that given a term x:Ax:A, each type Id A(x,x)Id_A(x,x) of the type family has a term refl(x):Id A(x,x)\mathrm{refl}(x):Id_A(x,x), and satisfy what is called the J-rule, path induction or identification elimination. In dependent type theory with dependent product types the J-rule states that given any type family C(x,y,p)C(x, y, p) indexed by x:Ax:A, y:Ay:A and p:Id A(x,y)p:Id_A(x,y), and an element c(x):C(x,x,refl(x))c(x):C(x, x, \mathrm{refl}(x)) for each x:Ax:A, there is an element J(x,y,p):C(x,y,p)J(x, y, p):C(x, y, p) for all x:Ax:A, y:Ay:A and p:Id A(x,y)p:Id_A(x,y), such that J(x,x,refl(x))J(x, x, \mathrm{refl}(x)) is equal to c(x)c(x).

However, since there are two notions of equality in type theory, there are similarly two notions of the J-rule in type theory. The definitional J-rule states that J(x,x,refl(x))J(x, x, \mathrm{refl}(x)) is definitionally equal to c(x)c(x) (i.e. J(x,x,refl(x))=c(x)J(x, x, \mathrm{refl}(x)) = c(x)). The propositional J-rule or typal J-rule states that there is a dependent term

q(x):Id C(x,x,refl(x))(J(x,x,refl(x)),c(x))q(x):Id_{C(x,x,\mathrm{refl}(x))}(J(x, x, \mathrm{refl}(x)), c(x))

Identity types which satisfy the definitional J-rule could be called strict identity types, while identity types which only satisfy the propositional J-rule could be called weak identity types, in parallel with similar definitions for a (weak and strict) Tarski universe. Martin-Löf identity types come in both strict and weak flavours. However, most other identity types in the literature, such as cubical path types and higher observational identity types, are only weak identity types.

Each kind of identity type also has one or more corresponding notions of dependent identity type. In some cases, such as cubical path types and higher observational identity types, the ordinary identity type is exactly a special case of the dependent one, where the dependence is constant or the base path is reflexivity. In other cases, such as some versions of the Martin-Lof dependent identity type, one or both of these degenerate forms of dependent identity type don’t reduce definitionally to the simple one, but are only equivalent to it.

Definition in Martin-Löf type theory

The definition of identity types was originally given in explicit form by Martin-Löf, in terms of introduction and elimination rules. Later, it was realized that this was a special case of the general notion of inductive type. We will discuss both formulations.

With introduction and elimination rules

The rules for forming identity types and terms are as follows (expressed in sequent calculus). First the rule that defines the identity type itself, as a dependent type, in some context Γ\Gamma.

type formation

ΓA:TypeΓ,x:A,y:AId A(x,y):Type\frac{\Gamma \vdash A:Type} {\Gamma, x:A, y:A \vdash Id_A(x,y):Type}

Now the basic “introduction” rule, which says that everything is equal to itself in a canonical way.

term introduction

ΓA:TypeΓ,x:Ar(x):Id A(x,x)\frac{\Gamma \vdash A:Type} {\Gamma, x:A \vdash r(x) : Id_A(x,x)}

To a category theorist, it might be more natural to call this 1 X1_X. The traditional notation r(x)r(x) indicates that this is a canonical proof of the reflexivity of equality.

Then we have the “elimination” rule, which is easily the most subtle and powerful.

term elimination

Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓ,x:A,Δ(x,x,r(x))t:C(x,x,r(x))Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)J(t;x,y,p):C(x,y,p)\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad \Gamma, x:A, \Delta(x,x,r(x)) \vdash t : C(x,x,r(x))} {\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash J(t;x,y,p) : C(x,y,p)}

Ignore the presence of the additional context Δ\Delta for now; it is unnecessary if we also have dependent product types. The elimination rule then says that if:

  1. for any x,y:Ax,y:A and any reason p:Id A(x,y)p:Id_A(x,y) why they are the same, we have a type C(x,y,p)C(x,y,p), and
  2. if xx and yy are actually identical and p:Id A(x,x)p:Id_A(x,x) is the reflexivity proof r(x)r(x), then we have a specified term t:C(x,x,r(x))t:C(x,x,r(x)),

then we can construct a canonically defined term J(t;x,y,p):C(x,y,p)J(t;x,y,p):C(x,y,p) for any xx, yy, and p:Id A(x,y)p:Id_A(x,y), by “transporting” the term tt along the proof of equality pp. In homotopical or categorical models, this can be viewed as a “path-lifting” property, i.e. that the display maps are some sort of fibration. This can be made precise with the identity type weak factorization system?.

A particular case is when CC is a term representing a proposition according to the propositions-as-types philosophy. In this case, the elimination rule says that in order to prove a statement is true about all x,y,px,y,p, it suffices to prove it in the special case for x,x,r(x)x,x,r(x).

Finally, we have the “computation” or β-reduction? rule. This says that if we substitute along a reflexivity proof, nothing happens. There are two possible computation rules, which result in strict and weak identity types respectively

computation rule for strict identity types

Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓ,x:A,Δ(x,x,r(x))t:C(x,x,r(x))Γ,x:A,Δ(x,x,r(x))J(t;x,x,r(x))=t\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad \Gamma, x:A, \Delta(x,x,r(x)) \vdash t : C(x,x,r(x))} {\Gamma, x:A, \Delta(x,x,r(x)) \vdash J(t;x,x,r(x)) = t}

Note that the equality == in the conclusion of this computation rule is definitional equality, not an instance of the identity/equality type itself.

computation rule for weak identity types

Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓ,x:A,Δ(x,x,r(x))t:C(x,x,r(x))Γ,x:A,Δ(x,x,r(x))q(x):Id C(x,x,r(x))(J(t;x,x,r(x)),t)\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad \Gamma, x:A, \Delta(x,x,r(x)) \vdash t : C(x,x,r(x))} {\Gamma, x:A, \Delta(x,x,r(x)) \vdash q(x):Id_{C(x,x,r(x))}(J(t;x,x,r(x)) ,t)}

These rules may seem a little ad-hoc, but they are actually a particular case of the general notion of inductive type.

In terms of inductive types

Using inductive types the notion of identity types is encoded in a single line (see Licata 11, Shulman 12).

In Coq notation we can say

Inductive id {A} : A -> A -> Type := idpath : forall x, id x x.   

In other words, the identity type of AA is inductively generated by reflexivity x=xx = x (the “first law of thought”), in the same way that the natural numbers are inductively generated by zero and successor. From this, the above introduction, elimination, and computation rules are all derived automatically.

This is the approach to Martin-Lof identity types taken by implementations of homotopy type theory in proof assistants such as Coq or Agda. See, for instance, Overture.v

An essentially equivalent way to give the definition, due to Paulin-Mohring, is

Inductive id {A} (x:A) : A -> Type := idpath : id x x.   

The difference here is that now xx is a parameter of the inductive definition rather than an index. In other words, the first definition says “for each type AA, we have a type Id AId_A dependent on A×AA\times A, inductively defined by a constructor idpathidpath which takes an element x:Ax\colon A as input and yields output in Id A(x,x)Id_A(x,x)” while the second definition says “for each type AA and each element x:Ax\colon A, we have a type Id A(x)Id_A(x) dependent on AA, inductively defined by a constructor idpathidpath which takes no input and yields output in Id A(x)(x)Id_A(x)(x).” The two formulations can be proven equivalent, but sometimes one is more convenient than the other.

Extensionality and η\eta-conversion

Almost all types in type theory can be given both β-reduction? and η-reduction rules. β\beta-reduction specifies what happens when we apply an eliminator to a term obtained by a constructor; η\eta-reduction specifies the reverse. Above we have formulated only the β\beta-reduction rule for identity types; the η\eta-conversion rule would be the following:

Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓ,x:A,y:A,p:Id A(x,y),Δ(x,x,r(x))t:C(x,y,p)Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)J(t[x/y,r(x)/p];x,y,p)=t\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad \Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,x,r(x)) \vdash t : C(x,y,p)} {\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash J(t[x/y, r(x)/p];x,y,p) = t}

This says that if CC is a type which we can use the eliminator JJ to construct a term of, but we already have a term tt of that type, then if we restrict tt to reflexivity inputs and then apply JJ to construct a term of type CC, the result is the same as the term tt we started with. As in the β\beta-reduction rule, the == in the conclusion refers to definitional equality.

This η\eta-conversion rule has some very strong consequences. For instance, suppose x:Ax\colon A, y:Ay\colon A, and p:Id A(x,y)p\colon Id_A(x,y), and let CAC \coloneqq A. Then with t=xt=x, the η\eta-conversion rule tells us that x=J(x[x/y,r(x)/p];x,y,p)x = J(x[x/y,r(x)/p];x,y,p). And with t=yt=y, the η\eta-conversion rule tells us that y=J(y[x/y,r(x)/p];x,y,p)y = J(y[x/y,r(x)/p];x,y,p). But substituting xx for yy (and r(x)r(x) for pp) in the term yy simply yields the term xx, which is the same as the result of substituting xx for yy and r(x)r(x) for pp in the term xx. Thus, we have

x=J(x;x,y,p)=yx = J(x;x,y,p) = y

In other words, if Id A(x,y)Id_A(x,y) is inhabited (that is, xx and yy are propositionally equal) then in fact xx and yy are definitionally equal. Moreover, by a similar argument we can show that

p=J(p[x/y,r(x)/p];x,y,p)=J(r(x)[x/y,r(x)/p];x,y,p)=r(x).p = J(p[x/y, r(x)/p];x,y,p) = J(r(x)[x/y,r(x)/p];x,y,p) = r(x).

(Here we are eliminating into the type C(x,y,p)Id A(x,y)C(x,y,p) \coloneqq Id_A(x,y). The term r(x)r(x) may be regarded as belonging to this type, because we have already shown that xx and yy are definitionally equal.)

Thus, the definitional η\eta-conversion rule for identity types implies that the type theory is extensional in a very strong sense. (This was observed already in (Streicher).) For this reason, in homotopy type theory we do not assume the η\eta-conversion rule for identity types.

This sort of extensionality in type theory is also problematic for non-homotopical reasons: since type-checking in dependent type theory depends on definitional equality, but the above rule implies that definitional equality depends on inhabitation of identity types, this makes definitional equality and hence type-checking undecidable in the formal computational sense. Thus, η\eta-conversion for identity types is often omitted (as in Coq).

On the other hand, it is possible to prove a propositional version of η\eta-conversion using only the identity types as defined above without definitional η\eta-conversion. In other words, given the hypotheses of the above η\eta-conversion rule, we can construct a term belonging to the type

Id C(x,y,p)(J(t[x/y,r(x)/p];x,y,p),t). Id_{C(x,y,p)}(J(t[x/y, r(x)/p];x,y,p), t).

This has none of the bad consequences of definitional η\eta-conversion, and in particular does not imply that the type theory is extensional. The argument that p:Id A(x,y)p\colon Id_A(x,y) implies x=yx=y becomes the tautologous statement that if p:Id A(x,y)p\colon Id_A(x,y) then p:Id A(x,y)p\colon Id_A(x,y), while the subsequent argument that p=r(x)p= r(x) fails because xx and yy are no longer definitionally equal, so r(x)r(x) does not have type Id A(x,y)Id_A(x,y). We can transport it along pp to obtain a term of this type, but then we obtain only that pp is equal to the transport of r(x)r(x) along pp, which is a perfectly intensional/homotopical statement.

Definition in observational type theory

Identity types in observational type theory and higher observational type theory are defined in a different manner than they are in Martin-Löf type theory.

In higher observational type theory, identity types have the same formation rule as Martin-Löf identity types do:

ΓA:TypeΓ,x:A,y:AId A(x,y):Type\frac{\Gamma \vdash A:Type} {\Gamma, x:A, y:A \vdash Id_A(x,y):Type}

However, it does not have global elimination or computation rules. Instead, it has a local computation rule for each particular type. For example, the identity type of the product type A×BA \times B has the following computation rule:

Id A×B(s,t)Id A(π 1s,π 1t)×Id B(π 2s,π 2t)Id_{A \times B} (s, t) \equiv Id_A(\pi_1 s, \pi_1 t) \times Id_B (\pi_2 s, \pi_2 t)

For types in universes

We are working in a dependent type theory with Tarski-style universes.

The identity types in a universe in higher observational type theory have the following formation rule:

A:𝒰a:𝒯 𝒰(A)b:𝒯 𝒰(A)id A(a,b):𝒰\frac{A:\mathcal{U} \quad a:\mathcal{T}_\mathcal{U}(A) \quad b:\mathcal{T}_\mathcal{U}(A)}{\mathrm{id}_A(a, b):\mathcal{U}}

We define a general congruence term called ap

x:Af:Bp:id A(a,a )ap x.f(p):id B(f[a/x],f[a /x])\frac{x:A \vdash f:B \quad p:\mathrm{id}_A(a, a^{'})}{\mathrm{ap}_{x.f}(p):\mathrm{id}_B(f[a/x], f[a^{'}/x])}

and the reflexivity terms:

a:Arefl a:id A(a,a)\frac{a:A}{\mathrm{refl}_{a}:\mathrm{id}_A(a, a)}

and computation rules for identity functions

ap x.x(p)p\mathrm{ap}_{x.x}(p) \equiv p

and for constant functions yy

ap x.y(p)refl y\mathrm{ap}_{x.y}(p) \equiv \mathrm{refl}_{y}

Thus, ap is a higher dimensional explicit substitution. There are definitional equalities

ap x.f(refl a)refl f[a/x]\mathrm{ap}_{x.f}(\mathrm{refl}_{a}) \equiv \mathrm{refl}_{f[a/x]}
ap y.g(ap x.f(p))ap x.g[f/y](p)\mathrm{ap}_{y.g}(\mathrm{ap}_{x.f}(p)) \equiv \mathrm{ap}_{x.g[f/y]}(p)
ap x.t(p)refl t\mathrm{ap}_{x.t}(p) \equiv \mathrm{refl}_{t}

for constant term tt.

For universes

Let A 𝒰BA \cong_\mathcal{U} B be the type of bijective correspondences between two terms of a universe A:𝒰A:\mathcal{U} and B:𝒰B:\mathcal{U}, and let id 𝒰(A,B)\mathrm{id}_\mathcal{U}(A, B) be the identity type between two terms of a universe A:𝒰A:\mathcal{U} and B:𝒰B:\mathcal{U}. Then there are rules

R:A 𝒰BΔ(R):id 𝒰(A,B)P:id 𝒰(A,B)(P):A 𝒰BR:A 𝒰B(Δ(R))R\frac{R:A \cong_\mathcal{U} B}{\Delta(R):\mathrm{id}_\mathcal{U}(A, B)} \qquad \frac{P:\mathrm{id}_\mathcal{U}(A, B)}{\nabla(P):A \cong_\mathcal{U} B} \qquad \frac{R:A \cong_\mathcal{U} B}{\nabla(\Delta(R)) \equiv R}

Identity types in universes and singleton contractibility

Given a term of a universe A:𝒰A:\mathcal{U}

id 𝒯 𝒰(A)π 1((refl A))\mathrm{id}_{\mathcal{T}_\mathcal{U}(A)} \equiv \pi_1(\nabla(\mathrm{refl}_A))

with terms representing singleton contractibility?.

π 1(π 2((refl A)): a:𝒯 𝒰(A)isContr( b:𝒯 𝒰(A)id 𝒯 𝒰(A)(a,b))\pi_1(\pi_2(\nabla(\mathrm{refl}_A)):\prod_{a:\mathcal{T}_\mathcal{U}(A)} \mathrm{isContr}\left(\sum_{b:\mathcal{T}_\mathcal{U}(A)} \mathrm{id}_{\mathcal{T}_\mathcal{U}(A)}(a, b)\right)
π 2(π 2((refl A))): b:𝒯 𝒰(A)isContr( a:𝒯 𝒰(A)id 𝒯 𝒰(A)(a,b))\pi_2(\pi_2(\nabla(\mathrm{refl}_A))):\prod_{b:\mathcal{T}_\mathcal{U}(A)} \mathrm{isContr}\left(\sum_{a:\mathcal{T}_\mathcal{U}(A)} \mathrm{id}_{\mathcal{T}_\mathcal{U}(A)}(a, b)\right)

Definition in cubical type theory

The primary identity types are the nondependent cubical path types in cubical type theory. Like the identity types in higher observational type theory, they do not satisfy the definitional version of identification elimination; only the propositional version of identification elimination. See cubical path type for more information on the construction of the cubical path types.

Some cubical type theories include a second identity type which satisfies the definitional version of identification elimination. This is called Swan's identity type?, and is defined by the following rules:

Identity types in cubical type theory are called path types and are defined using a primitive interval.

Categorical semantics

We discuss the categorical semantics for identity types in the extensional case, and identity types in the categorical semantics of homotopy type theory in the intensional case.

In categorical models of extensional type theory, generally every morphism of the category is allowed to represent a dependent type, and the extensional identity types are represented by diagonal maps AA×AA\to A\times A.

By contrast, in models of intensional type theory, there is only a particular class of display maps or fibrations which are allowed to represent dependent types, and intensional identity types are represented by path objects PAA×AP A \to A \times A.

Both of these cases apply in particular to models in the category of contexts of the type theory itself, i.e. the term model.


By the standard construction of mapping path spaces out of path space objects, the existence of identity types allows one to construct a weak factorization system.

Conversely, since any weak factorization system gives rise to path objects by factorization of diagonal maps, one may hope to construct a model of type theory with identity types in a category equipped with a WFS (L,R)(L,R). There are four obstacles in the way of such a construction.

  1. In order to handle the additional context Δ\Delta in the explicit definition above, it turns out to be necessary to assume that LL-maps are preserved by pullback along RR-maps between RR-objects. (Such a condition is also necessary in order to interpret type-theoretic dependent products in a locally cartesian closed category.)

  2. This enables us to define identity types with their elimination and computation rules “locally”, i.e. for each type individually. However, every construction in type theory is stable under substitution. This means that if y:YA(y):Typey\colon Y\vdash A(y)\colon Type is a dependent type and f:XYf\colon X\to Y is a morphism, then the identity type x:XId A(f(x))(,):Typex\colon X \vdash Id_{A(f(x))}(-,-)\colon Type is the same whether we first construct Id A(y)Id_{A(y)} and then substitute f(x)f(x) for yy, or first substitute f(x)f(x) for yy to obtain A(f(x))A(f(x)) and then construct its identity type. In order for this to hold up to isomorphism, we need to require that the WFS have stable path objects — a choice of path object data in each slice category which is preserved by pullback. In Warren 2008 it is shown that any simplicial model category in which the cofibrations are the monomorphisms can be equipped with stable path objects, while Garner & van den Berg 2011 it is shown that the presence of internal path-categories also suffices.

  3. The eliminator term JJ of identity types in type theory is also preserved by substitution. This imposes an additional coherence requirement which is tricky to obtain categorically. See Warren 2008 and Garner & van den Berg 2011 for methods that ensure this, such as by invoking an algebraic weak factorization system. It can also be handled a la Voevodsky by using a (possibly univalent) universe.

  4. Finally, substitution in type theory is strictly functorial/associative, whereas it is modeled categorically by pullback which is generally not strictly so. This is a general issue with the categorical interpretation of dependent type theory, not something specific to identity types. It can be resolved by passing to a split fibration which is equivalent to the codomain fibration, or by making use of a universe. See categorical model of dependent types.

Interpretation in a type-theoretic model category

Assume then that a category 𝒞\mathcal{C} with suitable WFSs has been chosen, for instance a type-theoretic model category. Then

  • The interpretation of a type A:Type \vdash A : Type is as a fibrant object [A:Type][\vdash A : Type] which we will just write “AA” for short.

  • type formation

    The identity type a,b:AId A(a,b):Typea, b : A \vdash Id_A(a,b) : Type is interpreted as the path space object fibration

    A I A×A \array{ A^I \\ \downarrow \\ A \times A }
  • term introduction

    By definition of path space object, there exists a lift σ\sigma in

    A I σ A (id,id) A×A. \array{ && A^I \\ & {}^{\mathllap{\sigma}}\nearrow& \downarrow \\ A &\stackrel{(id,id)}{\to}& A \times A } \,.

    By the universal property of the pullback this is equivalently a section of the pullback of the path space object along the diagonal morphism (id,id):AA×A(id,id) : A \to A \times A.

    (id,id) *A I A I σ A = A (id,id) A×A. \array{ && (id,id)^* A^I &\to& A^I \\ &{}^{\mathllap{\sigma}}\nearrow& \downarrow & & \downarrow \\ A &=& A &\stackrel{(id,id)}{\to}& A \times A } \,.

    Since (id,id) *A I(id, id)^* A^I is the interpretation of the substitution
    a:AId A(a,a):Typea : A \vdash Id_A (a,a) : Type in this sense σ\sigma is now the interpretation of a term a:Ar A:Id A(a,a)a : A \vdash r_A : Id_A (a,a).

  • term elimination

    A type depending on an identity type

    a,b:A,p:Id A(a,b)C(a,b,p) a, b : A, p : Id_A(a,b) \vdash C(a,b,p)

    is interpreted as a fibration

    C A I. \array{ C \\ \downarrow \\ A^I } \,.

    The substitution C(a,a,r a)C(a,a,r_a) is interpreted by the pullback

    (id,id) *C C A (id,id) A×A. \array{ (id,id)^* C &\to& C \\ \downarrow && \downarrow \\ A &\stackrel{(id,id)}{\to}& A \times A } \,.

    Therefore a term t:C(a,a,r a)t : C(a,a,r_a) is interpreted as a section of this pullback

    (id,id) *C C t A = A (id,id) A×A. \array{ && (id,id)^* C &\to& C \\ &{}^{\mathllap{t}}\nearrow& \downarrow && \downarrow \\ A &=& A &\stackrel{(id,id)}{\to}& A \times A } \,.

    By the universal property of the pullback, this is equivalently a morphism tt in

    C t A (id,id) A×A. \array{ && C \\ & {}^{\mathllap{t}}\nearrow & \downarrow \\ A &\stackrel{(id,id)}{\to}& A \times A } \,.

    The elimination rule says that given such tt, there exists a compatible section of CA IC \to A^I. If we redraw the previous diagram as a square, then this section is a lift in that diagram

    A C r A I = A I. \array{ A &\to& C \\ {}^{\mathllap{r}}\downarrow &\nearrow& \downarrow \\ A^I &=& A^I } \,.

    In particular, if CC itself is the pullback of a fibration DBD \to B along a morphism A IBA^I \to B, then rr has the left lifting property also against that fibration

    A C D r A I = A I B. \array{ A &\to& C &\to& D \\ {}^{\mathllap{r}}\downarrow &\nearrow& \downarrow && \downarrow \\ A^I &=& A^I &\to& B } \,.

    So the term elimination rule says that the interpretaton AA IA \to A^I of a:Ar(a):Id A(a,a)a : A \vdash r(a) : Id_A (a,a) has the left lifting property against all fibrations, hence that AA IA \to A^I is to be interpreted as an acyclic cofibration.

Weak ω\omega-groupoids

Some of the first work noticing the homotopical / higher-categorical interpretation of identity types (see below) focused on the fact that the tower of iterated identity types of a type has the structure of an internal algebraic ∞-groupoid.

In retrospect, this is roughly an algebraic version of the standard fact that every object of a model category (or more generally a category of fibrant objects or a category with a weak factorization system) admits a simplicial resolution which is an internal Kan complex, i.e. a nonalgebraic \infty-groupoid. Note, however, that the first technical condition above (stability of LL-maps under pullback along RR-maps) seems to be necessary for the algebraic version of the result to go through.


Explicit definition

The induction principle for identity types (also known as “path induction” or the “J-rule”) is first stated in

  • Per Martin-Löf, §1.7 and p. 94 of: An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80 Pages 73-118, Elsevier 1975 (doi:10.1016/S0049-237X(08)71945-1, CiteSeer)

and in the modern form of inference rules in

  • Bengt Nordström, Kent Petersson, Jan M. Smith, §8.1 of: Programming in Martin-Löf’s Type Theory, Oxford University Press (1990) [webpage, pdf, pdf]

with early survey in §1.0.1 of:

  • Michael Warren, Homotopy theoretic aspects of constructive type theory, PhD thesis (2008) [pdf, pdf]

See also (?):

The observation that the Id-induction principle (the J-rule) is equivalent to transport (“salva veritate”) together with contractibility of the type of identifications (“by reversal of identifications”) is stated in:

further highlighted in

and the proof of the equivalence is spelled out in:

  • Lennard Götz, §4.2 of: Martin-Löf’s J-rule, LMU (2018) [pdf]

Discussion of issues of extensional/intensional type theory:

The observation that Id

As inductive types

In (higher) observational type theory

Weak factorization systems

Types as \infty-groupoids

The observation that identity types witness groupoid and infinity-groupoid-structure:

For more see the references at homotopy type theory.

See also

Last revised on September 26, 2022 at 04:07:37. See the history of this page for a list of all contributions to it.