ch:extensional: ch:extensional

Both operations ignore their proof arguments: $$\mathsf{sym}:=\lambda p.\mathsf{refl},\mathsf{trans}:=\lambda p.\lambda q.\mathsf{refl}.$$ In the first context, Eq-Reflect applied to $p$ gives $a\equiv b:A$, so $\mathsf{refl}:{\mathsf{Eq}}_A(a,a)$ converts to an element of ${\mathsf{Eq}}_A(b,a)$. In the second, reflection applied to $p,q$ and transitivity give $a\equiv c:A$, so $\mathsf{refl}$ converts to the required type. Every application $\beta$-reduces judgmentally to $\mathsf{refl}$; the rule Eq-Uniq gives the same conclusion for any extensionally equal implementation.

Define $$\mathsf{happly}:=\lambda p.\lambda x.\mathsf{refl}.$$ Reflection sends $p:{\mathsf{Eq}}_{\prod _{x:A}B}(f,g)$ to $f\equiv g$; application congruence then gives $f(x)\equiv g(x)$, so the displayed $\mathsf{refl}$ converts to the required pointwise equality.

Now $\mathsf{funext}(h):=\mathsf{refl}$. Hence $\mathsf{happly}(\mathsf{funext}(h))\equiv \lambda x.\mathsf{refl}$, while Eq-Uniq gives $h(x)\equiv \mathsf{refl}$ for every $x$. Congruence and $\mathrm{\Pi }$-$\eta$ yield $h\equiv \lambda x.\mathsf{refl}$. Conversely, $\mathsf{funext}(\mathsf{happly}(p))\equiv \mathsf{refl}\equiv p$, the last equality again being Eq-Uniq. Abstracting these equations shows that both composites are judgmentally the corresponding identity functions.

For the $K$ step, the typed encoding supplies an extensional equality term $e_K⌜x⌝⌜y⌝:{\mathsf{Eq}}_X(⌜\mathsf{K}xy⌝,⌜x⌝)$ in ${\mathrm{\Gamma }}_{\mathsf{SK}}$. The two applications of $e_K$ check the endpoints at $X$; Eq-Reflect then concludes $⌜\mathsf{K}xy⌝\equiv ⌜x⌝$. Thus the derivation has two separable stages: construct and check the extensional equality evidence, then reflect it. Erasing that evidence leaves no procedure for finding a witness among arbitrary conversion goals; equality reflection checks supplied evidence but does not decide its existence.

Let $$\mathrm{\Theta }:=(A\mathsf{type};a:A;b:A)$$ be the parameter telescope of the raw former $\mathsf{Eq}(A,a,b)$. Two substitutions from $\mathrm{\Gamma }$ into $\mathrm{\Theta }$ are precisely triples $$\sigma =(A,a,b),{\sigma }^{\prime }=(A^{\prime },a^{\prime },b^{\prime }),$$ and an equality $\sigma \equiv {\sigma }^{\prime }:\mathrm{\Theta }$ consists, from left to right, of $$\mathrm{\Gamma }⊢A\equiv A^{\prime }\mathsf{type},\mathrm{\Gamma }⊢a\equiv a^{\prime }:A,\mathrm{\Gamma }⊢b\equiv b^{\prime }:A.$$ The classified congruence scheme for the type-valued operator $\mathrm{\Theta }⊢{\mathsf{Eq}}_A(a,b)\mathsf{type}$ therefore has the instance $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢A\equiv A^{\prime }\mathsf{type}\\ \mathrm{\Gamma }⊢a\equiv a^{\prime }:A\\ \mathrm{\Gamma }⊢b\equiv b^{\prime }:A\end{array}}{\mathrm{\Gamma }⊢{\mathsf{Eq}}_A(a,b)\equiv {\mathsf{Eq}}_{A^{\prime }}(a^{\prime },b^{\prime })\mathsf{type}}\mathrm{Eq}-\mathrm{F}-\mathrm{eq}.$$ The fact that the third component is compared in the fiber over the unprimed $A$ is exactly the left-to-right convention for equality of classified substitutions; context conversion places the primed component in that same fiber.

Now suppose $\mathrm{\Gamma }⊢a\equiv b:A$. Rule Eq-I gives $$\mathrm{\Gamma }⊢\mathsf{refl}:{\mathsf{Eq}}_A(a,a).$$ Apply the displayed congruence rule to $A\equiv A$, $a\equiv a$, and $a\equiv b$. It yields $$\mathrm{\Gamma }⊢{\mathsf{Eq}}_A(a,a)\equiv {\mathsf{Eq}}_A(a,b)\mathsf{type},$$ so Conv concludes $\mathrm{\Gamma }⊢\mathsf{refl}:{\mathsf{Eq}}_A(a,b)$.

The additional eliminator has the same shape as primitive identity elimination:

and its computation rule is $$\mathsf{J}(x.y.q.C;z.c;{\mathsf{refl}}_a)\equiv c[a/z]:C[a/x,a/y,{\mathsf{refl}}_a/q].$$ No uniqueness rule is assumed.

In the generic eliminator context, reflection applied to the variable $q:{\mathsf{Eq}}_A(x,y)$ gives $x\equiv y:A$. Hence ${\mathsf{refl}}_x:{\mathsf{Eq}}_A(x,x)$ converts to an element of ${\mathsf{Eq}}_A(x,y)$, and the family $$C(x,y,q):={\mathsf{Eq}}_{{\mathsf{Eq}}_A(x,y)}(q,{\mathsf{refl}}_x)$$ is well formed. Its diagonal fiber is $$C(z,z,{\mathsf{refl}}_z)\equiv {\mathsf{Eq}}_{{\mathsf{Eq}}_A(z,z)}({\mathsf{refl}}_z,{\mathsf{refl}}_z),$$ which has the branch ${\mathsf{refl}}_{{\mathsf{refl}}_z}$. Thus Eq-J constructs $$r(p):=\mathsf{J}(x.y.q.{\mathsf{Eq}}_{{\mathsf{Eq}}_A(x,y)}(q,{\mathsf{refl}}_x);z.{\mathsf{refl}}_{{\mathsf{refl}}_z};p):{\mathsf{Eq}}_{{\mathsf{Eq}}_A(a,b)}(p,{\mathsf{refl}}_a).$$ Finally apply Eq-Reflect to $r(p)$. Its conclusion is exactly $$\mathrm{\Gamma }⊢p\equiv {\mathsf{refl}}_a:{\mathsf{Eq}}_A(a,b),$$ where the classifier of ${\mathsf{refl}}_a$ has already been converted along the endpoint equality reflected from $p$. This is Eq-Uniq. The argument used only formation, introduction, reflection, and the stated $J$-eliminator.

Work in the extended context $\mathrm{\Gamma },u:B[a/x]$. Weakening preserves $p:{\mathsf{Eq}}_A(a,b)$, so reflection gives $a\equiv b:A$ there. Equal substitution into the family $B$ gives $$\mathrm{\Gamma },u:B[a/x]⊢B[a/x]\equiv B[b/x]\mathsf{type}.$$ Consequently the variable $u:B[a/x]$ converts to an element of $B[b/x]$, and $\mathrm{\Pi }$-introduction discharges it:

The occurrences of the family and of $p$ in the tree are obtained by weakening and exchange; these structural steps are suppressed exactly as in the book’s compressed rule convention.

Fix $a:A$ and $p:{\mathsf{Eq}}_A(a,a)$, and put $$D(x,q):={\mathsf{Eq}}_{{\mathsf{Eq}}_A(x,x)}(q,{\mathsf{refl}}_x).$$ At reflexivity the diagonal fiber is $$D(x,{\mathsf{refl}}_x)={\mathsf{Eq}}_{{\mathsf{Eq}}_A(x,x)}({\mathsf{refl}}_x,{\mathsf{refl}}_x),$$ with canonical inhabitant $d(x):={\mathsf{refl}}_{{\mathsf{refl}}_x}$. The derived $K$-operator of theorem 35.9(3) therefore gives $$k_p:=\mathsf{K}(x.q.D;x.d;a,p):D(a,p)={\mathsf{Eq}}_{{\mathsf{Eq}}_A(a,a)}(p,{\mathsf{refl}}_a).$$ By its definition in that theorem, $k_p\equiv d(a)\equiv {\mathsf{refl}}_{{\mathsf{refl}}_a}$; the classifier is changed from $D(a,{\mathsf{refl}}_a)$ to $D(a,p)$ using Eq-Uniq on $p$.

There is also the direct construction. Rule Eq-Uniq gives $p\equiv {\mathsf{refl}}_a:{\mathsf{Eq}}_A(a,a)$; hence Eq-I followed by conversion gives $$d_p:={\mathsf{refl}}_p:{\mathsf{Eq}}_{{\mathsf{Eq}}_A(a,a)}(p,{\mathsf{refl}}_a)=D(a,p).$$ The annotation on the printed reflexivity term is immaterial after the conversion: both $k_p$ and $d_p$ are judgmentally equal to the unique reflexivity inhabitant of $D(a,p)$. Thus $$\mathrm{\Gamma }⊢k_p\equiv d_p:D(a,p).$$ Applying theorem 35.7(1) at the ambient type $D(a,p)$ internalizes this comparison: $$\mathrm{\Gamma }⊢\mathsf{refl}:{\mathsf{Eq}}_{D(a,p)}(k_p,d_p).$$ So the $K$-construction and the direct uniqueness construction agree both judgmentally and internally.

Let $p:{\mathsf{Id}}_A(a,b)$, $q:{\mathsf{Id}}_A(b,c)$, and $u:B(a)$. By proposition 35.10, after the corresponding endpoint conversions, $$p\equiv {\mathsf{refl}}_a,q\equiv {\mathsf{refl}}_a.$$ Congruence therefore reduces the left-hand side of the transport law as follows: The right-hand side has the parallel calculation where the last two lines are the inner and outer instances of the transport computation rule. Transitivity gives the displayed law.

For inverse and composition, the same replacement gives Here $\mathsf{refl}\cdot \mathsf{refl}\equiv \mathsf{refl}$ is the computation rule for path composition and ${\mathsf{refl}}^{-1}\equiv \mathsf{refl}$ is the computation rule for inverse. Both sides are consequently judgmentally the same reflexivity term.

Suppose first that $A$ is a proposition. Every fiber $B(x)$ is a proposition by hypothesis, so $\sum _{x:A}B$ is a proposition by lemma 35.15(4).

Conversely, assume $S:=\sum _{x:A}B$ is a proposition. In the generic context $\mathrm{\Gamma },x:A,y:A$, the section gives $$(x,s(x)):S,(y,s(y)):S.$$ Proposition-hood of $S$ yields $$(x,s(x))\equiv (y,s(y)):S.$$ Apply congruence of the first projection and then the two $\mathrm{\Sigma }$-beta rules: $$x\equiv {\mathsf{pr}}_1((x,s(x)))\equiv {\mathsf{pr}}_1((y,s(y)))\equiv y:A.$$ This is precisely the generic judgment asserting that $A$ is a proposition. The section is essential for this direction: it embeds every $x:A$ into the dependent sum.

If $\mathbb{N}$ were a proposition, substitution into its generic equality would give $$\cdot ⊢\mathsf{0}\equiv \mathsf{suc}(\mathsf{0}):\mathbb{N}.$$ In the set interpretation of proposition 35.4, these terms denote $0$ and $1$, respectively. Soundness would force $0=1$, a contradiction. Hence $\mathbb{N}$ is not a proposition.

More generally, let $A$ be closed and let $a:A$ be closed. If $A+A$ were a proposition, then its two closed inhabitants would be judgmentally equal: $$\cdot ⊢\mathsf{inl}(a)\equiv \mathsf{inr}(a):A+A.$$ The set interpretation of a coproduct is a tagged disjoint union. The first term denotes the left-tagged element $(0,[[a]])$, while the second denotes the right-tagged element $(1,[[a]])$; these are unequal regardless of the value of $[[a]]$. Soundness rules out the displayed judgment, so $A+A$ is not a proposition.

Write $${\eta }_A:=\lambda a.|a|:A⟶\Vert A\Vert .$$ Assume first that $A$ is a proposition. Since Tr-E permits elimination into propositions, define $$r_A:=\lambda t.{\mathsf{rec}}_{\Vert A\Vert }(a.a,t):\Vert A\Vert ⟶A.$$ For every $a:A$, both $r_A({\eta }_A(a))$ and $a$ inhabit the proposition $A$, hence $r_A({\eta }_A(a))\equiv a$. Lambda congruence and $\mathrm{\Pi }$-eta give $$r_A\circ {\eta }_A\equiv \lambda a.a.$$ Likewise, for every $t:\Vert A\Vert$, the terms ${\eta }_A(r_A(t))$ and $t$ inhabit the proposition $\Vert A\Vert$, so $${\eta }_A\circ r_A\equiv \lambda t.t.$$ Thus the retraction is automatically a judgmental two-sided inverse; no computation rule for truncation is needed.

Conversely, suppose there is $r:\Vert A\Vert \to A$ with $r\circ {\eta }_A\equiv \lambda a.a$. In context $x:A,y:A$, rule Tr-Uniq gives ${\eta }_A(x)\equiv {\eta }_A(y)$. Application congruence and the retraction equation then give $$x\equiv r({\eta }_A(x))\equiv r({\eta }_A(y))\equiv y:A.$$ Therefore $A$ is a proposition.

Finally $\Vert A\Vert$ is always a proposition. Applying the first part to it gives the judgmental isomorphism $${\eta }_{\Vert A\Vert }:\Vert A\Vert ⟶\Vert \Vert A\Vert \Vert ,{\mu }_A:=\lambda T.{\mathsf{rec}}_{\Vert \Vert A\Vert \Vert }(t.t,T):\Vert \Vert A\Vert \Vert ⟶\Vert A\Vert ,$$ with both composites judgmentally equal to the corresponding identity functions.

For $f:A\to B$, define $$\Vert f\Vert :=\lambda t.{\mathsf{rec}}_{\Vert A\Vert }(x.|f(x)|,t):\Vert A\Vert ⟶\Vert B\Vert .$$ The branch has type $\Vert B\Vert$, and this target is a proposition by Tr-Uniq, so Tr-E applies.

For every $t:\Vert A\Vert$, the terms $(\Vert \lambda x.x\Vert )(t)$ and $t$ are two inhabitants of $\Vert A\Vert$. Proposition-hood gives their judgmental equality; lambda congruence followed by eta therefore gives $$\Vert \lambda x.x\Vert \equiv \lambda t.t.$$ Now let $f:A\to B$ and $g:B\to C$. For each $t:\Vert A\Vert$, both $$(\Vert g\circ f\Vert )(t)\text{and}(\Vert g\Vert )((\Vert f\Vert )(t))$$ inhabit the proposition $\Vert C\Vert$. Hence they are judgmentally equal, and extensional congruence for lambdas plus eta yields $$\Vert g\circ f\Vert \equiv (\Vert g\Vert )\circ (\Vert f\Vert ).$$ These functor laws use only uniqueness of inhabitants of the codomain truncations, not a primitive beta rule for Tr-E.

Recall $A\vee B:=\Vert A+B\Vert$. Define the symmetry map by $${\mathsf{swap}}_{A,B}(t):={\mathsf{rec}}_{\Vert A+B\Vert }(z.{\mathsf{ind}}_{+}(a.|\mathsf{inr}(a)|,b.|\mathsf{inl}(b)|,z),t).$$ Its codomain is $B\vee A=\Vert B+A\Vert$, hence a proposition, so the truncation elimination is valid. The reverse is ${\mathsf{swap}}_{B,A}$. Both composites are endomaps of a proposition; therefore, pointwise by Tr-Uniq and then by lambda congruence and eta, $${\mathsf{swap}}_{B,A}\circ {\mathsf{swap}}_{A,B}\equiv {\mathsf{id}}_{A\vee B},{\mathsf{swap}}_{A,B}\circ {\mathsf{swap}}_{B,A}\equiv {\mathsf{id}}_{B\vee A}.$$

For associativity abbreviate $$L:=(A\vee B)\vee C=\Vert \Vert A+B\Vert +C\Vert ,R:=A\vee (B\vee C)=\Vert A+\Vert B+C\Vert \Vert .$$ First define a helper $h:\Vert A+B\Vert \to R$ by $$h(w):={\mathsf{rec}}_{\Vert A+B\Vert }(z.{\mathsf{ind}}_{+}(a.|\mathsf{inl}(a)|,b.|\mathsf{inr}(|\mathsf{inl}(b)|)|,z),w).$$ Then set $$\alpha (t):={\mathsf{rec}}_{\Vert \Vert A+B\Vert +C\Vert }(z.{\mathsf{ind}}_{+}(w.h(w),c.|\mathsf{inr}(|\mathsf{inr}(c)|)|,z),t):R.$$ All recursors eliminate into the proposition $R$.

For the reverse map define $k:\Vert B+C\Vert \to L$ by $$k(w):={\mathsf{rec}}_{\Vert B+C\Vert }(z.{\mathsf{ind}}_{+}(b.|\mathsf{inl}(|\mathsf{inr}(b)|)|,c.|\mathsf{inr}(c)|,z),w),$$ and put $$\beta (t):={\mathsf{rec}}_{\Vert A+\Vert B+C\Vert \Vert }(z.{\mathsf{ind}}_{+}(a.|\mathsf{inl}(|\mathsf{inl}(a)|)|,w.k(w),z),t):L.$$ Again every truncation elimination has propositional target. Since both $L$ and $R$ are propositions, for every input the corresponding composite and identity value are judgmentally equal. Function congruence and eta therefore give $$\beta \circ \alpha \equiv {\mathsf{id}}_L,\alpha \circ \beta \equiv {\mathsf{id}}_R.$$ No nested computation calculation is required: truncation uniqueness makes all maps between the same proposition-valued source and target agree pointwise.

An element of ${\mathsf{Prop}}_0=\sum _{X:{\mathcal{U}}_0}\mathsf{isProp}(X)$ is a small type together with a term witnessing that any two of its elements are extensionally equal. Put $$q_{\mathbf{1}}:=\lambda x.\lambda y.\mathsf{refl},q_{\mathbf{0}}:=\lambda x.\lambda y.{\mathsf{abort}}_{{\mathsf{Eq}}_{\mathbf{0}}(x,y)}(x).$$ For $q_{\mathbf{1}}$, unit eta gives $x\equiv y$, so the printed reflexivity term converts to the required equality type. Hence the codes for truth and falsehood are $${\mathrm{\top }}_0:=(\mathbf{1},q_{\mathbf{1}}),{\mathrm{\perp }}_0:=(\mathbf{0},q_{\mathbf{0}}).$$

Let $\phi ,\psi :{\mathsf{Prop}}_0$, and abbreviate $$P:={\phi }^{\circ },Q:={\psi }^{\circ },q_P:={\mathsf{pr}}_2(\phi ),q_Q:={\mathsf{pr}}_2(\psi ).$$ For generic $u,v:P\times Q$, reflection applies to $$q_P({\mathsf{pr}}_{1}u)({\mathsf{pr}}_{1}v)\text{and}{q}_Q({\mathsf{pr}}_{2}u)({\mathsf{pr}}_{2}v).$$ Pair congruence and $\mathrm{\Sigma }$-eta then give $u\equiv v$. Thus $$q_{P\wedge Q}:=\lambda u.\lambda v.\mathsf{refl}:\mathsf{isProp}(P\times Q).$$ For generic $f,g:P\to Q$, reflection applied to $q_Q(f(x))(g(x))$ gives $f(x)\equiv g(x)$; lambda congruence and $\mathrm{\Pi }$-eta give $f\equiv g$. Hence $$q_{P\Rightarrow Q}:=\lambda f.\lambda g.\mathsf{refl}:\mathsf{isProp}(P\to Q).$$ The required elements are therefore $$\phi {\wedge }_0\psi :=(P\times Q,q_{P\wedge Q}),\phi {\Rightarrow }_0\psi :=(P\to Q,q_{P\Rightarrow Q}).$$ Universe closure under $\mathrm{\Sigma }$ and $\mathrm{\Pi }$ places both first components in ${\mathcal{U}}_0$.

More generally, suppose $A:{\mathcal{U}}_0$, $x:A⊢B:{\mathcal{U}}_0$, and $q:\prod _{x:A}\mathsf{isProp}(B)$. Rule U-Pi gives $\prod _{x:A}B:{\mathcal{U}}_0$. Define $$q_{\mathrm{\Pi }}:=\lambda f.\lambda g.\mathsf{refl}.$$ Indeed, in context $x:A$, reflection applied to $q(x)(f(x))(g(x))$ gives $f(x)\equiv g(x):B$; lambda congruence and eta give $f\equiv g$. Thus $$(\prod _{x:A}B,q_{\mathrm{\Pi }}):{\mathsf{Prop}}_0$$ has the requested underlying type.

Now let $A:{\mathcal{U}}_0$ and $a,b:A$. Rule Eq-Form-U gives $$\mathrm{\Gamma }⊢{\mathsf{Eq}}_A(a,b):{\mathcal{U}}_0.$$ For generic $p,r:{\mathsf{Eq}}_A(a,b)$, two applications of Eq-Uniq give $p\equiv \mathsf{refl}\equiv r$. Consequently $$q_{=}:=\lambda p.\lambda r.\mathsf{refl}:\mathsf{isProp}({\mathsf{Eq}}_A(a,b)),$$ and the desired equality proposition is represented by $$({\mathsf{Eq}}_A(a,b),q_{=}):{\mathsf{Prop}}_0.$$

Finally assume a small truncation code, so that $T:{\mathcal{U}}_0$ implies $\Vert T\Vert :{\mathcal{U}}_0$ with the stated decoding equation. Universe closure first gives $\sum _{x:A}B:{\mathcal{U}}_0$ and $P+Q:{\mathcal{U}}_0$. Rule Tr-Uniq makes each truncation a proposition; explicit witnesses are $$q_{\mathrm{\exists }}:=\lambda u.\lambda v.\mathsf{refl},q_{\vee }:=\lambda u.\lambda v.\mathsf{refl},$$ where the displayed reflexivity terms typecheck after the corresponding Tr-Uniq judgment $u\equiv v$. Hence $$(\Vert \sum _{x:A}B\Vert ,q_{\mathrm{\exists }}),(\Vert P+Q\Vert ,q_{\vee }):{\mathsf{Prop}}_0$$ are the universe-coded existential and disjunction.

In $T_I$, define the motive $$M(x,y,q):=\prod _{r:{\mathsf{Id}}_A(x,y)}{\mathsf{Id}}_{{\mathsf{Id}}_A(x,y)}(r,q).$$ At the diagonal it becomes $$M(z,z,{\mathsf{refl}}_z)=\prod _{r:{\mathsf{Id}}_A(z,z)}{\mathsf{Id}}_{{\mathsf{Id}}_A(z,z)}(r,{\mathsf{refl}}_z),$$ so the required branch is exactly $$z.\lambda r.\mathsf{uip}(r).$$ The full primitive two-endpoint $J$-term is therefore $$U(q):=\mathsf{J}(x.y.q.\prod _{r:{\mathsf{Id}}_A(x,y)}{\mathsf{Id}}_{{\mathsf{Id}}_A(x,y)}(r,q);z.\lambda r.\mathsf{uip}(r);q).$$ For arbitrary $a,b:A$ and $q:{\mathsf{Id}}_A(a,b)$, rule Id-elim gives $$U(q):\prod _{r:{\mathsf{Id}}_A(a,b)}{\mathsf{Id}}_{{\mathsf{Id}}_A(a,b)}(r,q).$$ Consequently, for $p,q:{\mathsf{Id}}_A(a,b)$, $$U(q)(p):{\mathsf{Id}}_{{\mathsf{Id}}_A(a,b)}(p,q),$$ which is the required general UIP inhabitant. At $q={\mathsf{refl}}_a$, the primitive computation rule verifies $$U({\mathsf{refl}}_a)\equiv \lambda r.\mathsf{uip}(r):M(a,a,{\mathsf{refl}}_a),$$ so the diagonal clause and the arbitrary-endpoint classifier both agree literally with the statement of the exercise.

For Conv, suppose the final source rule is $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢a:A\\ \mathrm{\Gamma }⊢A\equiv A^{\prime }\mathsf{type}\end{array}}{\mathrm{\Gamma }⊢a:A^{\prime }}\mathrm{Conv}.$$ The induction hypotheses give $$\mathrm{strip}(\mathrm{\Gamma })⊢\mathrm{strip}(a):\mathrm{strip}(A),\mathrm{strip}(\mathrm{\Gamma })⊢\mathrm{strip}(A)\equiv \mathrm{strip}(A^{\prime })\mathsf{type}.$$ Applying Conv in $T_E$ gives $\mathrm{strip}(\mathrm{\Gamma })⊢\mathrm{strip}(a):\mathrm{strip}(A^{\prime })$, which is exactly the stripping of the source conclusion. No special equation about the two new constants is needed in this case.

For Subst-Eq-Ty, suppose the source derivation ends in $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢a\equiv a^{\prime }:A\\ \mathrm{\Gamma },x:A,\mathrm{\Delta }⊢B\mathsf{type}\end{array}}{\mathrm{\Gamma },\mathrm{\Delta }[a/x]⊢B[a/x]\equiv B[a^{\prime }/x]\mathsf{type}}\mathrm{Subst}-\mathrm{Eq}-\mathrm{Ty}.$$ For compactness in this case put $$\begin{array}{c}G:=\mathrm{strip}(\mathrm{\Gamma }),D:=\mathrm{strip}(\mathrm{\Delta }),A_{\mathrm{s}}:=\mathrm{strip}(A),\\ a_{\mathrm{s}}:=\mathrm{strip}(a),a_{\mathrm{s}}^{\prime }:=\mathrm{strip}(a^{\prime }),B_{\mathrm{s}}:=\mathrm{strip}(B).\end{array}$$ The induction hypotheses are $$G⊢a_{\mathrm{s}}\equiv a_{\mathrm{s}}^{\prime }:A_{\mathrm{s}},G,x:A_{\mathrm{s}},D⊢B_{\mathrm{s}}\mathsf{type}.$$ Apply Subst-Eq-Ty in $T_E$: $$G,D[a_{\mathrm{s}}/x]⊢B_{\mathrm{s}}[a_{\mathrm{s}}/x]\equiv B_{\mathrm{s}}[a_{\mathrm{s}}^{\prime }/x]\mathsf{type}.$$ By lemma 35.28, componentwise also for telescopes, Substituting these literal equalities into the last judgment gives the componentwise stripping of the source conclusion: its context is $\mathrm{strip}(\mathrm{\Gamma },\mathrm{\Delta }[a/x])$, and its two types are $\mathrm{strip}(B[a/x])$ and $\mathrm{strip}(B[a^{\prime }/x])$. This is the point at which commutation of stripping with capture-avoiding substitution is load-bearing rather than cosmetic.

Define the iterate $i:\mathbb{N}\to \mathbb{N}$ by primitive recursion: $$i(\mathsf{0})\equiv \mathsf{0},i(\mathsf{suc}n)\equiv \mathsf{suc}(i(n)).$$ This is the term denoted ${\mathsf{suc}}^x(\mathsf{0})$ when evaluated at $x$. Use the motive $$C(x):={\mathsf{Id}}_{\mathbb{N}}(x,i(x)).$$ The base case is $c_0:={\mathsf{refl}}_{\mathsf{0}}:C(\mathsf{0})$, since $i(\mathsf{0})\equiv \mathsf{0}$. For the step, assume $n:\mathbb{N}$ and $p:C(n)$. Congruence of successor gives $${\mathsf{ap}}_{\mathsf{suc}}(p):{\mathsf{Id}}_{\mathbb{N}}(\mathsf{suc}n,\mathsf{suc}(i(n))).$$ Because $i(\mathsf{suc}n)\equiv \mathsf{suc}(i(n))$, conversion gives ${\mathsf{ap}}_{\mathsf{suc}}(p):C(\mathsf{suc}n)$. Hence Nat elimination constructs $$P:=\lambda x.{\mathsf{ind}}_{\mathbb{N}}(x.C(x);c_0,n.p.{\mathsf{ap}}_{\mathsf{suc}}(p);x):\prod _{x:\mathbb{N}}{\mathsf{Id}}_{\mathbb{N}}(x,i(x)).$$ In particular, in context $x:\mathbb{N}$, $$x:\mathbb{N}⊢P(x):{\mathsf{Id}}_{\mathbb{N}}(x,{\mathsf{suc}}^x(\mathsf{0})).$$ Applying Id-Reflect in $T_E$ yields $$x:\mathbb{N}⊢x\equiv {\mathsf{suc}}^x(\mathsf{0}):\mathbb{N}.$$ This is only a derivability claim in the extensional theory. The construction supplies no converse theorem asserting that the displayed judgmental equation is underivable in $T_I$.

Every code $⌜t⌝$ has type $X$ in ${\mathrm{\Gamma }}_{\mathsf{SK}}$. The closure cases in the induction proving lemma 35.46 are therefore as follows.

For encoded reflexivity, term reflexivity gives $$\frac{{\mathrm{\Gamma }}_{\mathsf{SK}}⊢⌜t⌝:X}{{\mathrm{\Gamma }}_{\mathsf{SK}}⊢⌜t⌝\equiv ⌜t⌝:X}\mathrm{Tm}-\mathrm{Refl}.$$ If the induction hypothesis for $t\sim u$ is $⌜t⌝\equiv ⌜u⌝:X$, term symmetry gives $$⌜u⌝\equiv ⌜t⌝:X.$$ If the hypotheses for $t\sim u$ and $u\sim v$ give $$⌜t⌝\equiv ⌜u⌝:X,⌜u⌝\equiv ⌜v⌝:X,$$ term transitivity gives $⌜t⌝\equiv ⌜v⌝:X$.

For SK-App, suppose $$⌜t⌝\equiv ⌜t^{\prime }⌝:X,⌜u⌝\equiv ⌜u^{\prime }⌝:X.$$ Since $app:\prod _{x:X}\prod _{y:X}X$, application congruence first gives $$app⌜t⌝\equiv app⌜t^{\prime }⌝:\prod _{y:X}X,$$ and a second application-congruence step gives $$app⌜t⌝⌜u⌝\equiv app⌜t^{\prime }⌝⌜u^{\prime }⌝:X.$$ By the recursive definition of coding, this is $$⌜tu⌝\equiv ⌜t^{\prime }{u}^{\prime }⌝:X.$$

The two generating conversion cases are the only places where an equation hypothesis from the context is consumed. Specifically, $$e_K⌜t⌝⌜u⌝:{\mathsf{Eq}}_X(⌜\mathsf{K}tu⌝,⌜t⌝)$$ and $$e_S⌜t⌝⌜u⌝⌜v⌝:{\mathsf{Eq}}_X(⌜\mathsf{S}tuv⌝,⌜(tv)(uv)⌝)$$ are reflected by Eq-Reflect. All remaining steps are typing, structural rules, or the reflexive, symmetric, transitive, and congruence closure of judgmental equality. Thus $e_K$ and $e_S$ are exactly the nonstructural equation families used by the soundness proof.

Let $$\mathrm{\Gamma }:=X:{\mathcal{U}}_0,p:{\mathsf{Eq}}_{{\mathcal{U}}_0}(X,X\to X).$$ First, Var gives $X:{\mathcal{U}}_0$. Weakening this judgment to $\mathrm{\Gamma },x:X$, followed by U-Pi, gives $$\mathrm{\Gamma }⊢X\to X:{\mathcal{U}}_0.$$ Consequently Eq-F forms the declared type of $p$, and Var gives $$\mathrm{\Gamma }⊢p:{\mathsf{Eq}}_{{\mathcal{U}}_0}(X,X\to X).$$ There is exactly one use of equality reflection in the derivation: $$\frac{\mathrm{\Gamma }⊢p:{\mathsf{Eq}}_{{\mathcal{U}}_0}(X,X\to X)}{\mathrm{\Gamma }⊢X\equiv X\to X:{\mathcal{U}}_0}\mathrm{Eq}-\mathrm{Reflect}.$$ Rule U-El-Eq converts this equality between universe elements into an equality of types: $$E:\mathrm{\Gamma }⊢X\equiv X\to X\mathsf{type}.$$ Every later use of the identification is an ordinary conversion along $E$ or its weakening, not another use of Eq-Reflect.

In context $\mathrm{\Gamma },x:X$, variable formation gives $x:X$. Converting that same variable along $E$ gives $x:X\to X$. Hence $\mathrm{\Pi }$-elimination derives $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}\mathrm{\Gamma },x:X⊢x:X\\ \mathrm{\Gamma },x:X⊢X\equiv X\to X\mathsf{type}\end{array}}{\mathrm{\Gamma },x:X⊢x:X\to X}}\mathrm{Conv}\\ \mathrm{\Gamma },x:X⊢x:X\end{array}}{\mathrm{\Gamma },x:X⊢xx:X}\mathrm{\Pi }-\mathrm{E}.$$ Discharging $x$ gives $$\omega :=\lambda x.xx:X\to X.$$ Symmetry of $E$ and Conv also give $\omega :X$. The final application therefore has the complete typing step $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢\omega :X\to X\\ {\displaystyle \frac{\begin{array}{c}\mathrm{\Gamma }⊢\omega :X\to X\\ \mathrm{\Gamma }⊢X\to X\equiv X\mathsf{type}\end{array}}{\mathrm{\Gamma }⊢\omega :X}}\mathrm{Conv}\end{array}}{\mathrm{\Gamma }⊢\omega \omega :X}\mathrm{\Pi }-\mathrm{E}.$$ Thus $\mathrm{\Omega }:=\omega \omega :X$, and ordinary beta reduction gives $$\mathrm{\Omega }{⟶}_{\beta }(\lambda x.xx)(\lambda x.xx)=\mathrm{\Omega }.$$ The sole reflection step is the one displayed above; its consequence is reused structurally throughout the derivation.