ch:linear-dependent-types: linear dependent type theory

Induct on the type or parameter-term constructor. State types map to $\mathbf{1}$, which is fixed by shape; parameter types are fixed. For functions and tensors, apply the induction hypotheses to the domain and codomain. For abstraction, application, pairs, and force, rebuild the corresponding parameter constructor after applying the hypotheses to its subterms. Lift is fixed by its shape clause. Hence applying shape twice changes no constructor. This is an equation between results of a meta-operation. A state term and its shape inhabit different syntactic classes and generally different types, so no term-equality judgment between them is asserted.

The first premise uses ${\mathrm{\Gamma }}_1=(u{:}_{1}A,v{:}_{0}D)$ and the second uses ${\mathrm{\Gamma }}_2=(u{:}_{0}A,v{:}_{1}D)$. Rule LD-Pair concludes in $${\mathrm{\Gamma }}_1+{\mathrm{\Gamma }}_2=(u{:}_{1}A,v{:}_{1}D).$$ Changing the second occurrence of $u$ to index $1$ makes its sum $1+1=\omega$. Context formation permits index $\omega$ only for a parameter type. If $A$ is a state type, the summed context is therefore ill formed; the failure occurs before pair introduction can be applied.

Split the occurrence of $x{:}_{k}A$ between the premises as $k=k_1+k_2$. The induction hypotheses give $${\mathrm{\Delta }}_1+k_1{\mathrm{\Gamma }}_2⊢M[V/x]:C[\mathrm{Sh}(V)/x]$$ and $${\mathrm{\Delta }}_2+k_2{\mathrm{\Gamma }}_2⊢N[V/x]:D[\mathrm{Sh}(M[V/x])/y,\mathrm{Sh}(V)/x].$$ The second classifier is licensed by parameter substitution and $$\mathrm{Sh}(M[V/x])=\mathrm{Sh}(M)[\mathrm{Sh}(V)/x].$$ Rebuilding LD-Pair uses $$({\mathrm{\Delta }}_1+k_1{\mathrm{\Gamma }}_2)+({\mathrm{\Delta }}_2+k_2{\mathrm{\Gamma }}_2)={\mathrm{\Delta }}_1+{\mathrm{\Delta }}_2+(k_1+k_2){\mathrm{\Gamma }}_2={\mathrm{\Delta }}_1+{\mathrm{\Delta }}_2+k{\mathrm{\Gamma }}_2.$$ This is the context and classifier in substitution clause (3).

Let $F=[[\lambda x.M_0]]$ and let $v=[[V]]:[[{\mathrm{\Gamma }}_2]]\to [[B]]$. The square has upper-left $[[{\mathrm{\Gamma }}_1]]\otimes [[{\mathrm{\Gamma }}_2]]$, upper-right $[[{\mathrm{\Gamma }}_1]]\otimes [[B]]$, lower-left $({\mathrm{\Pi }}_B[[A]])\otimes [[B]]$, and lower-right $[[A]]$. The top arrow is $\mathrm{id}\otimes v$; the left arrow is $F\otimes \mathrm{id}$; the bottom arrow is the dependent counit $ϵ$; the right-hand composite is the map induced by semantic value substitution. Naturality of the counit states $$ϵ\circ (F\otimes \mathrm{id})\circ (\mathrm{id}\otimes v)=[[M_0]]\circ (\mathrm{id}\otimes v)=[[M_0[V/x]]].$$ Together with the three evaluation induction hypotheses, this gives $$[[FN]]=[[W]].$$

Type the first read at register context $r{:}_1\mathsf{Cell}$, obtaining a tensor $(b,r^{\prime })$. In its eliminator, give the bit index zero if unused and give $r^{\prime }{:}_1\mathsf{Cell}$ to the second read. Thus the original $r$ occurs once, in the scrutinee derivation, and the bound returned register occurs once, in the body derivation. Attempting two reads of $r$ instead forms $$(r{:}_1\mathsf{Cell})+(r{:}_1\mathsf{Cell})=r{:}_{\omega }\mathsf{Cell}.$$ Because $\mathsf{Cell}$ is a state type, the $\omega$ declaration is not a well-formed context. Threading succeeds because the second read consumes a freshly bound component rather than adding a second use of the original.

For parameter substitution into $(M,N)$, clause (1) substitutes the parameter in the second component’s type; clause (2) substitutes it in both component terms, after which LD-Pair rebuilds the result. For value substitution, split the value’s usage as $k_1+k_2$, use clause (3) for $M$ and $N$, and use clause (1) on the shaped value to align $B[\mathrm{Sh}(M[V/x])]$. The context and shape equations are those in the solution of exercise 98.3. Replacing $\mathrm{Sh}(V)$ by $V$ makes the dependent suffix a kinding context containing a state term, so clause (1) is inapplicable and the reconstruction stops.

Take $\mathcal{B}=\mathsf{FinSet}$. Over a parameter set $X$, let a state object be a finite family of state sets and a morphism be an $X$-indexed finite transition; tensor is product of state spaces. For the two-state cell $C=\{0,1\}$ and a family $D(c)$, the dependent function object contains tables $f$ with $f(c)\in D(c)$. The counit is evaluation $ϵ(f,c)=f(c)$. For a transition $v:X\to C$, both routes around the substitution square send $(f,x)$ to $f(v(x))$; hence $ϵ\circ (\mathrm{id}\times v)$ is the reindexing of evaluation along $v$. Dependent pairs require stable fiberwise dependent tensors and their Beck–Chevalley comparison. The type $!A$ additionally requires the linear–nonlinear adjunction/comonad and its compatible reindexing.