5.8 Identity types and identity systems

We now wish to point out that the identity types, which play so central a role in homotopy type theory, may also be considered to be defined inductively. Specifically, they are an “inductive family” with indices, in the sense of §5.7 (http://planetmath.org/57generalizationsofinductivetypes). In fact, there are two ways to describe identity types as an inductive family, resulting in the two inductionMathworldPlanetmath principles described in http://planetmath.org/node/87533Chapter 1, path induction and based path induction.

In both definitions, the type A is a parameter. For the first definition, we inductively define a family =A:AA𝒰, with two indices belonging to A, by the following constructor:

  • for any a:A, an element 𝗋𝖾𝖿𝗅A:a=Aa.

By analogyMathworldPlanetmath with the other inductive families, we may extract the induction principle from this definition. It states that given any C:(a,b:A)(a=Ab)𝒰, along with d:(a:A)C(a,a,𝗋𝖾𝖿𝗅a), there exists f:(a,b:A)(p:a=Ab)C(a,b,p) such that f(a,a,𝗋𝖾𝖿𝗅a)d(a). This is exactly the path induction principle for identity types.

For the second definition, we consider one element a0:A to be a parameter along with A:𝒰, and we inductively define a family (a0=A):A𝒰, with one index belonging to A, by the following constructor:

  • an element 𝗋𝖾𝖿𝗅a0:a0=Aa0.

Note that because a0:A was fixed as a parameter, the constructor 𝗋𝖾𝖿𝗅a0 does not appear inside the inductive definition as a function, but only an element. The induction principle for this definition says that given C:(b:A)(a0=Ab)𝒰 along with an element d:C(a0,𝗋𝖾𝖿𝗅a0), there exists f:(b:A)(p:a0=Ab)C(b,p) with f(a0,𝗋𝖾𝖿𝗅a0)d. This is exactly the based path induction principle for identity types.

The view of identity types as inductive types has historically caused some confusion, because of the intuition mentioned in §5.1 (http://planetmath.org/51introductiontoinductivetypes) that all the elements of an inductive type should be obtained by repeatedly applying its constructors. For ordinary inductive types such as 𝟐 and , this is the case: we saw in (http://planetmath.org/18thetypeofbooleans#1 ) that indeed every element of 𝟐 is either 0𝟐 or 1𝟐, and similarly one can prove that every element of is either 0 or a successorMathworldPlanetmathPlanetmathPlanetmath.

However, this is not true for identity types: there is only one constructor 𝗋𝖾𝖿𝗅, but not every path is equal to the constant path. More precisely, we cannot prove, using only the induction principle for identity types (either one), that every inhabitant of a=Aa is equal to 𝗋𝖾𝖿𝗅a. In order to actually exhibit a counterexample, we need some additional principle such as the univalence axiom — recall that in Example 3.1.9 (http://planetmath.org/31setsandntypes#Thmpreeg6) we used univalence to exhibit a particular path 𝟐=𝒰𝟐 which is not equal to 𝗋𝖾𝖿𝗅𝟐.

The point is that, as validated by the study of homotopy-initial algebrasMathworldPlanetmathPlanetmathPlanetmath, an inductive definition should be regarded as freely generated by its constructors. Of course, a freely generated structureMathworldPlanetmath may contain elements other than its generatorsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath: for instance, the free group on two symbols x and y contains not only x and y but also words such as xy, yx-1y, and x3y2x-2yx. In general, the elements of a free structure are obtained by applying not only the generators, but also the operationsMathworldPlanetmath of the ambient structure, such as the group operationsMathworldPlanetmath if we are talking about free groups.

In the case of inductive types, we are talking about freely generated types — so what are the “operations” of the structure of a type? If types are viewed as like sets, as was traditionally the case in type theoryPlanetmathPlanetmath, then there are no such operations, and hence we expect there to be no elements in an inductive type other than those resulting from its constructors. In homotopy type theory, we view types as like spaces or -groupoidsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, in which case there are many operations on the paths (concatenation, inversionMathworldPlanetmathPlanetmath, etc.) — this will be important in http://planetmath.org/node/87579Chapter 6 — but there are still no operations on the objects (elements). Thus, it is still true for us that, e.g., every element of 𝟐 is either 0𝟐 or 1𝟐, and every element of is either 0 or a successor.

However, as we saw in http://planetmath.org/node/87569Chapter 2, viewing types as -groupoids entails also viewing functions as functorsMathworldPlanetmath, and this includes type families B:A𝒰. Thus, the identity type (a0=A), viewed as an inductive type family, is actually a freely generated functor A𝒰. Specifically, it is the functor F:A𝒰 freely generated by one element 𝗋𝖾𝖿𝗅a0:F(a0). And a functor does have operations on objects, namely the action of the morphismsMathworldPlanetmathPlanetmath (paths) of A.

In category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath, the Yoneda lemma tells us that for any category A and object a0, the functor freely generated by an element of F(a0) is the representable functorPlanetmathPlanetmath homA(a0,). Thus, we should expect the identity type (a0=A) to be this representable functor, and this is indeed exactly how we view it: (a0=Ab) is the space of morphisms (paths) in A from a0 to b.

One reason for viewing identity types as inductive families is to apply the uniqueness principles of §5.2 (http://planetmath.org/52uniquenessofinductivetypes),§5.5 (http://planetmath.org/55homotopyinductivetypes). Specifically, we can characterize the family of identity types of a type A, up to equivalence, by giving another family of types over A×A satisfying the same induction principle. This suggests the following definitions and theoremMathworldPlanetmath.

Definition 5.8.1.

Let A be a type and a0:A an element.

  • A pointed predicateMathworldPlanetmathPlanetmath over (A,a0) is a family R:A𝒰 equipped with an element r0:R(a0).

  • For pointed predicates (R,r0) and (S,s0), a family of maps g:(b:A)R(b)S(b) is pointed if g(a0,r0)=s0. We have

  • An identityPlanetmathPlanetmathPlanetmath system at a0 is a pointed predicate (R,r0) such that for any type family D:(b:A)R(b)𝒰 and d:D(a0,r0), there exists a function f:(b:A)(r:R(b))D(b,r) such that f(a0,r0)=d.

Theorem 5.8.2.

For a pointed predicate (R,r0), the following are logically equivalent.

  1. 1.

    (R,r0) is an identity system at a0.

  2. 2.

    For any pointed predicate (S,s0), the type 𝗉𝗉𝗆𝖺𝗉(R,S) is contractibleMathworldPlanetmath.

  3. 3.

    For any b:A, the function 𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍R(¯,r0):(a0=Ab)R(b) is an equivalence.

  4. 4.

    The type (b:A)R(b) is contractible.

Note that the equivalences 123 are a version of Lemma 5.5.4 (http://planetmath.org/55homotopyinductivetypes#Thmprelem1) for identity types a0=A, regarded as inductive families varying over one element of A. Of course, 24 are mere propositions, so that logical equivalence implies actual equivalence. (Condition 1 is also a mere proposition, but we will not prove this.)


First, assume 1 and let (S,s0) be a pointed predicate. Define D(b,r):S(b) and d:s0:S(a0)D(a0,r0). Since R is an identity system, we have f:(b:A)R(b)S(b) with f(a0,r0)=s0; hence 𝗉𝗉𝗆𝖺𝗉(R,S) is inhabited. Now suppose (f,fr),(g,gr):𝗉𝗉𝗆𝖺𝗉(R,S), and define D(b,r):(f(b,r)=g(b,r)), and let d:fr\centerdotgr-1:f(a0,r0)=s0=g(a0,r0). Then again since R is an identity system, we have h:(b:A)(r:R(b))D(b,r) such that h(a0,r0)=fr\centerdotgr-1. By the characterizationMathworldPlanetmath of paths in Σ-types and path types, these data yield an equality (f,fr)=(g,gr). Hence 𝗉𝗉𝗆𝖺𝗉(R,S) is an inhabited mere proposition, and thus contractible; so 2 holds.

Now suppose 2, and define S(b):(a0=b) with s0:𝗋𝖾𝖿𝗅a0:S(a0). Then (S,s0) is a pointed predicate, and λb.λp.𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍R(p,r):(b:A)S(b)R(b) is a pointed family of maps from S to R. By assumptionPlanetmathPlanetmath, 𝗉𝗉𝗆𝖺𝗉(R,S) is contractible, hence inhabited, so there also exists a pointed family of maps from R to S. And the composites in either direction are pointed families of maps from R to R and from S to S, respectively, hence equal to identities since 𝗉𝗉𝗆𝖺𝗉(R,R) and 𝗉𝗉𝗆𝖺𝗉(S,S) are contractible. Thus 3 holds.

Now supposing 3, condition 4 follows from Lemma 3.11.8 (http://planetmath.org/311contractibility#Thmprelem5), using the fact that Σ-types respect equivalences (the “if” direction of Theorem 4.7.7 (http://planetmath.org/47closurepropertiesofequivalences#Thmprethm4)).

Finally, assume 4, and let D:(b:A)R(b)𝒰 and d:D(a0,r0). We can equivalently express D as a family D:((b:A)R(b))𝒰. Now since (b:A)R(b) is contractible, we have


Moreover, since the path types of a contractible type are again contractible, we have p((a0,r0))=𝗋𝖾𝖿𝗅(a0,r0). Define f(u):𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍D(p(u),d), yielding f:(u:(b:A)R(b))D(u), or equivalently f:(b:A)(r:R(b))D(b,r). Finally, we have


Thus, 1 holds. ∎

We can deduce a similarMathworldPlanetmathPlanetmath result for identity types =A, regarded as a family varying over two elements of A.

Definition 5.8.3.

An identity system over a type A is a family R:AAU equipped with a function r0:(a:A)R(a,a) such that for any type family D:(a,b:A)R(a,b)U and d:(a:A)D(a,a,r0(a)), there exists a function f:(a,b:A)(r:R(b))D(a,b,r) such that f(a,a,r0(a))=d(a) for all a:A.

Theorem 5.8.4.

For R:AAU equipped with r0:(a:A)R(a,a), the following are logically equivalent.

  1. 1.

    (R,r0) is an identity system over A.

  2. 2.

    For all a0:A, the pointed predicate (R(a0),r0(a0)) is an identity system at a0.

  3. 3.

    For any S:AA𝒰 and s0:(a:A)S(a,a), the type


    is contractible.

  4. 4.

    For any a,b:A, the map 𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍R(a)(¯,r0(a)):(a=Ab)R(a,b) is an equivalence.

  5. 5.

    For any a:A, the type (b:A)R(a,b) is contractible.


The equivalence 12 follows exactly the proof of equivalence between the path induction and based path induction principles for identity types; see §1.12 (http://planetmath.org/112identitytypes). The equivalence with 4 and 5 then follows from Theorem 5.8.2 (http://planetmath.org/58identitytypesandidentitysystems#Thmprethm1), while 3 is straightforward. ∎

One reason this characterization is interesting is that it provides an alternative way to state univalence and function extensionality. The univalence axiom for a universePlanetmathPlanetmath 𝒰 says exactly that the type family


together with 𝗂𝖽:(A:𝒰)(AA) satisfies Theorem 5.8.4 (http://planetmath.org/58identitytypesandidentitysystems#Thmprethm2)4. Therefore, it is equivalentMathworldPlanetmathPlanetmathPlanetmath to the corresponding version of 1, which we can state as follows.

Corollary 5.8.5 (Equivalence induction).

Given any type family D:(A,B:U)(AB)U and function d:(A:U)D(A,A,idA), there exists f:(A,B:U)(e:AB)D(A,B,e) such that f(A,A,idA)=d(A) for all A:U.

In other words, to prove something about all equivalences, it suffices to prove it about identity mapsMathworldPlanetmath. We have already used this principle (without stating it in generality) in Lemma 4.1.1 (http://planetmath.org/41quasiinverses#Thmprelem1).

Similarly, function extensionality says that for any B:A𝒰, the type family


together with λf.λa.𝗋𝖾𝖿𝗅f(a) satisfies Theorem 5.8.4 (http://planetmath.org/58identitytypesandidentitysystems#Thmprethm2)4. Thus, it is also equivalent to the corresponding version of 1.

Corollary 5.8.6 (Homotopy induction).

Given any D:(f,g:(a:A)B(a))(fg)U and d:(f:(a:A)B(a))D(f,f,λx.reflf(x)), there exists


such that k(f,f,λx.reflf(x))=d(f) for all f.

Title 5.8 Identity types and identity systems