ch:coercive-subtyping: coherent casts

The first derivation synthesizes $x:A$, inserts $a:A\to B$, and then inserts $c:B\to D$, producing $c(a(x))$. The second inserts $b:A\to C$ and then $d:C\to D$, producing $d(b(x))$. Coherence requires the target-theory function equality $$\mathrm{\Gamma }⊢\lambda x.c(a(x))\equiv \lambda x.d(b(x)):A\to D.$$ An equality after substituting one selected $x:A$ does not compare the cast programs at all inputs and therefore does not satisfy path coherence.

The permitted derivation synthesizes $(x,y):A\times B$ by Coe-Pair and checks it at $\mathbf{2}$ by one Coe-Insert along $\sigma$, yielding $\mathsf{tt}$. The attempted second derivation tries to check $x:A$ at $A^{\prime }$ inside Coe-Pair; that premise cannot use Coe-Insert, because Coe-Pair demands synthesis for both components. The programmer can write the annotation $(x:A^{\prime })$, which lets Coe-Ann synthesize $A^{\prime }$ after checking $x$ along $\iota$. The pair then synthesizes $A^{\prime }\times B$, and final insertion along $\tau$ yields $\mathsf{ff}$.

The domain path is contravariant: $p\in \mathsf{Coe}(A_2,A_1)$. For each $x:A_2$, the codomain path is $$q_x\in \mathsf{Coe}(B_1({\mathsf{prog}}_{p}x),B_2(x)).$$ Given $f:\mathrm{\Pi }y:A_1.B_1(y)$, first ${\mathsf{prog}}_{p}x:A_1$, then $f({\mathsf{prog}}_{p}x):B_1({\mathsf{prog}}_{p}x)$, and finally ${\mathsf{prog}}_{q_x}(f({\mathsf{prog}}_{p}x)):B_2(x)$. Abstraction over $x$ and $f$ gives the cast from $\mathrm{\Pi }y:A_1.B_1(y)$ to $\mathrm{\Pi }x:A_2.B_2(x)$. Reversing $p$ would make the first application ill typed at $x:A_2$.

For $r:{\mathsf{Rec}}_1$, the first field is ${\mathsf{prog}}_p(r.n):\mathbb{N}$. The second is $${\mathsf{prog}}_{q_{r.n}}(r.v):\mathsf{Vec}{A}^{\prime }({\mathsf{prog}}_p(r.n)),$$ because $r.v:\mathsf{Vec}A(r.n)$ and $q_{r.n}$ has the corresponding dependent source and target. Thus the full cast is $({\mathsf{prog}}_p(r.n),{\mathsf{prog}}_{q_{r.n}}(r.v)):{\mathsf{Rec}}_2$. For $p=\mathsf{id}$, choosing $q_n=\mathsf{map}\alpha$ gives the well-typed second field $\mathsf{map}\alpha (r.v):\mathsf{Vec}{A}^{\prime }(r.n)$. If ${\mathsf{prog}}_p=\mathsf{suc}$, the required type is instead $\mathsf{Vec}{A}^{\prime }(\mathsf{suc}(r.n))$; reusing $\mathsf{map}\alpha (r.v):\mathsf{Vec}{A}^{\prime }(r.n)$ is ill typed.

Write the dependent application premises before completion as $$\mathrm{\Gamma }⊢f:(x:K_1)K_2,\mathrm{\Gamma }⊢t:K_1.$$ Completing their derivations separately may instead produce $${\mathrm{\Gamma }}^{\prime }⊢f^{\prime }:(x:K_1^{\prime })K_2^{\prime },{\mathrm{\Gamma }}^{″}⊢t^{\prime }:K_1^{″}.$$ The application rule can be rebuilt only after proving ${\mathrm{\Gamma }}^{\prime }={}_T{\mathrm{\Gamma }}^{″}$ and $K_1^{\prime }={}_T{K}_1^{″}$. Basic-edge coherence does not itself establish either equality. Lemma 5.3 shows that the operations used while completing derivations preserve equality of the relevant presupposed judgments, and Corollary 3.6 supplies coherence in $T[R{]}_{0K}$. Lemma 5.7 then proves derivation independence where both completion images are defined, and Theorem 5.8 proves totality.

Section 4 leaves open a simple general condition on arbitrary rule forms of $T$ and arbitrary basic-rule systems $R$ that guarantees this argument that matches these presuppositions. The proved result covers the displayed logical-framework systems, the stated coherent rule sets, and the cited inductive schemata.