ch:cdle-cedille: CDLE and Cedille

Erasing implicit abstractions and applications gives $$\mathrm{erase}(\mathsf{sucI}(n))=\lambda z.\lambda s.s(\mathrm{erase}(n)zs).$$ Also $$\mathrm{erase}(\mathsf{sucC}(n.1))=\lambda z.\lambda s.s(\mathrm{erase}(n.1)zs){=}_{\beta \eta }\lambda z.\lambda s.s(\mathrm{erase}(n)zs).$$ Thus CDLE-Isect-I applies. Two successors erase to $\lambda z.\lambda s.s(sz)$ after beta reduction; every intersection and projection annotation disappears.

Let the function view be $h:=\lambda x.d.1(c.1x):A\to C$. The equality view follows from the two cast equality proofs and transitivity of erased beta-eta equality. Pair them as $[h,p]:\mathsf{Cast}(A,C)$. The erasure calculation is $$\mathrm{erase}(h)=\lambda x.(\lambda y.y)((\lambda z.z)x)⟶\lambda x.(\lambda y.y)x⟶\lambda x.x.$$ Hence composition remains an identity-erasing cast.

The forgetful cast has function view $i:\mathsf{Vec}(A,n)\to \mathsf{List}(A)$ with $\mathrm{erase}(i)=\lambda x.x$. A copying conversion $k$ has the same function type but erases to a case recursor. On a two-element vector, $i$ erases to the original constructor tree, while $k$ performs two case steps and allocates two list constructors. Thus $\mathrm{erase}(k){\ne }_{\beta \eta }\lambda x.x$ as open functions. The equality view required by $\mathsf{Cast}$ is the failed premise; agreement on this one closed input would not repair it.

$\mathsf{zeroC}$ and $\mathsf{zeroI}$ both erase to $\lambda z.\lambda s.z$, so their intersection introduces $\mathsf{zero}$. For $n:\mathsf{Nat}$, the two successor components have the common erasure $$\mathrm{erase}(\mathsf{sucC}(n.1))=\mathrm{erase}(\mathsf{sucI}(n))=\lambda z.\lambda s.s(\mathrm{erase}(n)zs).$$ Their intersection therefore introduces $\mathsf{suc}(n)$. Instantiating $n.2$ with the Church-subject motive $P(m)\equiv m+0=m$ gives the result at $n.1$. The zero computation is erased beta reduction of the stored Church program; the occurrences identifying $m+0$ with $m$ in its classifier are internal equality rewrites and do not add runtime steps.

For intersection introduction, the common erased class lies in the first candidate and, by the second premise, in the dependent fiber; hence it lies in their intersection. For equality introduction, beta-eta equality of the two endpoints makes the equality interpretation the greatest candidate, which contains the arbitrary erasure of $\beta \{u\}$. If $t:\mathrm{\forall }X:\star .X$ were closed, soundness instantiated at the empty candidate would require $\mathrm{erase}(t)\in \varnothing$, a contradiction.

For $\mathsf{Top}=\{\lambda x.x\simeq \lambda x.x\}$, the rule types $\beta \{\mathrm{\Omega }\}:\mathsf{Top}$ because the endpoints agree, regardless of the erased witness. Its interpretation is the greatest candidate, not the empty candidate chosen for $X$ above, so this nonnormalizing inhabitant does not affect the consistency argument.