ch:inductive-types: ch:inductive-types

Unfolding $\mathrm{\neg }A:=A\to \mathbf{0}$, the term is $$\lambda h.\lambda a.h(\lambda k.k(a)).$$ Indeed, under $h:\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A$ and $a:A$, the abstraction $\lambda k.k(a)$ has type $\mathrm{\neg }\mathrm{\neg }A$; applying $h$ produces an element of $\mathbf{0}$, as required for a term of $\mathrm{\neg }A$.

Using the argument order for ${\mathsf{rec}}_{\mathbb{N}}$ fixed in definition 28.22, put $$\mathsf{pred}:=\lambda n.{\mathsf{rec}}_{\mathbb{N}}(\mathsf{0},\lambda k.\lambda r.k,n):\mathbb{N}\to \mathbb{N}.$$ The two recursor equations give $\mathsf{pred}(\mathsf{0})\equiv \mathsf{0}$ and $\mathsf{pred}(\mathsf{suc}(k))\equiv k$. Truncated subtraction can now recurse on its second argument: $$\dot{-}:=\lambda m.\lambda n.{\mathsf{rec}}_{\mathbb{N}}(m,\lambda k.\lambda r.\mathsf{pred}(r),n):\mathbb{N}\to \mathbb{N}\to \mathbb{N}.$$ Consequently $m\dot{-}\mathsf{0}\equiv m$ and $m\dot{-}\mathsf{suc}(n)\equiv \mathsf{pred}(m\dot{-}n)$, which is the usual truncated subtraction.

For a closed type $C$, weaken it to the constant family $w:W⊢C$. The W-elimination step therefore has type $$h:\prod _{a:A}\prod _{f:B(a)\to W}(B(a)\to C)\to C.$$ Define ${\mathsf{rec}}_W(h,t):={\mathsf{ind}}_{\mathsf{W}}(w.C;h,t)$. Rule W-comp calculates $${\mathsf{rec}}_W(h,\mathsf{sup}(a,f))\equiv h(a,f,\lambda y.{\mathsf{rec}}_W(h,f(y))):C.$$ The constant specialization erases the tree argument from the motive. It therefore cannot synthesize a result in a genuinely varying fiber $C(t)$; that dependency must already be supplied to W-elimination.

Use constructors $\mathsf{leaf}:A\to \mathsf{Tree}(A)$ and $\mathsf{node}:\mathsf{Tree}(A{)}^2\to \mathsf{Tree}(A)$. The eliminator gives Induct on the tree. The leaf case computes to reflexivity. In the node case, the two induction hypotheses reduce the double mirror to $\mathsf{node}(l,r)$; this is precisely the constructor congruence case of the eliminator.

Let $\omega :=\delta (\mathsf{roll}(\delta ))$. Unfolding $\delta$ and then using the proposed pattern equation gives the nonempty cycle In the constructor argument $D\to D$, the occurrence of $D$ in the domain is negative. Admitting the constructor together with the displayed destructor equation therefore destroys strong normalization, which strict positivity is designed to protect.

Recall that $\mathrm{\neg }X:=X\to \mathbf{0}$. The required terms are $$\lambda f.\lambda b.\lambda a.f(a)(b):(A\to \mathrm{\neg }B)\to (B\to \mathrm{\neg }A)$$ and $$\lambda a.\lambda k.k(a):A\to \mathrm{\neg }\mathrm{\neg }A.$$ For the first, in context $f:A\to (B\to \mathbf{0}),b:B,a:A$, application gives $f(a):B\to \mathbf{0}$, hence $f(a)(b):\mathbf{0}$; three uses of $\mathrm{\Pi }$-intro give the displayed type. For the second, in context $a:A,k:A\to \mathbf{0}$, application gives $k(a):\mathbf{0}$, and two abstractions finish the derivation. Neither construction eliminates a term of $\mathbf{0}$; each merely constructs a function whose codomain is $\mathbf{0}$.

Let $\mathrm{\Gamma }⊢D\mathsf{type}$. Restore the constant motive on empty elimination and define $$\lambda c.{\mathsf{ind}}_{\mathbf{0}}(x.D;h(c)):C\to D.$$ Indeed, in $\mathrm{\Gamma },c:C$ we have $h:C\to \mathbf{0}$ by weakening, so $h(c):\mathbf{0}$. Weakening $D$ once more gives $\mathrm{\Gamma },c:C,x:\mathbf{0}⊢D\mathsf{type}$. Therefore $\mathbf{0}$-elim yields $$\mathrm{\Gamma },c:C⊢{\mathsf{ind}}_{\mathbf{0}}(x.D;h(c)):D,$$ and $\mathrm{\Pi }$-intro gives the claimed map. Thus a map from $C$ into $\mathbf{0}$ permits a map from $C$ into every type.

For $\mathrm{\Gamma }⊢C\mathsf{type}$, the fully annotated definition is $${\mathsf{abort}}_C:=\lambda a:\mathbf{0}.{\mathsf{ind}}_{\mathbf{0}}(x.C;a):\mathbf{0}\to C.$$ Here the variable $x$ is bound in the motive annotation; $C$ does not actually depend on it. The body is the following instance of $\mathbf{0}$-elim. We display the structural premises that the book’s compressed convention ordinarily suppresses: $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}\mathrm{\Gamma }⊢C\mathsf{type}\\ \mathrm{\Gamma },a:\mathbf{0}\mathsf{ctx}\end{array}}{\mathrm{\Gamma },a:\mathbf{0}⊢C\mathsf{type}}}\mathrm{Wk}\\ \mathrm{\Gamma },a:\mathbf{0},x:\mathbf{0}\mathsf{ctx}\end{array}}{\mathrm{\Gamma },a:\mathbf{0},x:\mathbf{0}⊢C\mathsf{type}}}\mathrm{Wk}\\ {\displaystyle \frac{\mathrm{\Gamma },a:\mathbf{0}\mathsf{ctx}}{\mathrm{\Gamma },a:\mathbf{0}⊢a:\mathbf{0}}}\mathrm{Var}\end{array}}{\mathrm{\Gamma },a:\mathbf{0}⊢{\mathsf{ind}}_{\mathbf{0}}(x.C;a):C}}-\mathrm{elim}}{\mathrm{\Gamma }⊢\lambda a:\mathbf{0}.{\mathsf{ind}}_{\mathbf{0}}(x.C;a):\mathbf{0}\to C}\mathrm{\Pi }-\mathrm{intro}.$$ The two context judgments in this tree follow from $\mathrm{\Gamma }\mathsf{ctx}$, $\mathbf{0}$-form, and context extension. More explicitly, $$\frac{\begin{array}{c}\mathrm{\Gamma }\mathsf{ctx}\\ {\displaystyle \frac{\mathrm{\Gamma }\mathsf{ctx}}{\mathrm{\Gamma }⊢\mathbf{0}\mathsf{type}}}-\mathrm{form}\end{array}}{\mathrm{\Gamma },a:\mathbf{0}\mathsf{ctx}}\mathrm{Ctx}-\mathrm{Ext},$$ and the second extension is identical after weakening $\mathbf{0}$ to $\mathrm{\Gamma },a:\mathbf{0}$. Since $C[a/x]$ is literally $C$, the conclusion of empty elimination has exactly the required type.

Orienting case analysis by the first argument, define In each body both branches have type $\mathbf{2}$, so Boolean recursion and two uses of $\mathrm{\Pi }$-intro give type $\mathbf{2}\to \mathbf{2}\to \mathbf{2}$. Two function-beta steps followed by the appropriate Boolean computation rule give These are judgmental equations; no propositional equality type is involved.

Write $$T_t:=C(\mathsf{tt}),T_f:=C(\mathsf{ff}),P:=\prod _{b:\mathbf{2}}C(b).$$ Substitution into $\mathrm{\Gamma },x:\mathbf{2}⊢C\mathsf{type}$ forms $T_t$ and $T_f$ in $\mathrm{\Gamma }$. Starting from the context $$\mathrm{\Delta }:=\mathrm{\Gamma },c_t:T_t,c_f:T_f,b:\mathbf{2},$$ repeated weakening supplies $$\mathrm{\Delta },x:\mathbf{2}⊢C\mathsf{type},\mathrm{\Delta }⊢c_t:C(\mathsf{tt}),\mathrm{\Delta }⊢c_f:C(\mathsf{ff}),$$ while Var supplies $\mathrm{\Delta }⊢b:\mathbf{2}$. Thus $$\frac{\begin{array}{c}\mathrm{\Delta },x:\mathbf{2}⊢C\mathsf{type}\\ \mathrm{\Delta }⊢c_t:C(\mathsf{tt})\\ \mathrm{\Delta }⊢c_f:C(\mathsf{ff})\\ \mathrm{\Delta }⊢b:\mathbf{2}\end{array}}{\mathrm{\Delta }⊢{\mathsf{ind}}_{\mathbf{2}}(x.C;c_t,c_f,b):C(b)}-\mathrm{elim}.$$ The weakening sequence can be read explicitly as followed by weakening the resulting family by $b:\mathbf{2}$; exchange merely moves the fresh motive variable $x$ to the final displayed position. The branch terms are obtained by Var and weakened over declarations to their right.

Applying $\mathrm{\Pi }$-intro successively to $b,c_f,c_t$ yields $$\mathrm{\Gamma }⊢\lambda c_t.\lambda c_f.\lambda b.{\mathsf{ind}}_{\mathbf{2}}(x.C;c_t,c_f,b):T_t\to T_f\to P.$$ Call this term $I_C$. At the constructors, three Pi-beta steps expose the eliminator and then Boolean computation applies:

Conversely, suppose for every such family $C$ we are given $$J_C:T_t\to T_f\to \prod _{b:\mathbf{2}}C(b)$$ with the two displayed constructor equations. Define the eliminator constructed from this principle by $${\mathsf{ind}}_{\mathbf{2}}^{\prime }(x.C;c_t,c_f,b):=J_C(c_t)(c_f)(b).$$ Three uses of $\mathrm{\Pi }$-elim give it type $C(b)$. Its constructor computations are exactly the assumed equations $$J_C(c_t)(c_f)(\mathsf{tt})\equiv c_t,J_C(c_t)(c_f)(\mathsf{ff})\equiv c_f.$$ Hence the binder-form principle and the primitive elimination principle construct one another. This proves equivalence of principles, not a raw-term identity between $J_C$ and the primitive eliminator.

Let $${\mathbf{2}}^{\prime }:=\mathbf{1}+\mathbf{1},{\mathsf{tt}}^{\prime }:=\mathsf{inl}(\star ),{\mathsf{ff}}^{\prime }:=\mathsf{inr}(\star ).$$ Formation and the two introduction rules are immediate from $\mathbf{1}$-form, $\mathbf{1}$-intro, and the coproduct rules.

For elimination, suppose $$\mathrm{\Gamma },z:{\mathbf{2}}^{\prime }⊢C\mathsf{type},c_t:C({\mathsf{tt}}^{\prime }),c_f:C({\mathsf{ff}}^{\prime }),s:{\mathbf{2}}^{\prime }.$$ In the left branch, the family over $u:\mathbf{1}$ is $C(\mathsf{inl}(u))$. The derived dependent unit eliminator therefore gives $$f:=\lambda u.{\mathsf{ind}}_{\mathbf{1}}(v.C(\mathsf{inl}(v));c_t;u):\prod _{u:\mathbf{1}}C(\mathsf{inl}(u)).$$ Here the semicolon grouping only makes the motive, base point, and scrutinee visible; by proposition 27.17 the body is the unchanged raw term $c_t$, converted from $C(\mathsf{inl}(\star ))$ to $C(\mathsf{inl}(u))$. In the right branch, unit elimination converts the unchanged term $c_f$ from $C(\mathsf{inr}(\star ))$ to $C(\mathsf{inr}(u))$, giving $$g:=\lambda u.{\mathsf{ind}}_{\mathbf{1}}(v.C(\mathsf{inr}(v));c_f;u):\prod _{u:\mathbf{1}}C(\mathsf{inr}(u)).$$ Define $${\mathsf{ind}}_{{\mathbf{2}}^{\prime }}(z.C;c_t,c_f;s):={\mathsf{ind}}_{+}(z.C;f,g,s):C(s).$$ This has exactly the Boolean elimination rule, with ${\mathbf{2}}^{\prime }$, ${\mathsf{tt}}^{\prime }$, and ${\mathsf{ff}}^{\prime }$ substituted for their primitive counterparts. Its computations are judgmental: The middle equations are coproduct computation; the final equations are function beta followed by the reflexive computation of the derived unit eliminator. Thus no propositional transport remains in either Boolean computation rule.

Using the case-analysis notation of definition 28.18, define Successive coproduct and function beta rules give the three checks: Thus $\beta \circ \alpha$ computes to the identity on each constructor form listed in the exercise. The claim is deliberately constructorwise: no coproduct eta rule is required for a generic variable.

Parenthesize the source type as $((A+B)\to C)$. Define For a pair of functions, beta and the two projection rules give $$F(G((f,g)))\equiv (\lambda a.f(a),\lambda b.g(b))\equiv (f,g),$$ where the last equality uses $\mathrm{\Pi }$-eta in each component. For a generic $h:(A+B)\to C$, constructor computation gives The first equation uses function eta but not coproduct eta; the latter two hold directly on the two constructors.

Recur on the second argument and use the multiplication of construction 73.26: $$\mathsf{exp}:=\lambda m.\lambda n.{\mathsf{rec}}_{\mathbb{N}}(\bar{1},\lambda k.\lambda r.\mathsf{mul}(r,m),n).$$ The recursive result $r$ has type $\mathbb{N}$, and the predecessor $k$ is unused. Hence the term has type $\mathbb{N}\to \mathbb{N}\to \mathbb{N}$. Its defining equations are immediate: The equations use only Pi-beta and the two natural-number recursor computations.

At the constant motive $C$, define $$\mathsf{iter}(c_0,f,n):={\mathsf{rec}}_{\mathbb{N}}(c_0,\lambda k.\lambda r.f(r),n):C.$$ The step has type $\mathbb{N}\to C\to C$; it ignores the predecessor. Therefore Addition can now be defined without mentioning ${\mathsf{rec}}_{\mathbb{N}}$: $$\mathsf{add}:=\lambda m.\lambda n.\mathsf{iter}(m,\lambda r.\mathsf{suc}(r),n).$$ Its equations are $\mathsf{add}(m,\mathsf{0})\equiv m$ and $\mathsf{add}(m,\mathsf{suc}(n))\equiv \mathsf{suc}(\mathsf{add}(m,n))$, exactly as in construction 28.23.

Put $$T_0:=C(\mathsf{0}),S:=\prod _{k:\mathbb{N}}C(k)\to C(\mathsf{suc}(k)).$$ Substitution forms $T_0$ and $S$ in $\mathrm{\Gamma }$. In the context $$\mathrm{\Delta }:=\mathrm{\Gamma },c_0:T_0,c_s:S,n:\mathbb{N}$$ we need the four premises of $\mathbb{N}$-elim. They are obtained as follows. First weaken the original family past the two branch declarations: and then weaken it by the scrutinee declaration $n:\mathbb{N}$. Up to exchange of the fresh motive variable, this is $\mathrm{\Delta },x:\mathbb{N}⊢C\mathsf{type}$. The variable rule and weakening give $$\mathrm{\Delta }⊢c_0:C(\mathsf{0}),\mathrm{\Delta }⊢c_s:S,\mathrm{\Delta }⊢n:\mathbb{N}.$$ If the rule is read with an explicit step lambda, two applications followed by two abstractions derive $$\mathrm{\Delta }⊢\lambda k.\lambda r.c_s(k)(r):S;$$ by Pi-eta this is judgmentally equal to the weakened $c_s$. Hence $\mathbb{N}$-elim gives $$\mathrm{\Delta }⊢{\mathsf{ind}}_{\mathbb{N}}(x.C;c_0,\lambda k.\lambda r.c_s(k)(r);n):C(n).$$ Abstracting in the reverse order $n,c_s,c_0$ produces

At zero, three Pi-beta steps and $\mathbb{N}$-comp${}_1$ give $${\mathsf{ind}}_C(c_0,c_s,\mathsf{0})\equiv {\mathsf{ind}}_{\mathbb{N}}(x.C;c_0,\lambda k.\lambda r.c_s(k)(r);\mathsf{0})\equiv c_0.$$ At a successor, $\mathbb{N}$-comp${}_2$ and two further beta steps give The motive is genuinely $C(n)$; replacing it by a constant family would lose the dependent conclusion.

Let $1:=\bar{1}$, and define the base function and outer step The requested function is the outer recursion at the higher type $\mathbb{N}\to \mathbb{N}$: $$\mathsf{ack}:=\lambda m.{\mathsf{rec}}_{\mathbb{N}}(a_0,S,m):\mathbb{N}\to \mathbb{N}\to \mathbb{N}.$$ Writing $A_m:=\mathsf{ack}(m)$, the outer computation equations are $$A_{\mathsf{0}}\equiv a_0,A_{\mathsf{suc}(m)}\equiv S(m,A_m).$$ Consequently $$\mathsf{ack}(\mathsf{0},n)\equiv a_0(n)\equiv \mathsf{suc}(n).$$ For the successor row, substitute the displayed form of $S$ and abbreviate $$R_m(n):={\mathsf{rec}}_{\mathbb{N}}(A_m(1),\lambda k.\lambda r.A_m(r),n).$$ Then By the definition of $A_m$, the last term is $\mathsf{ack}(m,\mathsf{ack}(\mathsf{suc}(m),n))$. The crucial point is that the outer recursive result $A_m$ is itself a function and is used both as the inner base case and as the operation iterated in the inner successor case.

First define a zero test $$\mathsf{iszero}:=\lambda n.{\mathsf{rec}}_{\mathbb{N}}(\mathsf{tt},\lambda k.\lambda r.\mathsf{ff},n):\mathbb{N}\to \mathbf{2}.$$ It computes to $\mathsf{tt}$ at zero and to $\mathsf{ff}$ at every successor. Now let the outer recursion return a function $\mathbb{N}\to \mathbf{2}$: Here $e:\mathbb{N}\to \mathbf{2}$ is the predecessor result: when the first argument is $\mathsf{suc}(k)$ and the second is $\mathsf{suc}(j)$, the step returns $e(j)$, thereby comparing the two predecessors. Direct computation gives the four characteristic equations An induction on $m$, with a case split on $n$, now proves that closed numerals compute to $\mathsf{tt}$ exactly when their meta-level indices agree: the mixed zero/successor cases are false, and the successor/successor case reduces to the induction hypothesis for the predecessors. In particular, $$\mathsf{eq}(\bar{2},\bar{2})\equiv \mathsf{eq}(\bar{1},\bar{1})\equiv \mathsf{eq}(\mathsf{0},\mathsf{0})\equiv \mathsf{tt}.$$

The term is $$\lambda h.h(\mathsf{inr}(\lambda a.h(\mathsf{inl}(a)))):\mathrm{\neg }\mathrm{\neg }(A+\mathrm{\neg }A).$$ Indeed, assume $h:(A+\mathrm{\neg }A)\to \mathbf{0}$. In context $a:A$, $h(\mathsf{inl}(a)):\mathbf{0}$, so $k:=\lambda a.h(\mathsf{inl}(a)):\mathrm{\neg }A$. Hence $\mathsf{inr}(k):A+\mathrm{\neg }A$, and applying $h$ gives a term of $\mathbf{0}$. Abstracting over $h$ proves $((A+\mathrm{\neg }A)\to \mathbf{0})\to \mathbf{0}$, which is the stated double negation.

For the first direction define $$\lambda h.(\lambda a.h(\mathsf{inl}(a)),\lambda b.h(\mathsf{inr}(b))):\mathrm{\neg }(A+B)\to \mathrm{\neg }A\times \mathrm{\neg }B.$$ If $h:(A+B)\to \mathbf{0}$, its restrictions along the two injections have respectively types $A\to \mathbf{0}$ and $B\to \mathbf{0}$, so the pair has the required product type.

For the converse, define $$\lambda p.[{\mathsf{pr}}_1(p),{\mathsf{pr}}_2(p)]:\mathrm{\neg }A\times \mathrm{\neg }B\to \mathrm{\neg }(A+B).$$ For $p:\mathrm{\neg }A\times \mathrm{\neg }B$, both projections have codomain $\mathbf{0}$, so coproduct case analysis yields $[{\mathsf{pr}}_1(p),{\mathsf{pr}}_2(p)]:A+B\to \mathbf{0}$. Its constructor computations are

Use clause (ii) of theorem 28.32 at the constant result type $C:=\mathbb{N}$, with $$c_n:=\mathsf{0},c_c:=\lambda a.\lambda \ell .\lambda r.\mathsf{suc}(r):A\to L\to \mathbb{N}\to \mathbb{N}.$$ Let ${\mathsf{rec}}_L^{c_n,c_c}:L\to \mathbb{N}$ denote the recursor supplied by that clause, and define $$\mathsf{length}:={\mathsf{rec}}_L^{c_n,c_c}.$$ Its two stipulated W-recursion computations are The element $a$ and tail $\ell$ are available to the step, although only the recursive result is needed for length.

In the node case, clause (iii) supplies the step with the four arguments, in order, $$\ell :T,r:T,u:\mathbb{N}(=\mathsf{leaves}(\ell )),v:\mathbb{N}(=\mathsf{leaves}(r)).$$ At result type $\mathbb{N}$, choose $$c_l:=\bar{1},c_n:=\lambda \ell .\lambda r.\lambda u.\lambda v.u+v:T\to T\to \mathbb{N}\to \mathbb{N}\to \mathbb{N}.$$ Let ${\mathsf{rec}}_T^{c_l,c_n}$ be the recursor furnished by the theorem and put $\mathsf{leaves}:={\mathsf{rec}}_T^{c_l,c_n}$. Then

Write $W:={\mathsf{W}}_{x:A}B$. At the constant motive $\mathbf{0}$, the W-step must have type $$\prod _{a:A}\prod _{\alpha :B(a)\to W}(B(a)\to \mathbf{0})\to \mathbf{0}.$$ Using the assumed point $k(a):B(a)$, define $$h:=\lambda a.\lambda \alpha .\lambda q.q(k(a)).$$ The subtree family $\alpha$ is not needed; the inductive-hypothesis family $q:B(a)\to \mathbf{0}$ is evaluated at the distinguished arity point $k(a)$. Therefore W-elimination gives $$\lambda t.{\mathsf{ind}}_{\mathsf{W}}(w.\mathbf{0};h,t):W\to \mathbf{0},$$ which is a term of $\mathrm{\neg }W$. Conceptually, every purported tree has at least one immediate child, and following the selected child cannot terminate in a well-founded tree.

Fix $\mathrm{\Gamma }⊢A\mathsf{type}$ and abbreviate $L:=\mathsf{List}(A)$. The formation and introduction rules generated by definition 28.34 are

For a motive $\mathrm{\Gamma },w:L⊢C\mathsf{type}$, the nil case has no arguments, while the cons case receives, in the required order, the element, the recursive argument, and its inductive hypothesis: $$c_n:C(\mathsf{nil}),c_c:\prod _{a:A}\prod _{\ell :L}C(\ell )\to C(\mathsf{cons}(a,\ell )).$$ For the next three displays, abbreviate $$I(t):={\mathsf{ind}}_{\mathsf{List}}(w.C;c_n,c_c;t).$$ The elimination rule is therefore

Finally, the two generated computation rules are

The successor computation is the second rule:

The direct recursive argument has empty arity telescope, so its generated inductive-hypothesis family is simply the single term $C(\ell )$.

Use the constant motive $w.\mathbb{N}$, the nil branch $\mathsf{0}$, and the cons branch that ignores the element and tail but increments the recursive result: $$\mathsf{length}:=\lambda t.{\mathsf{ind}}_{\mathsf{List}}(w.\mathbb{N};\mathsf{0},\lambda a.\lambda \ell .\lambda r.\mathsf{suc}(r);t):\mathsf{List}(A)\to \mathbb{N}.$$ Function beta followed by the two list computations gives Both are judgmental equations generated by the primitive list rules.

Work in the hypothetical extension with $$\mathsf{fold}:(D\to \mathbf{0})\to D$$ and, for every $C$, a recursor $${\mathsf{rec}}_D(e):D\to C,{\mathsf{rec}}_D(e,\mathsf{fold}(u))\equiv e(u),e:(D\to \mathbf{0})\to C.$$ At $C:=D\to \mathbf{0}$, the identity step $$e:=\lambda u:D\to \mathbf{0}.u:(D\to \mathbf{0})\to (D\to \mathbf{0})$$ therefore defines $$\mathsf{unfold}:={\mathsf{rec}}_D(e):D\to (D\to \mathbf{0}),\mathsf{unfold}(\mathsf{fold}(u))\equiv u.$$ The typing of $\delta$ is the derivation $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}d:D⊢\mathsf{unfold}:D\to (D\to \mathbf{0})\\ d:D⊢d:D\end{array}}{d:D⊢\mathsf{unfold}(d):D\to \mathbf{0}}}\mathrm{\Pi }-\mathrm{elim}\\ d:D⊢d:D\end{array}}{d:D⊢\mathsf{unfold}(d)(d):\mathbf{0}}}\mathrm{\Pi }-\mathrm{elim}}{\cdot ⊢\delta :=\lambda d.\mathsf{unfold}(d)(d):D\to \mathbf{0}}\mathrm{\Pi }-\mathrm{intro}.$$ Weakening supplies the closed constant $\mathsf{unfold}$ in context $d:D$, and both occurrences of $d$ are variable-rule instances. Next, the constructor typing rule for $\mathsf{fold}$ and application give $$\frac{\begin{array}{c}\cdot ⊢\delta :D\to \mathbf{0}\\ {\displaystyle \frac{\cdot ⊢\delta :D\to \mathbf{0}}{\cdot ⊢\mathsf{fold}(\delta ):D}}\mathrm{fold}\end{array}}{\cdot ⊢\omega :=\delta (\mathsf{fold}(\delta )):\mathbf{0}}\mathrm{\Pi }-\mathrm{elim}.$$

Put $d_0:=\mathsf{fold}(\delta )$. Contextual closure of Pi-beta and of the bad recursor computation gives the nonempty cycle The first step unfolds the definition of $\delta$ and contracts its outer beta-redex. In the second, $\mathsf{unfold}(d_0)={\mathsf{rec}}_D(e,\mathsf{fold}(\delta ))$ contracts to $e(\delta )=(\lambda u.u)(\delta )$ inside function position. The third contracts that identity beta-redex. Each term has type $\mathbf{0}$: in $t_1$, $\mathsf{unfold}(d_0):D\to \mathbf{0}$; in $t_2$, $(\lambda u.u)(\delta ):D\to \mathbf{0}$; and $t_3=t_0$ was typed above.

Repeating the three arrows gives an infinite reduction sequence starting at $\omega$, so $\omega$ is not strongly normalizing. Moreover, no term on the cycle is a normal form. Term $t_0=t_3$ has the outer beta-redex $\delta (d_0)$; $t_1$ contains the recursor redex $\mathsf{unfold}(\mathsf{fold}(\delta ))$; and $t_2$ contains the beta redex $(\lambda u.u)(\delta )$. Thus every node on the exhibited cycle has an outgoing one-step reduction.

Normalize the two inner operators first. A convenient choice for $K\times X$ is the container with shapes $K$ and one position at every shape. A convenient choice for $L+X$ has shapes $L+N_1$, no positions at $\mathsf{inl}(\ell )$, and one position at $\mathsf{inr}(\star )$. The product clause of lemma 73.51 therefore gives $$A=K\times (L+N_1),B(k,\mathsf{inl}(\ell ))=N_1,B(k,\mathsf{inr}(\star ))=N_1+N_1.$$ On the two forms of element, the forward isomorphism is where $q(\mathsf{inl}(\star ))=x$ and $q(\mathsf{inr}(\star ))=x^{\prime }$. The inverse reads the shape tag. It returns $((k,q(\star )),\mathsf{inl}(\ell ))$ at a left shape, and $((k,q(\mathsf{inl}(\star ))),\mathsf{inr}(q(\mathsf{inr}(\star ))))$ at a right shape. Sum and unit eta prove the two inverse equations in ${\mathcal{T}}_{\mathrm{D}}$.