ch:pi-sigma-unit: ch:pi-sigma-unit

Composition was defined by $g\circ f:=\lambda (x:A).g(fx)$. Hence the two equations are direct $\beta$-computations followed by congruence under abstraction; the second also uses app-eq, since its redex lies in the argument of $g$: In context $\mathrm{\Gamma },z:C$, In context $\mathrm{\Gamma },y:B$, The original $f$ and $g$ are weakened into the displayed extended contexts. The superscript records the domain and codomain of each constant map; the freshness conditions on $x,x^{\prime }$ are supplied by alpha-renaming.

For a fresh $u:\mathbf{1}$, the unit uniqueness rule gives $fu\equiv \star$ and $gu\equiv \star$. Symmetry of the second equality gives $fu\equiv gu$. Congruence for abstraction and the two $\mathrm{\Pi }$-uniqueness equations therefore give $$f\equiv \lambda (u:\mathbf{1}).fu\equiv \lambda (u:\mathbf{1}).\star \equiv \lambda (u:\mathbf{1}).gu\equiv g.$$ The third step uses symmetry of unit uniqueness for $gu$, and the last step uses symmetry of function eta for $g$. Taking $g={\mathrm{id}}_{\mathbf{1}}$ yields the final claim. The argument uses both $\mathbf{1}$-$\eta$, to identify the values, and $\mathrm{\Pi }$-$\eta$, to identify the functions.

For $p:\sum _{x:A}B$, use the positive eliminator with constant motive $A$ and branch $x$: $${\mathsf{pr}}_1(p):={\mathsf{ind}}_{\mathrm{\Sigma }}(x;p):A.$$ Its pair computation gives ${\mathsf{pr}}_1((a,b))\equiv a$. Next use the motive $C(z):=B[{\mathsf{pr}}_1(z)/x]$ and branch $y$. The first projection equation converts $y:B[x/x]$ to the required $B[{\mathsf{pr}}_1((x,y))/x]$, so $${\mathsf{pr}}_2(p):={\mathsf{ind}}_{\mathrm{\Sigma }}(y;p):B[{\mathsf{pr}}_1(p)/x],$$ and positive computation yields ${\mathsf{pr}}_2((a,b))\equiv b$ after the same conversion.

Conversely define elimination by substituting the projections into the branch: $${\mathsf{ind}}_{\mathrm{\Sigma }}(z.C;d;p):=d[{\mathsf{pr}}_1(p)/x,{\mathsf{pr}}_2(p)/y].$$ Projection beta proves its pair computation. Typing the displayed term first places it in $C[({\mathsf{pr}}_1(p),{\mathsf{pr}}_2(p))/z]$; judgmental $\mathrm{\Sigma }$-eta is used exactly once to convert this type to $C[p/z]$.

For $h:\prod _{p:\sum _{x:A}B}C(p)$, put $\mathsf{curry}(h):=\lambda x.\lambda y.h(x,y)$; in the reverse direction put $\mathsf{uncurry}(k):=\lambda p.k({\mathsf{pr}}_1(p))({\mathsf{pr}}_2(p))$. Then $$\mathsf{uncurry}(\mathsf{curry}(h))\stackrel{\mathrm{\Pi }-\beta }{=}\lambda p.h({\mathsf{pr}}_1(p),{\mathsf{pr}}_2(p))\stackrel{\mathrm{\Sigma }-\eta }{=}h$$ and $$\mathsf{curry}(\mathsf{uncurry}(k))\stackrel{\mathrm{\Pi }-\beta ,\mathrm{\Sigma }-\beta }{=}\lambda x.\lambda y.kxy\stackrel{\mathrm{\Pi }-\eta }{=}k.$$ For $C(p):={\mathsf{Id}}_{\sum _{x:A}B}(p,p)$, replacing judgmental $\mathrm{\Sigma }$-eta by a path makes the first round trip only propositionally, not judgmentally, equal to $h$.

Both terms are beta-normal. The neutral form $p$ has a variable at its head, whereas $({\mathsf{pr}}_1(p),{\mathsf{pr}}_2(p))$ has a pair constructor at its head; no beta rule relates them. Consequently the uncurry–curry composite stops at $$\lambda p.h(({\mathsf{pr}}_1(p),{\mathsf{pr}}_2(p)))$$ instead of reducing judgmentally to $h$. A propositional $\mathrm{\Sigma }$-eta witness permits congruence to construct a propositional equality between the two maps, followed by function extensionality if equality of functions is wanted. It does not turn the stalled normal forms into a judgmental equality, so the result is a propositional rather than definitional isomorphism.

The simply typed function rules, reorganized in the fourfold order, are

If judgmental equality is added, the computation and uniqueness rules are

with $x\notin \mathrm{FV}(f)$. The chapter on simple typing has no judgmental-equality judgment, so these last two displays are an extension of that calculus, not a reclassification of rules already present there.

For $\mathrm{\Pi }$-types, the codomain is no longer a fixed type $B$ in $\mathrm{\Gamma }$, but a family $B$ formed in $\mathrm{\Gamma },x:A$. Consequently:

• formation assumes $B\mathsf{type}$ in the extended context;

• the abstraction body has the dependent type $B$ there;

• application to $a$ has type $B[a/x]$, rather than $B$;

• the beta equation is likewise classified by $B[a/x]$;

• in eta, the generic application $fx$ has type $B$ in $\mathrm{\Gamma },x:A$.

The arrow rules are exactly the constant-family specialization in which $x\notin \mathrm{FV}(B)$, so every displayed fiber $B[a/x]$ is literally $B$.

Assume first $\mathrm{\Pi }$-$\eta$. From $$\mathrm{\Gamma },x:A⊢fx\equiv gx:B$$ and reflexive equalities for the domain and family, abstraction congruence gives $$\mathrm{\Gamma }⊢\lambda (x:A).fx\equiv \lambda (x:A).gx:\prod _{x:A}B.$$ The two eta instances are $$f\equiv \lambda (x:A).fx,g\equiv \lambda (x:A).gx.$$ Therefore, using symmetry on the second and transitivity, $$f\equiv \lambda (x:A).fx\equiv \lambda (x:A).gx\equiv g:\prod _{x:A}B.$$ This is extensionality.

Conversely, assume the extensionality rule and take $f:\prod _{x:A}B$. Put $$g:=\lambda (x:A).fx.$$ It is well typed by $\mathrm{\Pi }$-intro. In the generic context $\mathrm{\Gamma },x:A$, choose a fresh binder $y$ for the displayed abstraction. The beta rule gives $$(\lambda (y:A).fy)x\equiv fx:B.$$ After symmetry this is the pointwise premise $fx\equiv gx:B$. Extensionality now yields $$f\equiv g=\lambda (x:A).fx:\prod _{x:A}B,$$ which is precisely $\mathrm{\Pi }$-$\eta$. Thus, with the remaining product rules fixed, eta and judgmental function extensionality are interderivable.

Choose $x$ fresh for $f$. In context $\mathrm{\Gamma },x:A$, beta for the identity gives $$\mathrm{\Gamma },x:A⊢{\mathrm{id}}_{A}x\equiv x:A.$$ Application congruence, using reflexivity of $f:A\to B$, therefore gives

Abstraction congruence lifts this equality out of the generic context:

By definition the left side is $f\circ {\mathrm{id}}_A$. Eta gives $f\equiv \lambda (x:A).fx$; after symmetry, $\lambda (x:A).fx\equiv f$. Transitivity now yields $$\mathrm{\Gamma }⊢f\circ {\mathrm{id}}_A\equiv f:A\to B.$$ Thus the beta step is transported first through application and then through abstraction, while eta removes the final generic abstraction.

Assume first the ordinary beta rule and a derivation $\mathrm{\Gamma },x:A⊢b:B$. Rename the local declaration from $x$ to a fresh $y$, obtaining $$\mathrm{\Gamma },y:A⊢b[y/x]:B[y/x].$$ Weakening inserts a fresh declaration $x:A$ before $y:A$, and $\mathrm{\Pi }$-$\beta$ in ambient context $\mathrm{\Gamma },x:A$ gives $$(\lambda (y:A).b[y/x])x\equiv (b[y/x])[x/y]:(B[y/x])[x/y].$$ The two successive fresh substitutions undo one another on a clean display, so the right side and its type are respectively $b$ and $B$. This is the generic beta instance.

For the converse, assume all such generic instances. Start with $\mathrm{\Gamma },x:A⊢b:B$ and $\mathrm{\Gamma }⊢a:A$. Choose $y$ fresh for $\mathrm{\Gamma },A,B,b,a$, rename the body to $d:=b[y/x]$ in context $\mathrm{\Gamma },y:A$, and use the assumed generic instance there, taking the fresh abstraction binder to be $x$: $$\mathrm{\Gamma },y:A⊢(\lambda (x:A).d[x/y])y\equiv d:B[y/x].$$ Since $d[x/y]=(b[y/x])[x/y]=b$, this is $$\mathrm{\Gamma },y:A⊢(\lambda (x:A).b)y\equiv b[y/x]:B[y/x].$$ Substitute $a$ for $y$. The left side becomes $(\lambda (x:A).b)a$. For the right side, apply proposition 26.11.4 with the successive substitutions $[y/x]$ and $[a/y]$: because $x\ne y$, $x\notin \mathrm{FV}(a)$, and $y\notin \mathrm{FV}(b)$, $$(b[y/x])[a/y]=b[a/y][y[a/y]/x]=b[a/x].$$ The identical calculation gives $(B[y/x])[a/y]=B[a/x]$. Hence substitution of the generic equation yields $$\mathrm{\Gamma }⊢(\lambda (x:A).b)a\equiv b[a/x]:B[a/x],$$ the ordinary beta rule.

Since $B$ is formed already in $\mathrm{\Gamma }$, Exch applied to $\mathrm{\Gamma },x:A,y:B⊢C\mathsf{type}$ gives $$\mathrm{\Gamma },y:B,x:A⊢C\mathsf{type}.$$ Thus the same raw family can be used after swapping the two independent arguments. Put $$F:=\prod _{x:A}\prod _{y:B}C,F^{\prime }:=\prod _{y:B}\prod _{x:A}C,$$ and define Successive applications and abstractions give $$\sigma :(\prod _{x:A}\prod _{y:B}C)\to (\prod _{y:B}\prod _{x:A}C),$$ and ${\sigma }^{\prime }$ has the reverse type. The uses of $C$ in the body of $\sigma$ are licensed by the exchanged formation judgment above.

For a generic $f:F$, repeated beta and congruence give $${\sigma }^{\prime }(\sigma f)\equiv \lambda (x:A).\lambda (y:B).fxy.$$ In context $\mathrm{\Gamma },f:F,x:A$, eta for the inner product gives $$\lambda (y:B).fxy\equiv fx.$$ Abstraction congruence yields $$\lambda (x:A).\lambda (y:B).fxy\equiv \lambda (x:A).fx,$$ and a second eta step gives $\lambda (x:A).fx\equiv f$. Hence $${\sigma }^{\prime }(\sigma f)\equiv f:F.$$ Abstracting over $f$ shows $${\sigma }^{\prime }\circ \sigma =\lambda (f:F).{\sigma }^{\prime }(\sigma f)\equiv \lambda (f:F).f={\mathrm{id}}_F.$$ The symmetric calculation proves $\sigma \circ {\sigma }^{\prime }\equiv \mathrm{id}$ on the swapped product. Each round trip uses eta once for the inner argument and once for the outer argument.

We list the normally suppressed judgments and indicate how the natural type of each right-hand term is moved to the common type displayed in the equality.

For pair-eq, the expanded data are $$\begin{array}{c}\mathrm{\Gamma }\mathsf{ctx},\mathrm{\Gamma }⊢A\mathsf{type},\mathrm{\Gamma },x:A⊢B\mathsf{type},\mathrm{\Gamma }⊢\sum _{x:A}B\mathsf{type},\\ \mathrm{\Gamma }⊢a:A,\mathrm{\Gamma }⊢a^{\prime }:A,\mathrm{\Gamma }⊢a\equiv a^{\prime }:A,\\ \mathrm{\Gamma }⊢B[a/x]\mathsf{type},\mathrm{\Gamma }⊢B[a^{\prime }/x]\mathsf{type},\\ \mathrm{\Gamma }⊢b:B[a/x],\mathrm{\Gamma }⊢b^{\prime }:B[a/x],\mathrm{\Gamma }⊢b\equiv b^{\prime }:B[a/x].\end{array}$$ Equal substitution in $B$ gives $$\mathrm{\Gamma }⊢B[a/x]\equiv B[a^{\prime }/x]\mathsf{type}.$$ Consequently Conv types the same raw term $b^{\prime }$ at its natural right-pair fiber $B[a^{\prime }/x]$. The two intro instances then supply $$(a,b):\sum _{x:A}B,(a^{\prime },b^{\prime }):\sum _{x:A}B,$$ which are the direct presuppositions of the pair equality. With all of these premises restored, pair-eq concludes $$\mathrm{\Gamma }⊢(a,b)\equiv (a^{\prime },b^{\prime }):\sum _{x:A}B.$$

For ${\mathsf{pr}}_1$-eq, restore $$\begin{array}{c}\mathrm{\Gamma }\mathsf{ctx},\mathrm{\Gamma }⊢A\mathsf{type},\mathrm{\Gamma },x:A⊢B\mathsf{type},\mathrm{\Gamma }⊢\sum _{x:A}B\mathsf{type},\\ \mathrm{\Gamma }⊢p:\sum _{x:A}B,\mathrm{\Gamma }⊢p^{\prime }:\sum _{x:A}B,\mathrm{\Gamma }⊢p\equiv p^{\prime }:\sum _{x:A}B,\\ \mathrm{\Gamma }⊢{\mathsf{pr}}_1(p):A,\mathrm{\Gamma }⊢{\mathsf{pr}}_1(p^{\prime }):A.\end{array}$$ The last line consists of the two projection-elimination instances and is the direct term presupposition of the conclusion ${\mathsf{pr}}_1(p)\equiv {\mathsf{pr}}_1(p^{\prime }):A$.

For ${\mathsf{pr}}_2$-eq, put $$q:={\mathsf{pr}}_1(p),q^{\prime }:={\mathsf{pr}}_1(p^{\prime }),r:={\mathsf{pr}}_2(p),r^{\prime }:={\mathsf{pr}}_2(p^{\prime }).$$ In addition to all the context, family, sum, and package judgments listed for ${\mathsf{pr}}_1$-eq, restore $$\begin{array}{c}\mathrm{\Gamma }⊢q:A,\mathrm{\Gamma }⊢q^{\prime }:A,\mathrm{\Gamma }⊢q\equiv q^{\prime }:A,\\ \mathrm{\Gamma }⊢B[q/x]\mathsf{type},\mathrm{\Gamma }⊢B[q^{\prime }/x]\mathsf{type},\\ \mathrm{\Gamma }⊢r:B[q/x],\mathrm{\Gamma }⊢r^{\prime }:B[q^{\prime }/x].\end{array}$$ The equality of first projections is the preceding congruence rule. The requested transport of the right-hand second projection is the literal tree

Together with $r:B[q/x]$, this supplies the direct term presuppositions of $$\mathrm{\Gamma }⊢r\equiv r^{\prime }:B[q/x].$$ Thus every equality is stated in one common fiber, even though the natural type of $r^{\prime }$ is the fiber over $q^{\prime }$.

Use Subst with empty telescope and with the generic thesis $B\mathsf{type}$:

Hence $B[a/x]$ is a formed type before the premise $\mathrm{\Gamma }⊢b:B[a/x]$ is even considered. This is the meta-well-typedness required by convention 26.14; the structural substitution rule supplies it from the family and the first component.

Choose $x$ fresh for $B$. Weakening forms $B$ in $\mathrm{\Gamma },x:A$, and the dependent-sum rules specialize to

All fibers $B[a/x]$ have simplified to $B$.

Given $f:A\to (B\to C)$ and $p:A\times B$, define $${\mathsf{rec}}_{\times }(f;p):=f({\mathsf{pr}}_1(p))({\mathsf{pr}}_2(p)):C.$$ For $a:A$ and $b:B$, the two projection beta equations and two uses of application congruence give Thus the non-dependent recursor computes by $${\mathsf{rec}}_{\times }(f;(a,b))\equiv fab:C.$$

Work in the positive presentation. First define $${\mathsf{pr}}_1(p):={\mathsf{ind}}_{\mathrm{\Sigma }}(x;p)$$ using the constant motive $C_1:=A$, formed in the package context, and branch $x:A$. The primitive computation rule gives $${\mathsf{pr}}_1((a,b))\equiv a:A.$$

Now let $z:\sum _{x:A}B$ and define the second motive $$C_2:=B[{\mathsf{pr}}_1(z)/x]\text{in context }z:\sum _{x:A}B.$$ It is a type because ${\mathsf{pr}}_1(z):A$ and ordinary substitution forms the corresponding fiber. In the branch context $\mathrm{\Gamma },x:A,y:B$, the eliminator requires a term of $$C_2[(x,y)/z]=B[{\mathsf{pr}}_1((x,y))/x].$$ The first-projection computation equation gives $$\mathrm{\Gamma },x:A,y:B⊢{\mathsf{pr}}_1((x,y))\equiv x:A.$$ Applying equal substitution to the family $B$ yields $$B[{\mathsf{pr}}_1((x,y))/x]\equiv B[x/x]=B\mathsf{type}.$$ After symmetry, the required branch typing is

We may therefore define $${\mathsf{pr}}_2(p):={\mathsf{ind}}_{\mathrm{\Sigma }}(y;p):B[{\mathsf{pr}}_1(p)/x].$$

On a displayed pair, primitive computation gives $${\mathsf{ind}}_{\mathrm{\Sigma }}(y;(a,b))\equiv y[a/x,b/y]=b:B[{\mathsf{pr}}_1((a,b))/x].$$ The first-projection beta equation and equal substitution identify this type with $B[a/x]$; Conv-Eq therefore yields the familiar rule $${\mathsf{pr}}_2((a,b))\equiv b:B[a/x].$$ For an arbitrary variable $p$, however, the primitive eliminator is neutral: its computation rule matches only a scrutinee whose outer form is $(a,b)$. With no eta or uniqueness rule in the positive presentation, nothing derives $p\equiv ({\mathsf{pr}}_1(p),{\mathsf{pr}}_2(p))$.

Let ${\mathcal{D}}_C:\mathrm{\Gamma },z:\mathbf{1}⊢C\mathsf{type}$, ${\mathcal{D}}_c:\mathrm{\Gamma }⊢c:C[\star /z]$, and ${\mathcal{D}}_a:\mathrm{\Gamma }⊢a:\mathbf{1}$. The typing derivation is

Since ${\mathsf{ind}}_{\mathbf{1}}(c;a):=c$, the conclusion is exactly $\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbf{1}}(c;a):C[a/z]$. The computation judgment at $\star$ is the reflexivity tree

The raw term on the left is definitionally $c$, so no beta rule is hidden in this last step.

Choose the family binder $x$ fresh for $B$, so $B[a/x]=B$ for every $a$. The dependent sum on the right side of theorem 27.22 then becomes an ordinary Cartesian product. The maps are Projection and pair congruence make both definitions independent of the chosen representatives.

The first round trip is by the two beta rules. The other is by symmetry of $\mathrm{\Sigma }$-$\eta$. Hence the two maps are inverse bijections.

Use the notation and hypotheses of theorem 27.21(2). The local product variable $x$ is distinct from the context variable $y$. Moreover, scoping gives $\mathrm{FV}(c)\subseteq \mathrm{dom}({\mathrm{\Gamma }}_0)$, while $x\notin \mathrm{dom}({\mathrm{\Gamma }}_0)$; hence $x\notin \mathrm{FV}(c)$.

Choose all other displayed binders away from $y$ and $\mathrm{FV}(c)$. The abstraction clause of capture-avoiding substitution then applies without freshening: $$\mathrm{\Lambda }(b)[c/y]=(\lambda (x:A).b)[c/y]=\lambda (x:A[c/y]).b[c/y]=\mathrm{\Lambda }(b[c/y]).$$ The condition $x\ne y$ ensures that substitution passes through rather than replacing the binder, and $x\notin \mathrm{FV}(c)$ ensures that the inserted term is not captured by that binder.

For evaluation, weakening changes the derivation of $f$ but not its raw expression. The application clause gives The third line uses $x\ne y$. The condition $x\notin \mathrm{FV}(c)$ is what makes the substituted context still extend by the same fresh declaration $x:A[c/y]$, and it is also the side condition for the substitution-composition identity identifying all dependent result fibers. Thus the equalities are literal equalities of clean raw displays and therefore equalities of judgmental classes.

Let $U_{\mathrm{\Gamma }}:\mathrm{Tm}(\mathrm{\Gamma },\mathbf{1})\to \{\ast \}$ be the unique map $U_{\mathrm{\Gamma }}([a])=\ast$, with inverse $V_{\mathrm{\Gamma }}(\ast )=[\star ]$. Under a context substitution $[c/y]:\mathrm{\Gamma }\to \mathrm{\Gamma }[c/y]$, term substitution defines $$S_c:\mathrm{Tm}(\mathrm{\Gamma },\mathbf{1})⟶\mathrm{Tm}(\mathrm{\Gamma }[c/y],\mathbf{1}),S_c([a])=[a[c/y]].$$ This is well defined because structural substitution preserves term equality. The analogue of theorem 27.21(2) is the commutative square Indeed, the two composites send a class $[a]$ respectively to $$[a]⟼\ast ⟼\ast \text{and}[a]⟼[a[c/y]]⟼\ast .$$ They are the same unique map.

The inverse maps commute as well. From the singleton, the two composites are $$\ast ⟼[\star ]⟼[\star [c/y]]\text{and}\ast ⟼\ast ⟼[\star ].$$ The nullary-operator clause of substitution gives $\star [c/y]=\star$, so both return $[\star ]$. Thus the singleton bijection is natural under context substitution in both directions.

Take the assumed judgment $\mathrm{\Gamma }⊢P\mathsf{type}$ as the formation rule. The introduction operation is $$\frac{\mathrm{\Gamma },x:A⊢b:B}{\mathrm{\Gamma }⊢{\mathrm{\Lambda }}^{\prime }(b):P}.$$ For elimination, weaken $f:P$ to $\mathrm{\Gamma },x:A$, apply $E^{\prime }$, and then substitute the argument:

Define the resulting raw operation by $$fa:=E^{\prime }(f)[a/x].$$

For beta, start with the inverse equation in the generic context, $$E^{\prime }({\mathrm{\Lambda }}^{\prime }(b))\equiv b:B.$$ Substituting $a$ for $x$ in this equality gives $$E^{\prime }({\mathrm{\Lambda }}^{\prime }(b))[a/x]\equiv b[a/x]:B[a/x].$$ The left side is ${\mathrm{\Lambda }}^{\prime }(b)a$ by definition, so this is the beta rule. Commutation of the operations with substitution ensures that this expression is independent of the chosen derivation representatives and fresh displays.

For eta, the second inverse equation says $${\mathrm{\Lambda }}^{\prime }(E^{\prime }(f))\equiv f:P.$$ After symmetry, $$f\equiv {\mathrm{\Lambda }}^{\prime }(E^{\prime }(f)):P,$$ which is eta, since $E^{\prime }(f)$ is the generic application $fx$.

Equality preservation by ${\mathrm{\Lambda }}^{\prime }$ gives introduction congruence directly: $$b\equiv b^{\prime }:B⟹{\mathrm{\Lambda }}^{\prime }(b)\equiv {\mathrm{\Lambda }}^{\prime }(b^{\prime }):P.$$ For elimination congruence, suppose $f\equiv f^{\prime }:P$ and $a\equiv a^{\prime }:A$. Equality preservation by $E^{\prime }$ gives, in $\mathrm{\Gamma },x:A$, $$E^{\prime }(f)\equiv E^{\prime }(f^{\prime }):B.$$ Ordinary substitution with $a$ yields $$E^{\prime }(f)[a/x]\equiv E^{\prime }(f^{\prime })[a/x]:B[a/x].$$ Independently, Subst-Eq-Tm applied to $a\equiv a^{\prime }:A$ and the term $E^{\prime }(f^{\prime })$ gives $$E^{\prime }(f^{\prime })[a/x]\equiv E^{\prime }(f^{\prime })[a^{\prime }/x]:B[a/x].$$ Transitivity produces $$fa\equiv f^{\prime }{a}^{\prime }:B[a/x],$$ with the natural type $B[a^{\prime }/x]$ of the right side converted to the common fiber by equal substitution. These are exactly the fixed-family $\lambda$-eq and app-eq rules. Hence the internal bijection data reconstruct formation, introduction, elimination, beta, eta, and congruence.

Let $y:C_0$ be any declaration of $\mathrm{\Gamma }$, let ${\mathrm{\Gamma }}_0⊢c:C_0$, and choose the local binders $x,p,q,r$ outside $\{y\}\cup \mathrm{FV}(c)$. Write $L$ and $R$ for the left and right associated sum types in example 27.26. The fully annotated first map has the form $$\mathrm{\Theta }=\lambda (q:L).({\mathsf{pr}}_1({\mathsf{pr}}_1(q)),({\mathsf{pr}}_2({\mathsf{pr}}_1(q)),{\mathsf{pr}}_2(q))).$$ Applying the operator clauses of definition 26.10 from the outside in gives No occurrence of $q$ is substituted, and no occurrence of $c$ is captured, by the chosen freshness. Consequently, for every argument, $$(\mathrm{\Theta }s)[c/y]=\mathrm{\Theta }[c/y]s[c/y]={\mathrm{\Theta }}_{A[c/y],B[c/y],C[c/y]}s[c/y].$$

The same literal recursion for $$\mathrm{\Xi }=\lambda (r:R).(({\mathsf{pr}}_1(r),{\mathsf{pr}}_1({\mathsf{pr}}_2(r))),{\mathsf{pr}}_2({\mathsf{pr}}_2(r)))$$ gives $$\mathrm{\Xi }[c/y]={\mathrm{\Xi }}_{A[c/y],B[c/y],C[c/y]},(\mathrm{\Xi }t)[c/y]=\mathrm{\Xi }[c/y]t[c/y].$$ Substitution in the dependent annotations and result fibers is governed by the same binder clause; the identity $(D[a/x])[c/y]=D[c/y][a[c/y]/x]$ follows from the freshness assumptions. Thus both comparison maps commute with substitution in an arbitrary variable of $\mathrm{\Gamma }$, and hence in every such variable.

For the sum unit law, define For $a:A$, beta for the first projection gives $$F(Ga)\equiv {\mathsf{pr}}_1((a,\star ))\equiv a.$$ For $p:\sum _{x:A}\mathbf{1}$, unit eta gives ${\mathsf{pr}}_2(p)\equiv \star :\mathbf{1}$; pair congruence and sum eta give $$p\equiv ({\mathsf{pr}}_1(p),{\mathsf{pr}}_2(p))\equiv ({\mathsf{pr}}_1(p),\star )=G(Fp).$$ After symmetry this is the required round trip $G(Fp)\equiv p$. This isomorphism uses exactly $\mathrm{\Sigma }$-eta and $\mathbf{1}$-eta.

For the product unit law, set $B_{\star }:=B[\star /x]$ and define $$H:=\lambda (f:\prod _{x:\mathbf{1}}B).f\star :(\prod _{x:\mathbf{1}}B)\to B_{\star }.$$ For $b:B_{\star }$, weaken $b$ to $\mathrm{\Gamma },x:\mathbf{1}$. Unit eta gives $x\equiv \star :\mathbf{1}$, so equal substitution in $B$, followed by symmetry, gives $$B_{\star }\equiv B\mathsf{type}\text{in }\mathrm{\Gamma },x:\mathbf{1}.$$ Convert the unchanged raw term $b$ along this equality; call the resulting term ${\overline{b}}_x:B$. Define $$K:=\lambda (b:B_{\star }).\lambda (x:\mathbf{1}).{\overline{b}}_x:B_{\star }\to \prod _{x:\mathbf{1}}B.$$ Because conversion changes typing derivations, not raw terms, beta at $\star$ gives $$H(Kb)\equiv {\overline{b}}_{\star }=b:B_{\star }.$$

For $f:\prod _{x:\mathbf{1}}B$, unit eta in the generic context gives $x\equiv \star$. Application congruence therefore identifies $fx$ with the converted term $f\star :B$. Abstraction congruence and product eta give $$K(Hf)\equiv \lambda (x:\mathbf{1}).fx\equiv f.$$ Thus the second isomorphism uses $\mathbf{1}$-eta to compare the arguments and $\mathrm{\Pi }$-eta to remove the rebuilt abstraction. The two laws use no other eta principles.

Take $B$ independent of $x$ and $C$ independent of the pair variable $p$ in example 27.25. Then the two types reduce to $$(A\times B)\to C\text{and}A\to (B\to C).$$ The comparison maps specialize literally to which are exactly the classical simply typed combinators displayed in the exercise. No dependent conversion remains because every substituted codomain is constant.

For $f:(A\times B)\to C$, beta reduction gives The middle step uses symmetry of product eta under application, and the last uses function eta. For $g:A\to (B\to C)$, The second step uses the two projection beta rules; the last uses function eta first at $B\to C$ and then at $A\to (B\to C)$. Hence the specialization is a definitional isomorphism, not merely a set-theoretic bijection.