Indexed signatures, records, and descriptions

Vec, Fin, and valid case trees

For $A:{\mathcal{U}}_i$ the indexed family is formed and introduced by $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢A:{\mathcal{U}}_i\\ \mathrm{\Gamma }⊢n:\mathbb{N}\end{array}}{\mathrm{\Gamma }⊢\mathsf{Vec}(A,n):{\mathcal{U}}_i}\mathrm{Vec}-\mathrm{form}$$ $$\frac{\mathrm{\Gamma }⊢A:{\mathcal{U}}_i}{\mathrm{\Gamma }⊢\mathsf{vnil}:\mathsf{Vec}(A,\mathsf{0})}\mathrm{Vec}-{\mathrm{intro}}_0$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢n:\mathbb{N}\\ \mathrm{\Gamma }⊢a:A\\ \mathrm{\Gamma }⊢xs:\mathsf{Vec}(A,n)\end{array}}{\mathrm{\Gamma }⊢\mathsf{vcons}(n,a,xs):\mathsf{Vec}(A,\mathsf{suc}(n))}\mathrm{Vec}-{\mathrm{intro}}_{\mathrm{s}}.$$ Writing $P_0=P(\mathsf{0},\mathsf{vnil})$ and $P_s=P(\mathsf{suc}(n),\mathsf{vcons}(n,a,xs))$, elimination is $$\frac{\begin{array}{c}\mathrm{\Gamma },n:\mathbb{N},v:\mathsf{Vec}(A,n)⊢P(n,v):{\mathcal{U}}_j\\ \mathrm{\Gamma }⊢p_0:P_0\\ \mathrm{\Gamma },n:\mathbb{N},a:A,xs:\mathsf{Vec}(A,n),q:P(n,xs)⊢p_s:P_s\\ \mathrm{\Gamma }⊢m:\mathbb{N}\\ \mathrm{\Gamma }⊢ys:\mathsf{Vec}(A,m)\end{array}}{\mathrm{\Gamma }⊢\mathsf{vind}(P;p_0;p_s;m,ys):P(m,ys)}\mathrm{Vec}-\mathrm{elim}.$$ Its two computations are printed separately to expose their constructor premises. Abbreviate $r_{n,xs}:=\mathsf{vind}(P;p_0;p_s;n,xs)$ and $V_{n,a,xs}:=\mathsf{vind}(P;p_0;p_s;\mathsf{suc}(n),\mathsf{vcons}(n,a,xs))$. $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢P\mathsf{motive}\\ \mathrm{\Gamma }⊢p_0:P_0\end{array}}{\mathrm{\Gamma }⊢\mathsf{vind}(P;p_0;p_s;\mathsf{0},\mathsf{vnil})\equiv p_0:P_0}\mathrm{Vec}-{\mathrm{comp}}_1$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢n:\mathbb{N}\\ \mathrm{\Gamma }⊢a:A\\ \mathrm{\Gamma }⊢xs:\mathsf{Vec}(A,n)\end{array}}{\mathrm{\Gamma }⊢V_{n,a,xs}\equiv p_s[n,a,xs,r_{n,xs}]:P_s}\mathrm{Vec}-{\mathrm{comp}}_2$$

${\mathsf{Fin}}_{\mathrm{ind}}$ has $\mathsf{fz}(n):{\mathsf{Fin}}_{\mathrm{ind}}(\mathsf{suc}(n))$ and $\mathsf{fs}(n,k):{\mathsf{Fin}}_{\mathrm{ind}}(\mathsf{suc}(n))$ from $k:{\mathsf{Fin}}_{\mathrm{ind}}(n)$. For $Q(n,k):{\mathcal{U}}_j$, methods give the full elimination rule $$\frac{\begin{array}{c}\mathrm{\Gamma },n:\mathbb{N},k:{\mathsf{Fin}}_{\mathrm{ind}}(n)⊢Q(n,k):{\mathcal{U}}_j\\ \mathrm{\Gamma }⊢q_z:(n:\mathbb{N})\to Q(\mathsf{suc}(n),\mathsf{fz}(n))\\ \mathrm{\Gamma }⊢q_s:(n:\mathbb{N})(k:{\mathsf{Fin}}_{\mathrm{ind}}(n))\to Q(n,k)\to Q(\mathsf{suc}(n),\mathsf{fs}(n,k))\\ \mathrm{\Gamma }⊢m:\mathbb{N}\\ \mathrm{\Gamma }⊢l:{\mathsf{Fin}}_{\mathrm{ind}}(m)\end{array}}{\mathrm{\Gamma }⊢\mathsf{find}(Q;q_z;q_s;m,l):Q(m,l)}\mathrm{Fin}-\mathrm{elim}.$$ Its computations are

Put $${\mathsf{Comp}}_{\mathcal{C}}(f^{\prime }):=(\overrightarrow{t}:\mathrm{\Delta })(u:T).{\mathsf{CT}}_{\mathcal{C}}(\overrightarrow{t},u)\to f^{\prime }\overrightarrow{t}\equiv u[f^{\prime }/f].$$ The case-tree compiler has the theorem rule $$\frac{\begin{array}{c}f:(\overrightarrow{t}:\mathrm{\Delta })\to T\text{has a valid case tree }\mathcal{C}\\ \mathcal{C}\text{uses no deletion}\\ \text{every injectivity step first self-unifies the constructor index}\end{array}}{\mathrm{\exists }{f}^{\prime }:(\overrightarrow{t}:\mathrm{\Delta })\to T.{\mathsf{Comp}}_{\mathcal{C}}(f^{\prime })}\mathrm{Compile}.$$ Validity also includes well-typed leaves, dependency-preserving unifier factorizations, structural recursion, and the proof-relevant basic-analysis, specialization, and no-confusion transitions of definition 78.15. These are premises, not consequences of an unrestricted coverage checker.

For IR signatures, $\mathsf{intro}:{\mathsf{E}}_S(\mathsf{IR}(S),\mathsf{El})\to \mathsf{IR}(S)$ and $\mathsf{El}(\mathsf{intro}(x))\equiv {\mathsf{F}}_S(x)$. IIR adds an index to $\mathsf{IR}$ and to the decoder. The context/type IIT has simultaneous $\mathsf{Con}$ and $\mathsf{Ty}:\mathsf{Con}\to \mathcal{U}$ eliminators with the four computations for empty, extension, universe, and decoding recorded in section 78.5.

Pollack true records

$$\frac{\begin{array}{c}\mathrm{\Gamma }⊢L\mathsf{type}\\ \mathrm{\Gamma },l:L⊢A\mathsf{type}\end{array}}{\mathrm{\Gamma }⊢⟨L,r:A⟩\mathsf{type}}\mathrm{Rec}-\mathrm{form}$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢⟨L,r:A⟩\mathsf{type}\\ \mathrm{\Gamma }⊢l:L\\ \mathrm{\Gamma }⊢a:A(l)\end{array}}{\mathrm{\Gamma }⊢⟨l,r=a⟩:⟨L,r:A⟩}\mathrm{Rec}-\mathrm{intro}.$$ Restriction removes the visible field and projection returns it: $$\frac{\mathrm{\Gamma }⊢l:⟨L,r:A⟩}{\mathrm{\Gamma }⊢l|r:L}\mathrm{Rec}-\mathrm{rest}\frac{\mathrm{\Gamma }⊢l:⟨L,r:A⟩}{\mathrm{\Gamma }⊢l.r:A[l|r/x]}\mathrm{Rec}-\mathrm{proj}.$$ The computation equations, including right-to-left passing, are The pass-typing schemas reconstruct the recursively established searched field type $P$: $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢l:⟨L,r:A⟩\\ \mathrm{\Gamma }⊢(l|r)|p:P\\ r\ne p\end{array}}{\mathrm{\Gamma }⊢l|p:P}\mathrm{Rec}-\mathrm{rest}-\mathrm{pass}$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢l:⟨L,r:A⟩\\ \mathrm{\Gamma }⊢(l|r).p:P\\ r\ne p\end{array}}{\mathrm{\Gamma }⊢l.p:P}\mathrm{Rec}-\mathrm{proj}-\mathrm{pass}.$$ Repeated labels select the rightmost occurrence. There is no width rule and no judgmental record eta.

Regular and indexed description codes

The finite regular normal form has $\mathsf{one}$, $\mathsf{K}(A)$, $\mathsf{X}(j)$, sum, product, and finite-tag $\mathsf{sigma}(A,F)$. For $X:I\to {\mathcal{U}}_i$ its interpretation is For $D:I\to {\mathsf{Desc}}_i(I)$, fixed-point formation, introduction, and observation are $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢I:{\mathcal{U}}_i\\ \mathrm{\Gamma },j:I⊢D(j):{\mathsf{Desc}}_i(I)\end{array}}{\mathrm{\Gamma }⊢\mathsf{Mu}(D):I\to {\mathcal{U}}_i}\mathrm{Mu}-\mathrm{form}$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢j:I\\ \mathrm{\Gamma }⊢u:[[D(j)]](\mathsf{Mu}(D))\end{array}}{\mathrm{\Gamma }⊢{\mathsf{roll}}_j(u):\mathsf{Mu}(D)(j)}\mathrm{Mu}-\mathrm{intro}$$ $${\mathsf{out}}_j:\mathsf{Mu}(D)(j)\to [[D(j)]](\mathsf{Mu}(D))$$ with $${\mathsf{out}}_j({\mathsf{roll}}_j(u))\equiv u.$$ For $P:(j:I)\to \mathsf{Mu}(D)(j)\to {\mathcal{U}}_k$, define $\mathsf{All}$ structurally, with ${\mathsf{All}}_{\mathsf{X}(j)}(P,x)=P(j,x)$ and products of hypotheses at product codes. The induction rule and computation are $$\frac{\begin{array}{c}s:(j:I)(u:[[D(j)]](\mathsf{Mu}(D)))\to {\mathsf{All}}_{D(j)}(P,u)\to P(j,{\mathsf{roll}}_j(u))\\ t:\mathsf{Mu}(D)(j)\end{array}}{{\mathsf{ind}}_D(P,s;j,t):P(j,t)}\mathrm{Desc}-\mathrm{ind}$$ $${\mathsf{ind}}_D(P,s;j,{\mathsf{roll}}_j(u))\equiv s_j(u,{\mathsf{calls}}_{D(j)}(P,{\mathsf{ind}}_D(P,s),u)).$$ The principal MAG universe separately has input variables, $0$, $1$, ${\mathrm{\Sigma }}_f$, ${\mathrm{\Pi }}_f$, and $\mu$. Its ${\mathrm{\Sigma }}_f$ interpretation stores a witness, an equality $f(o)=o^{\prime }$, and the branch payload; ${\mathrm{\Pi }}_f$ quantifies over such witnesses. Decidable equality is defined only on the finite $\mathsf{EqDesc}$ grammar of unit, decidable constants, recursive positions, sums, and products.