Chapter 77Core route

Identity Types

Addition on the natural numbers (construction 28.23) already poses the problem. Its defining equations make $n + 0 \equiv n$ , but for a variable $n$ no computation rule turns $0 + n$ into $n$ . Nevertheless induction proves that the two terms agree. To state that proof inside the theory we need a type whose elements are evidence that two terms are equal.

Judgmental equality is a judgment, not a type: it licenses conversion, but there is no context declaration $p : a \equiv b$ and no eliminator for such a declaration inside the theory. The intensional identity type ${Id}_{A} (a, b)$ internalizes equality as such a type. Its sole constructor is reflexivity. The target ${Id}_{N} (0 + n, n)$ is inhabited by natural-number induction; the successor case must turn evidence for $0 + n = n$ into evidence after applying successor to both endpoints.

The rules of the identity type

The identity family is the family $({Id}_{A} (a, b))_{a, b : A}$ generated over the diagonal by the single constructor reflexivity; its eliminator $J$ is induction over that family.

Definition 30.1 — Identity types ¶

An identification of $a$ with $b$ is an element of ${Id}_{A} (a, b)$ . Reflexivity introduces an identification, and $J$ eliminates one by proving the reflexivity case of a family over both endpoints and the identification. Premises recoverable by convention 26.14 are omitted.

Γ ⊢ a : A

Γ ⊢ b : A

Γ ⊢ {Id}_{A} (a, b) type

Id-form

Γ ⊢ A : U_{i}

Γ ⊢ a : A

Γ ⊢ b : A

Γ ⊢ {Id}_{A} (a, b) : U_{i}

Id-form-

Γ ⊢ a : A

Γ ⊢ {refl}_{a} : {Id}_{A} (a, a)

Id-intro

Γ, x : A, y : A, p : {Id}_{A} (x, y) ⊢ C type

Γ, z : A ⊢ c : C [z / x, z / y, {refl}_{z} / p]

Γ ⊢ q : {Id}_{A} (a, b)

Γ ⊢ J (x . y . p . C; z . c; q) : C [a / x, b / y, q / p]

Id-elim

Γ, x : A, y : A, p : {Id}_{A} (x, y) ⊢ C type

Γ, z : A ⊢ c : C [z / x, z / y, {refl}_{z} / p]

Γ ⊢ a : A

Γ ⊢ J (x . y . p . C; z . c; {refl}_{a}) \equiv c [a / z] : C [a / x, a / y, {refl}_{a} / p]

Id-comp

The closure rule Id-form- $U$ is available only with the universe hierarchy of definition 29.1; Id-form, Id-intro, Id-elim, and Id-comp do not presuppose universes. There is no uniqueness ( $η$ ) rule; cf. remark 30.8. As required by convention 27.1, each operator also respects judgmental equality in all its classified arguments. The dependent instance for $J$ is stated explicitly in remark 30.2.

Referenced from 29 locations

In the raw binding signature, ${Id}_{A} (a, b)$ has arity $(0, 0, 0)$ , ${refl}_{a}$ has arity $(0)$ , and the fully annotated eliminator is $J_{A; a; b} (x . y . p . C; z . c; q) .$ It has arity $(0, 0, 0, 3, 1, 0)$ : the first three arguments record $A, a, b$ ; it binds $x, y, p$ in $C$ and $z$ in $c$ . The notation in definition 30.1 suppresses $A, a, b$ when its typing judgment determines them.

When the optional lifting package of definition 29.10 is present, extend its strict code equations by

Γ ⊢ A : U_{i}

Γ ⊢ a : A

Γ ⊢ b : A

Γ ⊢ {Lift}_{i} ({Id}_{A} (a, b)) \equiv {Id}_{{Lift}_{i} A} (a, b) : U_{i + 1}

Lift-Id

The endpoints on the right are well typed by conversion along Lift-El.

Remark 30.2 — The congruence instances ¶

Identity formation has the rule

Γ ⊢ A \equiv A^{'} type

Γ ⊢ a \equiv a^{'} : A

Γ ⊢ b \equiv b^{'} : A

Γ ⊢ {Id}_{A} (a, b) \equiv {Id}_{A^{'}} (a^{'}, b^{'}) type

Id-form-eq

For elimination, put $Δ : = Γ, x : A, y : A, p : {Id}_{A} (x, y)$ . After context conversion has placed all primed data in the same displayed contexts, the rule is

Γ ⊢ A \equiv A^{'} type

Δ ⊢ C \equiv C^{'} type

Γ, z : A ⊢ c \equiv c^{'} : C [z / x, z / y, {refl}_{z} / p]

Γ ⊢ a \equiv a^{'} : A

Γ ⊢ b \equiv b^{'} : A

Γ ⊢ q \equiv q^{'} : {Id}_{A} (a, b)

Γ ⊢ J (x . y . p . C; z . c; q) \equiv J (x . y . p . C^{'}; z . c^{'}; q^{'}) : C [a / x, b / y, q / p]

Id-elim-eq

In the conclusion, the left printed term abbreviates the raw constructor $J_{A; a; b}$ and the right one abbreviates $J_{A^{'}; a^{'}; b^{'}}$ . Thus the first premise and the two endpoint premises also compare the three newly explicit raw annotations; they are not discarded by the notation. Applying Id-elim-eq to the six displayed equality premises first gives the right-hand eliminator at its naturally formed classifier $C^{'} [a^{'} / x, b^{'} / y, q^{'} / p]$ . Use the following two local equations:

symmetry of equal substitution in $a, b, q$ ;
symmetry of the substituted motive equality.

They give the classifier chain $\begin{aligned} C^{'} [a^{'} / x, b^{'} / y, q^{'} / p] & \overset{(1)}{\equiv} C^{'} [a / x, b / y, q / p] \\ \overset{(2)}{\equiv} C [a / x, b / y, q / p] . \end{aligned}$ Conversion along this chain places the right-hand $J$ term at the result type used in the conclusion. The congruence rule for $refl$ is the unary special case. These are the exact instances used below.

Referenced from 5 locations

Convention 30.3 — Notation ¶

Elements of ${Id}_{A} (a, b)$ are called identifications of $a$ with $b$ . We suppress annotations that are determined by the judgment: in particular, the printed term $J (x . y . p . C; z . c; q)$ abbreviates the raw term $J_{A; a; b} (x . y . p . C; z . c; q)$ when $q : {Id}_{A} (a, b)$ . We also write $refl$ for ${refl}_{a}$ , and $J (z . c; q)$ when the expected type determines the motive. Throughout this part we retain the fully typed notation ${Id}_{A} (a, b)$ .

Referenced from 2 locations

Identity Types

Lemma 30.4 — Judgmental equality yields identifications ¶

If $Γ ⊢ a \equiv b : A$ , then $Γ ⊢ {refl}_{a} : {Id}_{A} (a, b)$ .

Referenced from 4 locations

Identity Types

Proof of Lemma 30.4 — Judgmental equality yields identifications

Proof. By Id-intro, $Γ ⊢ {refl}_{a} : {Id}_{A} (a, a)$ . From $Γ ⊢ a \equiv b : A$ the congruence rule $I d - f o r m - e q$ of remark 30.2 gives $Γ ⊢ {Id}_{A} (a, a) \equiv {Id}_{A} (a, b) type$ , and the conversion rule concludes $Γ ⊢ {refl}_{a} : {Id}_{A} (a, b)$ . ◻

Remark 30.5 ¶

The converse of lemma 30.4 — from $Γ ⊢ q : {Id}_{A} (a, b)$ conclude $Γ ⊢ a \equiv b : A$ — is the equality reflection rule. It is not a rule of this theory; adding it changes an identification hypothesis into a judgmental equality. Here an identification may be used only through $J$ ; it does not silently become a conversion.

Referenced from 2 locations

Identity Types

Convention 30.6 — The path-induction pattern ¶

The path-induction pattern is the admissible use of $J$ specified by the genericity and computation obligations below. Suppose the context has three pairwise distinct variables $a : A$ , $b : A$ , and $q : {Id}_{A} (a, b)$ . Move any independent later hypotheses to the left by exchange, and abstract into $Π$ -types every remaining later hypothesis. The resulting goal must be an instance $C [a / x, b / y, q / p]$ of a well-formed motive $Γ, x : A, y : A, p : {Id}_{A} (x, y) ⊢ C type$ , where $x, y, p$ are pairwise distinct and ${x, y, p} \cap dom (Γ) = \emptyset$ . Thus the endpoint variables $x, y$ and identification variable $p$ must all be generic in the displayed motive. Under these conditions, Id-elim reduces the construction to an element of $C [z / x, z / y, {refl}_{z} / p]$ for $z \notin dom (Γ) \cup {x, y, p}$ . We abbreviate this step by the phrase

“by identity induction on $q$ , we may assume $b$ is $a$ and $q$ is ${refl}_{a}$ .”

Using the phrase carries two obligations. (i) Genericity. The displayed motive is the test: if it is not well formed, the phrase cannot be used. One must first generalize the fixed hypotheses that obstruct it. In particular, from $x : A, p : {Id}_{A} (x, x)$ one cannot manufacture two independent endpoint variables merely by calling both of them $x$ ; doing so would falsely derive that every loop is reflexivity. More precisely, that apparent conclusion comes from an ill-formed motive, not from an instance of Id-elim. When only the left or only the right endpoint can be generalized, the corresponding based induction orientation applies. If neither a left-based nor a right-based motive is well formed, identity induction is unavailable. (ii) Computation. The term so constructed computes by Id-comp when $q$ is $refl$ ; we record this judgmental equality with each construction, since later well-typedness frequently depends on it. Inferring $C$ from a concrete goal is a higher-order matching problem, not a primitive kernel operation. Tactics named induction, destruct, or cases automate that search; a motive is not type correct failure usually means that the genericity obligation in (i) was not met and more hypotheses must be generalized.

Referenced from 4 locations

Identity Types

Remark 30.7 — The family is inductive, not the type ¶

The rule Id-elim does not make every identification a reflexivity. It says instead that the family $({Id}_{A} (x, y))_{x, y : A}$ , considered over the whole context $x : A, y : A$ , is generated by the diagonal elements ${refl}_{x}$ . A map out of the total family is determined by its values on the diagonal; about a single fiber ${Id}_{A} (a, b)$ with fixed endpoints, the rule says nothing. The laws relating identifications are themselves inhabited identity types, not additional judgmental equations.

Referenced from 2 locations

Identity Types

Remark 30.8 — No η -rule ¶

For $Σ$ -types the uniqueness rule is $u \equiv ({pr}_{1} (u), {pr}_{2} (u)),$ so every element is judgmentally a pair (definition 27.9). There is no uniformly well-typed expression of the form $q \equiv refl$ : when $q : {Id}_{A} (a, b)$ , the term ${refl}_{a}$ naturally has type ${Id}_{A} (a, a)$ , and the two types need not be judgmentally equal. The intensional identity type therefore has a mapping-out principle but no judgmental uniqueness principle.

Referenced from 3 locations

Identity Types

Exercise 30.1 ¶

★☆☆ Using definition 26.22 and Id-intro, write the full derivation tree of the judgment $x : A ⊢ {refl}_{x} : {Id}_{A} (x, x)$ from the premise $\cdot ⊢ A type$ , displaying every application of the variable and context-formation rules.

Referenced from 3 locations

Exercise 30.2 ¶

★★☆

Formulate the based variant of the formation rule: from $Γ ⊢ a : A$ conclude $Γ, y : A ⊢ {Id}_{A} (a, y) type$ . Show that in the presence of the structural rules (definition 26.22) it follows from Id-form, and recover Id-form from it by substituting an arbitrary $b : A$ for $y$ . Finally explain why reflexivity already has the single based rule $\frac{Γ ⊢ a : A}{Γ ⊢ {refl}_{a} : {Id}_{A} (a, a)},$ so there is no second introduction variant to compare.

Referenced from 3 locations

Transport and the derived operations

For $q : {Id}_{A} (a, b)$ and $u : B [a / x]$ , transport carries $u$ along $q$ , giving ${tr}_{q}^{x . B} (u) : B [b / x]$ . Inverse, concatenation, and congruence are likewise defined by identity induction, and each computes at reflexivity.

Construction 30.9 — Transport ¶

Let $Γ, x : A ⊢ B type$ and $Γ ⊢ q : {Id}_{A} (a, b)$ . There is a term $Γ ⊢ {tr}_{q}^{x . B} : B [a / x] \to B [b / x] with Γ ⊢ {tr}_{{refl}_{a}}^{x . B} (u) \equiv u : B [a / x]$ for every $Γ ⊢ u : B [a / x]$ . We omit the binder and write ${tr}_{q}^{B}$ when $B$ has exactly one displayed free variable to abstract.

Referenced from 7 locations

Proof of Construction 30.9 — Transport

Construction. Apply Id-elim with the motive $Γ, x : A, y : A, p : {Id}_{A} (x, y) ⊢ B \to B [y / x] type$ (the motive does not mention $p$ ) and the reflexivity clause $z . λ u . u$ , whose required type is $(B \to B [y / x]) [z / x, z / y, {refl}_{z} / p] \equiv B [z / x] \to B [z / x]$ . Set ${tr}_{q}^{x . B} : = J (x . y . p . B \to B [y / x]; z . λ u . u; q)$ . Formation of $B [y / x]$ while retaining the declaration $x : A$ first uses lemma 26.30 to rename the family binder from $x$ to the fresh $y$ . Two applications of weakening then insert the original declaration $x : A$ before $y$ and the path declaration $p$ after it. No capture-prone raw replacement or ill-ordered substitution is implicit. The computation rule is an instance of Id-comp followed by $β$ -reduction (definition 27.2). ◻

Example 30.10 — A blocked open transport ¶

Given $x : N ⊢ B type$ , work in the context $n : N, m : N, p : {Id}_{N} (n + m, m + n), u : B [n + m / x]$ . The term ${tr}_{p}^{B} (u)$ is well typed in $B [m + n / x]$ , but its defining computation does not fire: the identification is the variable $p$ , not a displayed reflexivity. This is why calculations with transport require proofs of the groupoid laws.

Referenced from 2 locations

Identity Types

Proposition 30.11 — Indiscernibility of identicals ¶

For every family $Γ, x : A ⊢ B type$ and elements $Γ ⊢ a : A$ , $Γ ⊢ b : A$ , the type ${Id}_{A} (a, b) \to B [a / x] \to B [b / x]$ is inhabited, namely by $λ q . {tr}_{q}^{x . B}$ . Under propositions-as-types this is Leibniz’s principle: identified elements are indiscernible by every property expressible in the theory.

Referenced from 2 locations

Identity Types

Proof of Proposition 30.11 — Indiscernibility of identicals

Proof. For $q : {Id}_{A} (a, b)$ , construction 30.9 gives ${tr}_{q}^{x . B} : B [a / x] \to B [b / x]$ . Therefore $λ q . {tr}_{q}^{x . B}$ inhabits the displayed dependent function type; at $q = {refl}_{a}$ , its application to $u$ is judgmentally $u$ by the transport computation rule. ◻

Example 30.12 — Boolean constructors are internally disjoint ¶

Assume the universe and large Boolean elimination of construction 29.12. Put $P : = λ b . {If}_{0} (1, 0, b) : 2 \to U_{0} .$ The two computation rules give $P tt \equiv 1$ and $P ff \equiv 0$ . Hence, for $q : {Id}_{2} (tt, ff)$ , transport gives ${tr}_{q}^{b . P b} (⋆) : P ff,$ which converts to a term of $0$ . Thus $λ q . {tr}_{q}^{b . P b} (⋆) : {Id}_{2} (tt, ff) \to 0 .$ Unlike the metatheoretic separation in theorem 29.14, this is an internal negation: an assumed identification itself transports the unit element into the empty type.

Referenced from 5 locations

Proposition 30.13 — Least reflexive relation ¶

Let $Γ, x : A, y : A ⊢ R type$ be a binary family equipped with a proof of reflexivity, $Γ ⊢ ρ : \prod_{z : A} R [z / x, z / y]$ . Then there is a term $Γ ⊢ e : \prod_{x : A} \prod_{y : A} {Id}_{A} (x, y) \to R$ and, in context $Γ, z : A$ , its reflexivity computation is $Γ, z : A ⊢ e z z {refl}_{z} \equiv ρ z : R [z / x, z / y] .$ Thus ${Id}_{A} (-, -)$ maps into every reflexive relation on $A$ : it is the least reflexive relation, which was Martin-Löf’s original specification of the identity type [ML98, ML84].

Referenced from 2 locations

Identity Types

Proof of Proposition 30.13 — Least reflexive relation

Proof. Apply Id-elim with the $p$ -independent motive $R$ (weakened to the context $Γ, x : A, y : A, p : {Id}_{A} (x, y)$ ) and clause $z . ρ z$ ; the computation rule is Id-comp. ◻

Construction 30.14 — Inverse ¶

For $Γ ⊢ q : {Id}_{A} (a, b)$ there is a term $Γ ⊢ q^{- 1} : {Id}_{A} (b, a)$ with $Γ ⊢ ({refl}_{a})^{- 1} \equiv {refl}_{a} : {Id}_{A} (a, a)$ : set $q^{- 1} : = J (x . y . p . {Id}_{A} (y, x); z . {refl}_{z}; q) .$

Referenced from 2 locations

Identity Types

Construction 30.15 — Concatenation ¶

For $Γ ⊢ p : {Id}_{A} (a, b)$ and $Γ ⊢ q : {Id}_{A} (b, c)$ there is a term $Γ ⊢ p \cdot q : {Id}_{A} (a, c)$ with $Γ ⊢ p \cdot {refl}_{b} \equiv p : {Id}_{A} (a, b)$ : transport $p$ in the family of identifications out of $a$ , $p \cdot q : = {tr}_{q}^{w . {Id}_{A} (a, w)} (p) .$ The computation rule is that of construction 30.9.

Referenced from 5 locations

Remark 30.16 — Asymmetry of concatenation ¶

Construction 30.15 proceeds by induction on the second argument, so the right unit law $p \cdot {refl}_{b} \equiv p$ is judgmental while the left unit law holds only up to an identification (theorem 30.20(i)). Inducting on the first argument instead yields an operation with ${refl}_{a} \cdot^{'} q \equiv q$ ; inducting on both (as in the HoTT Book [Uni13]) yields one computing only on $refl \cdot^{″} refl$ . All three agree up to identifications. Indeed, compare either alternative with $\cdot$ by identity induction on both inputs: after they have reduced to reflexivity, both concatenations compute to reflexivity, so reflexivity inhabits the comparison type. Exercise 30.4 asks for one such comparison with every motive made explicit. Such choices are harmless when one asks only for an identification, but differ when one tracks which unit equation is judgmental.

Referenced from 2 locations

Identity Types

Construction 30.17 — Action on identifications ¶

For $Γ ⊢ f : A \to B$ and $Γ ⊢ q : {Id}_{A} (a, b)$ there is a term $Γ ⊢ {ap}_{f} (q) : {Id}_{B} (f a, f b)$ with $Γ ⊢ {ap}_{f} ({refl}_{a}) \equiv {refl}_{f a} : {Id}_{B} (f a, f a)$ : set ${ap}_{f} (q) : = J (x . y . p . {Id}_{B} (f x, f y); z . {refl}_{f z}; q) .$ Thus every function preserves identifications: no operation of the theory can distinguish identified elements.

Referenced from 3 locations

Construction 30.18 — Dependent action ¶

For $Γ ⊢ f : \prod_{x : A} B$ and $Γ ⊢ q : {Id}_{A} (a, b)$ there is a term $\begin{matrix} Γ ⊢ {apd}_{f} (q) : {Id}_{B [b / x]} ({tr}_{q}^{x . B} (f a), f b) \\ with Γ ⊢ {apd}_{f} ({refl}_{a}) \equiv {refl}_{f a} : {Id}_{B [a / x]} (f a, f a), \end{matrix}$ namely ${apd}_{f} (q) : = J (x . y . p . {Id}_{B [y / x]} ({tr}_{p}^{x . B} (f x), f y); z . {refl}_{f z}; q)$ . Note that the clause $z . {refl}_{f z}$ has the required type ${Id}_{B [z / x]} ({tr}_{{refl}_{z}}^{x . B} (f z), f z)$ only via the computation rule ${tr}_{{refl}_{z}} (f z) \equiv f z$ and the conversion rule: the well-typedness of the eliminand depends on Id-comp for transport, as announced in convention 30.6(ii).

Referenced from 3 locations

Identity Types

Example 30.19 — Identifications beyond judgmental equality ¶

Use the addition of construction 28.23, which recurs on the second argument. Thus $m + 0 \equiv m$ and $m + suc (n) \equiv suc (m + n)$ . Then:

${refl}_{n + 0} : {Id}_{N} (n + 0, n)$ , by lemma 30.4: the equation holds judgmentally.
For a variable $n$ , no defining equation applies to $0 + n$ : the recursor inspects its second argument and that argument is a variable. Reflexivity has type ${refl}_{0 + n} : {Id}_{N} (0 + n, 0 + n)$ , not the required type ${Id}_{N} (0 + n, n)$ , because the endpoints $0 + n$ and $n$ are not judgmentally equal. Induction instead gives an inhabitant $α : = {ind}_{N} (m . {Id}_{N} (0 + m, m); {refl}_{0}, λ m . λ h . {ap}_{suc} (h); n),$ where the step clause is well-typed because $0 + suc (m) \equiv suc (0 + m)$ , so that ${ap}_{suc} (h) : {Id}_{N} (suc (0 + m), suc (m))$ converts to the required type.

Here the defining equations prove the right-unit law, whereas induction proves the left-unit identification. Identifications can therefore express equations not supplied by the defining computations; they are terms that must themselves be transported, inverted, and compared. Groupoid laws perform those comparisons.

Referenced from 2 locations

Identity Types

Exercise 30.3 ¶

★☆☆ Let $B$ be a type not depending on $x : A$ and $q : {Id}_{A} (a, b)$ . Construct a term of type ${Id}_{B} ({tr}_{q}^{x . B} (u), u)$ for each $u : B$ . Explain why this identification is in general not a judgmental equality, although ${tr}_{{refl}_{a}}^{x . B} (u) \equiv u$ .

Referenced from 3 locations

Exercise 30.4 ¶

★★★ Define $p \cdot^{'} q$ by identity induction on $p$ , so that ${refl}_{a} \cdot^{'} q \equiv q$ , and construct a term of type ${Id}_{{Id}_{A} (a, c)} (p \cdot q, p \cdot^{'} q)$ for all $p : {Id}_{A} (a, b)$ , $q : {Id}_{A} (b, c)$ . First induct on $p$ to compare $p \cdot^{'} {refl}_{b}$ with $p$ ; then induct on $q$ with $p$ generalized into the motive, using the inverse of that comparison in the reflexivity case.

Referenced from 4 locations

Exercise 30.5 ¶

★★☆ Construct identifications ${Id}_{{Id}_{A} (a, b)} ({ap}_{λ x . x} (q), q) and {Id}_{{Id}_{B} (b_{0}, b_{0})} ({ap}_{λ x . b_{0}} (q), {refl}_{b_{0}})$ for $q : {Id}_{A} (a, b)$ and $b_{0} : B$ . Which of the two, if either, holds judgmentally for a general path variable $q$ , and why?

Referenced from 3 locations

Exercise 30.6 ¶

★★☆ Fix a universe $U_{i}$ with $A : U_{i}$ , and define the Leibniz relation $L (a, b) : = \prod_{B : A \to U_{i}} B a \to B b$ . Construct maps ${Id}_{A} (a, b) \to L (a, b)$ and $L (a, b) \to {Id}_{A} (a, b)$ . (For the second, instantiate $B$ at the based family $λ w . {Id}_{A} (a, w)$ .) Thus identity of indiscernibles is derivable, given a universe.

Referenced from 3 locations

Exercise 30.7 ¶

★★☆ Let $\cdot ⊢ A type$ and assume, in addition to definition 30.1, equality reflection: from $Γ ⊢ q : {Id}_{A} (a, b)$ conclude $Γ ⊢ a \equiv b : A$ . Construct a closed term of type $\prod_{x : A} \prod_{p : {Id}_{A} (x, x)} {Id}_{{Id}_{A} (x, x)} (p, {refl}_{x})$ . Hint: in the generic context $x, y : A, p : {Id}_{A} (x, y)$ , reflection lets ${refl}_{x}$ convert to the type ${Id}_{A} (x, y)$ ; use this converted term in the motive of $J$ .

Referenced from 3 locations

The groupoid laws

The operations $refl$ , $(-)^{- 1}$ , $\cdot$ obey the groupoid laws—but only up to further identifications. Each law is an identity type between identifications, and what we construct is an inhabitant of it.

Theorem 30.20 — Groupoid laws ¶

Let $A$ be a type and $a, b, c, d : A$ , with $p : {Id}_{A} (a, b)$ , $q : {Id}_{A} (b, c)$ , $r : {Id}_{A} (c, d)$ . The following types are inhabited:

unit laws: ${Id}_{{Id}_{A} (a, b)} ({refl}_{a} \cdot p, p)$ , and judgmentally $p \cdot {refl}_{b} \equiv p$ ;
inverse laws: ${Id}_{{Id}_{A} (a, a)} (p \cdot p^{- 1}, {refl}_{a})$ and ${Id}_{{Id}_{A} (b, b)} (p^{- 1} \cdot p, {refl}_{b})$ ;
involution: ${Id}_{{Id}_{A} (a, b)} ((p^{- 1})^{- 1}, p)$ ;
associativity: ${Id}_{{Id}_{A} (a, d)} ((p \cdot q) \cdot r, p \cdot (q \cdot r))$ .

Referenced from 45 locations

Proof of Theorem 30.20 — Groupoid laws

Proof. (i) The judgmental half is the computation rule for concatenation. For the other half, the endpoints $a, b$ of $p$ are generic, so identity induction applies (convention 30.6). In context $x, y : A, ρ : {Id}_{A} (x, y)$ , take the motive ${Id}_{{Id}_{A} (x, y)} ({refl}_{x} \cdot ρ, ρ) .$ For the clause, note that ${refl}_{z} \cdot {refl}_{z} \equiv {refl}_{z}$ by the computation rule of $\cdot$ , so that ${refl}_{{refl}_{z}}$ inhabits the instance ${Id}_{{Id}_{A} (z, z)} ({refl}_{z} \cdot {refl}_{z}, {refl}_{z})$ after conversion. Then $J (z . {refl}_{{refl}_{z}}; p)$ inhabits ${Id}_{{Id}_{A} (a, b)} ({refl}_{a} \cdot p, p)$ .

(ii) Induct on $p$ , once for each inverse law. The two motives are $x, y : A, ρ : {Id}_{A} (x, y) ⊢ {Id}_{{Id}_{A} (x, x)} (ρ \cdot ρ^{- 1}, {refl}_{x}) type,$ $x, y : A, ρ : {Id}_{A} (x, y) ⊢ {Id}_{{Id}_{A} (y, y)} (ρ^{- 1} \cdot ρ, {refl}_{y}) type .$ At $x = y = z$ and $ρ = {refl}_{z}$ , inverse computes to ${refl}_{z}$ . In the first motive the resulting concatenation computes because its second argument is ${refl}_{z}$ ; in the second the defining equation of $\cdot$ applies because the right argument is again ${refl}_{z}$ . Both instances are therefore judgmentally ${Id}_{{Id}_{A} (z, z)} ({refl}_{z}, {refl}_{z})$ , with clause $z . {refl}_{{refl}_{z}}$ .

(iii) Use the motive $x, y : A, ρ : {Id}_{A} (x, y) ⊢ {Id}_{{Id}_{A} (x, y)} ((ρ^{- 1})^{- 1}, ρ) type .$ At reflexivity, the two applications of inverse both compute, so the clause is again $z . {refl}_{{refl}_{z}}$ .

(iv) Concatenation computes on its second argument, so eliminate $r$ . The fixed path $q : {Id}_{A} (b, c)$ contains the left endpoint $c$ of $r$ in its type, and therefore cannot remain fixed while that endpoint is made generic. Generalize both $p$ and $q$ into the motive. Work in context $x, y : A, ρ : {Id}_{A} (x, y)$ and quantify over $a^{'}, b^{'} : A$ , $p^{'} : {Id}_{A} (a^{'}, b^{'})$ , and $q^{'} : {Id}_{A} (b^{'}, x)$ . The fiber of the resulting iterated product is ${Id}_{{Id}_{A} (a^{'}, y)} ((p^{'} \cdot q^{'}) \cdot ρ, p^{'} \cdot (q^{'} \cdot ρ)) .$ This is well formed because $x$ is a variable of the motive’s context. For the clause at $z$ , both sides compute: $(p^{'} \cdot q^{'}) \cdot {refl}_{z} \equiv p^{'} \cdot q^{'}$ and $p^{'} \cdot (q^{'} \cdot {refl}_{z}) \equiv p^{'} \cdot q^{'}$ , so $λ a^{'} . λ b^{'} . λ p^{'} . λ q^{'} . {refl}_{p^{'} \cdot q^{'}}$ has the required type after conversion. Applying $J$ to $r$ and instantiating the resulting $Π$ -term at $a, b, p, q$ yields the associator $\begin{aligned} α_{p, q, r} : = & J (z . λ a^{'} . λ b^{'} . λ p^{'} . λ q^{'} . {refl}_{p^{'} \cdot q^{'}}; r) a b p q, \\ α_{p, q, r} : & {Id}_{{Id}_{A} (a, d)} ((p \cdot q) \cdot r, p \cdot (q \cdot r)) . \end{aligned}$ ◻

Proposition 30.21 — Functoriality of ¶

For $f : A \to B$ , $g : B \to C$ , $p : {Id}_{A} (a, b)$ , $q : {Id}_{A} (b, c)$ , the following types are inhabited:

${Id}_{{Id}_{B} (f a, f c)} ({ap}_{f} (p \cdot q), {ap}_{f} (p) \cdot {ap}_{f} (q))$ ;
${Id}_{{Id}_{B} (f b, f a)} ({ap}_{f} (p^{- 1}), ({ap}_{f} (p))^{- 1})$ ;
${Id}_{{Id}_{C} (g (f a), g (f b))} ({ap}_{λ x . g (f x)} (p), {ap}_{g} ({ap}_{f} (p)))$ .

Referenced from 5 locations

Proof of Proposition 30.21 — Functoriality of

Proof. (i) Induct on $q$ and generalize $a$ and $p$ into the motive. For generic $x, y : A$ and $ρ : {Id}_{A} (x, y)$ take $\prod_{a^{'} : A} \prod_{p^{'} : {Id}_{A} (a^{'}, x)} {Id}_{{Id}_{B} (f (a^{'}), f (y))} ({ap}_{f} (p^{'} \cdot ρ), {ap}_{f} (p^{'}) \cdot {ap}_{f} (ρ)) .$ At $ρ = {refl}_{x}$ , the concatenation $p^{'} \cdot {refl}_{x}$ , the action ${ap}_{f} ({refl}_{x})$ , and the right-hand concatenation all compute. Both sides are ${ap}_{f} (p^{'})$ , so the clause is $λ a^{'} . λ p^{'} . {refl}_{{ap}_{f} (p^{'})}$ . Instantiate the result at $a, p$ .

(ii) For generic $x, y : A$ and $ρ : {Id}_{A} (x, y)$ , take the motive ${Id}_{{Id}_{B} (f (y), f (x))} ({ap}_{f} (ρ^{- 1}), ({ap}_{f} (ρ))^{- 1}) .$ At $x = y = z$ and $ρ = {refl}_{z}$ , inverse and $ap$ both compute. The reflexivity clause is $z . {refl}_{{refl}_{f (z)}}$ . Instantiating at $a, b, p$ gives the required path.

(iii) For generic $x, y : A$ and $ρ : {Id}_{A} (x, y)$ , take the motive ${Id}_{{Id}_{C} (g (f (x)), g (f (y)))} ({ap}_{λ w . g (f (w))} (ρ), {ap}_{g} ({ap}_{f} (ρ))) .$ At $x = y = z$ and $ρ = {refl}_{z}$ , both endpoints compute to ${refl}_{g (f (z))}$ . The clause is $z . {refl}_{{refl}_{g (f (z))}}$ ; instantiate at $a, b, p$ . ◻

Proposition 30.22 — Transport is functorial ¶

Let $Γ, x : A ⊢ B type$ , and let $p : {Id}_{A} (a, b)$ , $q : {Id}_{A} (b, c)$ , $u : B [a / x]$ . The following types are inhabited:

${Id}_{B [c / x]} ({tr}_{p \cdot q}^{B} (u), {tr}_{q}^{B} ({tr}_{p}^{B} (u)))$ ;
${Id}_{B [a / x]} ({tr}_{p^{- 1}}^{B} ({tr}_{p}^{B} (u)), u)$ .
for $v : B [b / x]$ , ${Id}_{B [b / x]} ({tr}_{p}^{B} ({tr}_{p^{- 1}}^{B} (v)), v)$ .

Referenced from 2 locations

Identity Types

Proof of Proposition 30.22 — Transport is functorial

Proof. (i) Induct on $q$ while generalizing $a$ , $p$ , and $u$ into the motive. For generic $x, y : A$ and $ρ : {Id}_{A} (x, y)$ take $\prod_{a^{'} : A} \prod_{p^{'} : {Id}_{A} (a^{'}, x)} \prod_{u^{'} : B [a^{'} / x]} {Id}_{B [y / x]} ({tr}_{p^{'} \cdot ρ}^{B} (u^{'}), {tr}_{ρ}^{B} ({tr}_{p^{'}}^{B} (u^{'}))) .$ At $ρ = {refl}_{x}$ , the concatenation and the outer transport compute, so both endpoints reduce to ${tr}_{p^{'}}^{B} (u^{'})$ . The clause is $λ a^{'} . λ p^{'} . λ u^{'} . {refl}_{{tr}_{p^{'}}^{B} (u^{'})}$ ; instantiate at $a, p, u$ .

(ii) Generalize $u$ into the motive $x, y : A, ρ : {Id}_{A} (x, y) ⊢ \prod_{u^{'} : B} {Id}_{B} ({tr}_{ρ^{- 1}}^{B} ({tr}_{ρ}^{B} (u^{'})), u^{'}) type .$ At $ρ = {refl}_{x}$ both transports and the inverse compute, so the clause is $λ u^{'} . {refl}_{u^{'}}$ . Instantiate the result at $u$ .

(iii) This time generalize $v$ into the motive $x, y : A, ρ : {Id}_{A} (x, y) ⊢ \prod_{v^{'} : B [y / x]} {Id}_{B [y / x]} ({tr}_{ρ}^{B} ({tr}_{ρ^{- 1}}^{B} (v^{'})), v^{'}) type .$ Its reflexivity clause is again $λ v^{'} . {refl}_{v^{'}}$ after the inverse and both transports compute. Instantiate at $v$ . ◻

Remark 30.23 — Higher structure ¶

The laws of theorem 30.20 are themselves terms, so their identity types may be formed in turn. Repeated identity induction constructs many coherence identifications; for example, it compares the two composites of associators that rebracket four consecutive identifications. Thus the rules produce a hierarchy: identifications, identifications between those, and so on without end. The four groupoid laws above are only its first level. A complete coherence theorem for the whole hierarchy is a separate metatheoretic result.

Referenced from 2 locations

Identity Types

Exercise 30.8 ¶

★★☆ For $p : {Id}_{A} (a, b)$ and $q : {Id}_{A} (b, c)$ , construct an identification ${Id}_{{Id}_{A} (c, a)} ((p \cdot q)^{- 1}, q^{- 1} \cdot p^{- 1}) .$ Induct first on $q$ with $p$ generalized; in the reflexivity instance use the inverse of the left-unit identification in theorem 30.20(i).

Referenced from 3 locations

Exercise 30.9 ¶

★★☆ Given $f, f^{'} : A \to B$ and a pointwise identification $h : \prod_{x : A} {Id}_{B} (f (x), f^{'} (x))$ , show that for $p : {Id}_{A} (a, b)$ the two boundary composites $(h (a)^{- 1} \cdot {ap}_{f} (p)) \cdot h (b)$ and ${ap}_{f^{'}} (p)$ are identified. Induct on $p$ and use the groupoid laws in the reflexivity case. The other bracketing follows from the associativity identification of theorem 30.20(iv).

Referenced from 3 locations

Exercise 30.10 ¶

★★☆ Let $B$ and $C$ be families over $A$ and $h : \prod_{x : A} B (x) \to C (x)$ . For $p : {Id}_{A} (a, b)$ and $u : B (a)$ , construct an identification ${Id}_{C (b)} ({tr}_{p}^{C} (h (a) (u)), h (b) ({tr}_{p}^{B} (u))) .$ State the motive and verify its reflexivity clause.

Referenced from 3 locations

Singletons and based path induction

The eliminator $J$ requires both endpoints to be generic. This section derives the sharper principle in which one endpoint stays fixed — based path induction — from a single new construction: contractibility of singletons.

A direct use of Id-elim cannot simply insert the based motive. If $C$ is formed in $Γ, y : A, p : {Id}_{A} (a, y)$ , the tempting assignment $D (x, y, p) \overset{?}{: =} C (y, p) for x, y : A, p : {Id}_{A} (x, y)$ is ill formed: inside $C$ , the variable $p$ must have type ${Id}_{A} (a, y)$ , whereas the generic $p$ supplied by Id-elim has type ${Id}_{A} (x, y)$ . The construction below performs exactly the missing change of base point.

Definition 30.24 — Singleton type ¶

For $Γ ⊢ a : A$ , the singleton of $a$ is ${Sing}_{A} (a) : = \sum_{y : A} {Id}_{A} (a, y),$ the type of elements of $A$ together with an identification with $a$ . Its distinguished element is the center $(a, {refl}_{a}) : {Sing}_{A} (a)$ .

Referenced from 2 locations

Identity Types

Construction 30.25 — Contractibility of singletons ¶

For $Γ ⊢ a : A$ and $Γ ⊢ u : {Sing}_{A} (a)$ there is a term $Γ ⊢ {uniq}_{a} (u) : {Id}_{{Sing}_{A} (a)} ((a, {refl}_{a}), u) .$ At the center it computes judgmentally: $Γ ⊢ {uniq}_{a} ((a, {refl}_{a})) \equiv {refl}_{(a, {refl}_{a})} : {Id}_{{Sing}_{A} (a)} ((a, {refl}_{a}), (a, {refl}_{a})) .$

Referenced from 3 locations

Identity Types

Proof of Construction 30.25 — Contractibility of singletons

Construction. Apply Id-elim with the motive $x : A, y : A, p : {Id}_{A} (x, y) ⊢ {Id}_{{Sing}_{A} (x)} ((x, {refl}_{x}), (y, p)) type$ and clause $z . {refl}_{(z, {refl}_{z})}$ , obtaining $e (x, y, p) : {Id}_{{Sing}_{A} (x)} ((x, {refl}_{x}), (y, p))$ . Set ${uniq}_{a} (u) : = e (a, {pr}_{1} (u), {pr}_{2} (u))$ ; by the $η$ -rule for $Σ$ -types (definition 27.9) we have $u \equiv ({pr}_{1} (u), {pr}_{2} (u))$ , so the type of ${uniq}_{a} (u)$ converts to the one stated. The computation rule follows from Id-comp and the $β$ -rules for $Σ$ (which give ${pr}_{1} (a, {refl}_{a}) \equiv a$ , ${pr}_{2} (a, {refl}_{a}) \equiv {refl}_{a}$ ). Note that the motive generalizes the goal: it proves the statement for every center $x$ at once, which is what makes the induction legitimate. ◻

Theorem 30.26 — Based path induction ¶

The following rules are derivable from definition 30.1 together with $Σ$ -types:

Γ ⊢ a : A

Γ, y : A, p : {Id}_{A} (a, y) ⊢ C type

Γ ⊢ c : C [a / y, {refl}_{a} / p]

Γ ⊢ q : {Id}_{A} (a, b)

Γ ⊢ J^{'} (y . p . C; c; q) : C [b / y, q / p]

Id-elim'

Γ ⊢ a : A

Γ, y : A, p : {Id}_{A} (a, y) ⊢ C type

Γ ⊢ c : C [a / y, {refl}_{a} / p]

Γ ⊢ J^{'} (y . p . C; c; {refl}_{a}) \equiv c : C [a / y, {refl}_{a} / p]

Id-comp'

Here the endpoint $a$ is arbitrary — fixed, not generic — and the computation rule holds judgmentally.

Referenced from 6 locations

Proof of Theorem 30.26 — Based path induction

Proof. Uncurry the family $C$ over the singleton: let $Γ, u : {Sing}_{A} (a) ⊢ \hat{C} type, \hat{C} : = C [{pr}_{1} (u) / y, {pr}_{2} (u) / p] .$ Given $q : {Id}_{A} (a, b)$ , the contraction path at $(b, q)$ is ${uniq}_{a} ((b, q)) : {Id}_{{Sing}_{A} (a)} ((a, {refl}_{a}), (b, q)),$ and we transport along it: $J^{'} (y . p . C; c; q) : = {tr}_{{uniq}_{a} ((b, q))}^{u . \hat{C}} (c) .$ This is well-typed: by the $β$ -rules for $Σ$ , $\hat{C} [(a, {refl}_{a}) / u] \equiv C [a / y, {refl}_{a} / p]$ , the type of $c$ , and $\hat{C} [(b, q) / u] \equiv C [b / y, q / p]$ , the stated conclusion. For the computation rule, take $b : = a$ , $q : = {refl}_{a}$ : then $\begin{aligned} {tr}_{{uniq}_{a} ((a, {refl}_{a}))}^{\hat{C}} (c) & \overset{c o n s t r u c t i o n 30.25}{=} {tr}_{{refl}_{(a, {refl}_{a})}}^{\hat{C}} (c) \\ \overset{c o n s t r u c t i o n 30.9}{=} c . \end{aligned}$ Both steps are judgmental, so Id-comp $^{'}$ holds as stated. ◻

Proposition 30.27 — Equivalence of the presentations ¶

In the presence of the $Σ$ -rules of definition 27.9, including their judgmental $η$ -rule, the following three presentations are interderivable with their displayed judgmental computation rules:

the two-endpoint eliminator $J$ of definition 30.1;
the based eliminator $J^{'}$ of theorem 30.26;
transport of construction 30.9 together with singleton contraction $uniq$ from construction 30.25.

Referenced from 4 locations

Proof of Proposition 30.27 — Equivalence of the presentations

Proof. The implication (i) $\Rightarrow$ (iii) is the construction of transport and $uniq$ above, and (iii) $\Rightarrow$ (ii) is the proof of theorem 30.26. It remains only to recover full $J$ from (ii), or directly from (iii).

Suppose $C$ is a motive over $x, y, p$ and $c$ is its reflexivity clause. For each $x : A$ and $u : {Sing}_{A} (x)$ define ${\hat{C}}_{x} (u) : = C [x / x, {pr}_{1} (u) / y, {pr}_{2} (u) / p] .$ Given $q : {Id}_{A} (a, b)$ , set $J_{tr} (x . y . p . C; z . c; q) : = {tr}_{{uniq}_{a} ((b, q))}^{u . {\hat{C}}_{a} (u)} (c [a / z]) .$ The source fiber reduces to $C [a / x, a / y, {refl}_{a} / p]$ and the target fiber to $C [a / x, b / y, q / p]$ , so the term has exactly the conclusion of Id-elim. For $q = {refl}_{a}$ , singleton contraction computes to ${refl}_{(a, {refl}_{a})}$ , and transport along that reflexivity computes to $c [a / z]$ . Hence Id-comp is judgmental. This proves (iii) $\Rightarrow$ (i). From $J^{'}$ at the fixed endpoint $a$ one obtains the same conclusion directly: $J_{based} (x . y . p . C; z . c; q) : = J^{'} (y . p . C [a / x]; c [a / z]; q) .$ Its classifier is $C [a / x, b / y, q / p]$ , and its reflexivity equation is exactly Id-comp $^{'}$ . This proves (ii) $\Rightarrow$ (i). ◻

Exercise 30.11 ¶

★☆☆ Using only $J^{'}$ and its computation rule, reconstruct inverse and concatenation. Which unit law for the resulting concatenation is judgmental? Compare with construction 30.15.

Referenced from 3 locations

Exercise 30.12 ¶

★★☆ Take only $tr$ and $uniq$ with their computation rules as primitive. Reconstruct the dependent action ${apd}_{f} (q)$ of construction 30.18. Use the formula for $J_{tr}$ in proposition 30.27, and verify the reflexivity computation without appealing to primitive $J$ .

Referenced from 3 locations

Limits of path induction

The eliminator $J$ proves inverse, concatenation, congruence, and groupoid laws by acting on the identity family with both endpoints generic. None of the displayed constructions identifies every pair of identifications with fixed endpoints, or supplies function extensionality, the principle that pointwise identifications produce an identification between functions. We state these types explicitly and then separate two questions: whether adding them is consistent, and whether they are derivable from $J$ alone.

Definition 30.28 — UIP and K ¶

For a type $A$ , define $\begin{aligned} {UIP}_{A} & : = \prod_{x : A} \prod_{y : A} \prod_{p : {Id}_{A} (x, y)} \prod_{q : {Id}_{A} (x, y)} {Id}_{{Id}_{A} (x, y)} (p, q), \\ K_{A} & : = \prod_{x : A} \prod_{p : {Id}_{A} (x, x)} {Id}_{{Id}_{A} (x, x)} (p, {refl}_{x}) . \end{aligned}$ ${UIP}_{A}$ (uniqueness of identity proofs) asserts that any two identifications of the same endpoints are identified; $K_{A}$ (Streicher’s axiom K) is the special case of loops at a point, compared with $refl$ [Str93].

Referenced from 4 locations

Proposition 30.29 ¶

For every type $A$ , the types ${UIP}_{A} \to K_{A}$ and $K_{A} \to {UIP}_{A}$ are inhabited.

Referenced from 2 locations

Identity Types

Proof of Proposition 30.29

Proof. The first map sends $u : {UIP}_{A}$ to $λ x . λ p . u x x p {refl}_{x}$ ; no symmetry is needed. For the second, fix $k : K_{A}$ and $x : A$ ; we construct all of ${UIP}_{A}$ ’s remaining arguments by based path induction on $q$ (theorem 30.26), with $p$ generalized into the motive: $y : A, q : {Id}_{A} (x, y) ⊢ \prod_{p : {Id}_{A} (x, y)} {Id}_{{Id}_{A} (x, y)} (p, q) type .$ The reflexivity clause required when $y : = x$ and $q : = {refl}_{x}$ has type $\prod_{p : {Id}_{A} (x, x)} {Id}_{{Id}_{A} (x, x)} (p, {refl}_{x}),$ and is exactly $k x$ . The remaining loop $p$ has both endpoints fixed at $x$ . Thus neither Id-elim nor Id-elim $^{'}$ applies directly; this residue is precisely $K_{A}$ . ◻

Construction 30.34 — Pointwise action ¶

For $f, g : \prod_{x : A} B$ there is a term $\begin{matrix} {happly}_{f, g} : {Id}_{\prod_{x : A} B} (f, g) \to \prod_{x : A} {Id}_{B} (f x, g x) \\ with {happly}_{f, f} ({refl}_{f}) \equiv λ x . {refl}_{f x}, \end{matrix}$ by identity induction: take the motive $\prod_{x : A} {Id}_{B} (u x, v x)$ over $u, v, p$ and the clause $w . λ x . {refl}_{w x}$ .

Referenced from 4 locations

Identity Types

Definition 30.35 — Function extensionality ¶

For an arbitrary family $Γ, x : A ⊢ B type$ and functions $f, g : \prod_{x : A} B$ , first put $Pt (f, g) : = \prod_{x : A} {Id}_{B} (f x, g x) .$ Then define ${Funext}_{A, B} : = \prod_{f : \prod_{x : A} B} \prod_{g : \prod_{x : A} B} Pt (f, g) \to {Id}_{\prod_{x : A} B} (f, g) .$ This is the assertion converse to construction 30.34: pointwise identified functions are identified.

Referenced from 3 locations

Proposition 77.32 — The set interpretation validates UIP and function extensionality ¶

In ZFC, the set interpretation of definition 73.39 extends to Id-form, Id-intro, Id-elim, and Id-comp. Under the Grothendieck-universe hypothesis of lemma 74.14, it also validates Id-form- $U$ and Lift-Id. In either corresponding signature, the extensions by $UIP$ and $Funext$ have semantic sections.

Referenced from 6 locations

Proof of Proposition 77.32 — The set interpretation validates UIP and function extensionality

Proof. Interpret ${Id}_{A} (a, b)$ at $ρ$ as ${*}$ when $[[a {]]}_{ρ} = [[b {]]}_{ρ}$ and as $\emptyset$ otherwise. Reflexivity denotes $*$ . Whenever $[[q {]]}_{ρ}$ is defined, the identity fiber is inhabited, hence $[[a {]]}_{ρ} = [[b {]]}_{ρ}$ . Define $[[J_{A; a; b} (x . y . p . C; z . c; q) {]]}_{ρ}^{Γ} : = [[c {]]}_{(ρ, [[a {]]}_{ρ})}^{Γ, z : A} .$ After replacing $[[b {]]}_{ρ}$ by $[[a {]]}_{ρ}$ and the unique identity element by $*$ , the right side belongs to the interpreted motive at $([[a {]]}_{ρ}, [[b {]]}_{ρ}, [[q {]]}_{ρ})$ . If $q$ is not interpreted, the partial value of the eliminator is undefined. At $q = {refl}_{a}$ the defining equation is literal.

The two new raw clauses commute with semantic substitution and weakening: reindexing preserves equality of endpoint values, and the displayed $J$ equation reduces to the substitution equation for $c$ . Thus the structural lemma lemma 28.13 gains these two operator cases. The simultaneous derivation induction of lemma 28.14 then gains formation, introduction, elimination, computation, and congruence cases for identity types. Grothendieck-universe closure makes each equality fiber small, and strict lifting leaves that fiber unchanged, giving the two universe rules.

Every identity fiber has at most one element, which supplies the semantic $UIP$ section. Pointwise equal set-theoretic dependent functions are the same set of ordered pairs, so the identity fiber of the two functions is inhabited; this supplies $Funext$ . ◻

Remark 77.33 — Set-model boundary ¶

Proposition 77.32 proves relative consistency of adding UIP and function extensionality. It validates both principles, so it cannot show either one underivable. Showing UIP underivable requires a model with nontrivial identity fibers. The groupoid model of [HS98] is such a countermodel. No independence theorem is used here.

Referenced from 2 locations

Identity Types

Example 30.37 — Blocked elimination under an assumed principle ¶

Work in the context $χ : {Funext}_{2, 2}$ . Let $g : = λ x . {ind}_{2} (y . 2; tt, ff; x) : 2 \to 2,$ so that $g tt \equiv tt$ and $g ff \equiv ff$ , while the displayed body has no computation step when its scrutinee is the variable $x$ . Boolean induction gives $h : = λ x . {ind}_{2} (y . {Id}_{2} (y, g y); {refl}_{tt}, {refl}_{ff}; x) : \prod_{x : 2} {Id}_{2} (x, g x) .$

Hence $e : = χ (λ x . x) g h : {Id}_{2 \to 2} (λ x . x, g)$ . Now the term $b : = J (u . v . p . 2; z . tt; e) : 2$ is blocked: its outer computation rule Id-comp requires the eliminand to be $refl$ , and $e$ — an application of the variable $χ$ — is not displayed in that form. Thus an inhabitant of $Funext$ supplies an identification but no new computation equation for eliminating it.

Referenced from 3 locations

Identity Types

Remark 77.35 — Final motive audit ¶

Every use of path induction in this chapter can be replayed with the following three-line check: $\begin{array}{ll} generic context: & x, y : A, p : {Id}_{A} (x, y), \\ motive: & C (x, y, p) : U_{j}, \\ clause: & d (z) : C (z, z, {refl}_{z}) . \end{array}$ For inverse functoriality, $C (x, y, p)$ is the equality displayed in proposition 30.21(ii), and substituting $y := x$ , $p := {refl}_{x}$ produces its clause. Based induction first generalizes the fixed endpoint, applies this same audit, and then specializes it back. By contrast, the K-shaped family $p : {Id}_{A} (a, a) ⊢ {Id}_{{Id}_{A} (a, a)} (p, {refl}_{a}) : U_{i}$ has already fixed both endpoints. It cannot occupy the generic motive line, which is the exact point where the K derivation stops.

Referenced from 2 locations

Identity Types

Exercise 30.13 ¶

★★★ Show that $UIP$ is hereditary: from a term of ${UIP}_{A}$ , construct a term of ${UIP}_{{Id}_{A} (a, b)}$ for any $a, b : A$ . Hint: put $I : = {Id}_{A} (a, b)$ , fix $p : I$ , and let $c (q) : {Id}_{I} (p, q)$ be supplied by ${UIP}_{A}$ . By based induction on $r : {Id}_{I} (p, q)$ , compare $r$ with the canonical composite $c (p)^{- 1} \cdot c (q)$ ; the reflexivity case is an inverse law. Compare any two $r, s$ through that same composite.

Referenced from 3 locations

Exercise 30.14 ¶

★★☆ Verify in detail that the term $b$ of example 30.37 is well-typed in the context $χ : {Funext}_{2, 2}$ , and check that its outer $J$ computation rule does not apply. List the subterms that do compute and the variable-headed eliminators that remain blocked.

Referenced from 3 locations

Exercise 30.15 ¶

★☆☆ Let $s : {Funext}_{A, B}$ and fix $f, g : \prod_{x : A} B$ . Unfold the two displayed $Π$ -binders and derive $s f g : Pt (f, g) ⟶ {Id}_{\prod_{x : A} B} (f, g) .$ Together with ${happly}_{f, g}$ of construction 30.34, write down the two maps between $Pt (f, g)$ and ${Id}_{\prod_{x : A} B} (f, g)$ . No inverse law is asserted.

Referenced from 3 locations

Suggested first pass.

Begin with exercise 77.16, then complete exercise 77.17.

Exercise 77.16 ¶

★★☆ Starting from $J$ , derive based path induction and use it to prove the left unit, inverse, and associativity laws for path composition. In each case display the motive before applying $J$ and explain why direct induction on an endpoint would be ill typed.

Referenced from 4 locations

Exercise 77.17 ¶

★★★ Practical project.identity-eliminator-checker Implement in Agda or Kappa a checker for the displayed $J$ rule. Maintain the invariant that the motive is checked in the full endpoint-and-path context before the reflexivity branch is substituted. It must accept the based-induction derivation above and reject the same branch with the second endpoint left free; report the missing substitution in the rejection. Before implementing the checker, write the accepted and rejected derivation attempts on paper and circle the motive premise. The rejected tree must fail exactly because the second endpoint remains free after the reflexivity substitution.

Referenced from 5 locations

Sources. Identity formation, reflexivity, and elimination originate in Martin-Löf’s intensional type theory [ML98, ML75, ML84]. Axiom K and its intensionality criterion are due to Streicher [Str93]; the groupoid countermodel is due to Hofmann and Streicher [HS98]. The derived path operations, based induction, singleton contraction, and groupoid laws are also developed in [Uni13].