Logic enrichment, same-subject types, and erased induction

The LTT logical and set fragments

For typed contexts $\mathrm{\Gamma }$ and proposition lists $\mathrm{\Delta }$, the logical rules used in chapter 92 are

$\mathrm{\Gamma }\mathsf{valid}$

$\mathrm{\Gamma }⊢\mathrm{\perp }\mathsf{Prop}$

$\mathrm{\Gamma }⊢P\mathsf{Prop}$$\mathrm{\Gamma }⊢Q\mathsf{Prop}$

$\mathrm{\Gamma }⊢P\Rightarrow Q\mathsf{Prop}$

$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A⊢P\mathsf{Prop}$

$\mathrm{\Gamma }⊢\mathrm{\forall }x:A.P\mathsf{Prop}$

$\mathrm{\Gamma }⊢a:\mathsf{U}$$\mathrm{\Gamma }⊢t:\mathsf{T}(a)$$\mathrm{\Gamma }⊢X:\mathsf{Set}(\mathsf{T}(a))$

$\mathrm{\Gamma }⊢t{\in }_{a}X\mathsf{Prop}$

$P\in \mathrm{\Delta }$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P$

$\mathrm{\Gamma };\mathrm{\Delta },P⊢Q$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P\Rightarrow Q$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P\Rightarrow Q$$\mathrm{\Gamma };\mathrm{\Delta }⊢P$

$\mathrm{\Gamma };\mathrm{\Delta }⊢Q$

$\mathrm{\Gamma },x:A;\mathrm{\Delta }⊢P$$x\notin \mathrm{FV}(\mathrm{\Delta })$

$\mathrm{\Gamma };\mathrm{\Delta }⊢\mathrm{\forall }x:A.P$

$\mathrm{\Gamma };\mathrm{\Delta }⊢\mathrm{\forall }x:A.P$$\mathrm{\Gamma }⊢t:A$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P[t/x]$

$\mathrm{\Gamma };\mathrm{\Delta },P\Rightarrow \mathrm{\perp }⊢\mathrm{\perp }$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P$

The small-set rules, in formation through uniqueness order, are

$\mathrm{\Gamma }⊢a:\mathsf{U}$

$\mathrm{\Gamma }⊢\mathsf{Set}(\mathsf{T}(a))\mathsf{type}$

$\mathrm{\Gamma }⊢a:\mathsf{U}$$\mathrm{\Gamma },x:\mathsf{T}(a)⊢p\mathsf{prop}$

$\mathrm{\Gamma }⊢\{x:\mathsf{T}(a)\mid p\}:\mathsf{Set}(\mathsf{T}(a))$

$\mathrm{\Gamma }⊢X:\mathsf{Set}(\mathsf{T}(a))$$\mathrm{\Gamma }⊢t:\mathsf{T}(a)$

$\mathrm{\Gamma }⊢t{\in }_{a}X\mathsf{Prop}$

$\mathrm{\Gamma },x:\mathsf{T}(a)⊢p\mathsf{prop}$$\mathrm{\Gamma }⊢t:\mathsf{T}(a)$

$\mathrm{\Gamma };\varnothing ⊢(t{\in }_a\{x:\mathsf{T}(a)\mid p\})\iff \mathsf{V}(p[t/x])$

$\mathrm{\Gamma }⊢X:\mathsf{Set}(\mathsf{T}(a))$$\mathrm{\Gamma }⊢Y:\mathsf{Set}(\mathsf{T}(a))$$\mathrm{\Gamma };\varnothing ⊢\mathrm{\forall }x:\mathsf{T}(a).(x{\in }_{a}X\iff x{\in }_{a}Y)$

$\mathrm{\Gamma }⊢X\equiv Y:\mathsf{Set}(\mathsf{T}(a))$

For $b:\mathsf{N}\to \mathsf{U}$, put $B(n)=\mathsf{T}(bn)$. Given $c:B(0)$ and $f:\mathrm{\Pi }n:\mathsf{N}.B(n)\to B(Sn)$, recursion has type ${\mathsf{rec}}_B(c,f):\mathrm{\Pi }n:\mathsf{N}.B(n)$ with equations ${\mathsf{rec}}_B(c,f,0)\equiv c$ and ${\mathsf{rec}}_B(c,f,Sn)\equiv f(n,{\mathsf{rec}}_B(c,f,n))$ (LTT-Nat-rec, LTT-Nat-rec-$0$, and LTT-Nat-rec-$S$). Rule LTT-Nat-Ind${}_0$ is

$\mathrm{\Gamma },n:\mathsf{N}⊢p\mathsf{prop}$$\mathrm{\Gamma };\mathrm{\Delta }⊢\mathsf{V}(p[0/n])$$\mathrm{\Gamma },n:\mathsf{N};\mathrm{\Delta },\mathsf{V}(p)⊢\mathsf{V}(p[Sn/n])$

$\mathrm{\Gamma };\mathrm{\Delta }⊢\mathrm{\forall }n:\mathsf{N}.\mathsf{V}(p)$

Dependent intersections and System S self types

$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A⊢B\mathsf{type}$

$\mathrm{\Gamma }⊢x:A\cap B\mathsf{type}$

$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢b:B[a/x]$$\mathrm{erase}(a){=}_{\beta \eta }\mathrm{erase}(b)$

$\mathrm{\Gamma }⊢\mathsf{both}(a,b):x:A\cap B$

$\mathrm{\Gamma }⊢d:x:A\cap B$

$\mathrm{\Gamma }⊢\mathsf{left}(d):A$

$\mathrm{\Gamma }⊢d:x:A\cap B$

$\mathrm{\Gamma }⊢\mathsf{right}(d):B[\mathsf{left}(d)/x]$

The computations and uniqueness are These are DI-${\beta }_1$, DI-${\beta }_2$, and DI-$\eta$.

System S implicit products have

$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A⊢B\mathsf{type}$

$\mathrm{\Gamma }⊢\mathrm{\forall }x:A.B\mathsf{type}$

$\mathrm{\Gamma },x:A⊢t:B$$x\notin \mathrm{FV}(t)$

$\mathrm{\Gamma }⊢t:\mathrm{\forall }x:A.B$

$\mathrm{\Gamma }⊢t:\mathrm{\forall }x:A.B$$\mathrm{\Gamma }⊢u:A$

$\mathrm{\Gamma }⊢t:B[u/x]$

Rule S-$\mathrm{\forall }$-$\beta$ records $\mathrm{erase}(t)=\mathrm{erase}(t)$. Self formation, generation, and instantiation are

$\mathrm{\Gamma },x:\iota x.T⊢T\mathsf{type}$

$\mathrm{\Gamma }⊢\iota x.T\mathsf{type}$

$\mathrm{\Gamma }⊢t:T[t/x]$$\mathrm{\Gamma }⊢\iota x.T\mathsf{type}$

$\mathrm{\Gamma }⊢t:\iota x.T$

$\mathrm{\Gamma }⊢t:\iota x.T$

$\mathrm{\Gamma }⊢t:T[t/x]$

Rule S-Self-Erase states that the generation and instantiation views both erase to $\mathrm{erase}(t)$.

Very-dependent functions

Write $g:\mathsf{Pred}(y)$ for the predecessor function at $y$.

$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },y:A,g:\mathsf{Pred}(y)⊢B[g,y/f,x]\mathsf{type}$

$\mathrm{\Gamma }⊢\{f\mid x:A\to B[f,x]\}\mathsf{type}$

$\mathrm{\Gamma },x:A,g:\mathsf{Pred}(x)⊢b:B[g,x/f,x]$${\mathsf{Ext}}_{A,B}(b)$

$\mathrm{\Gamma }⊢\lambda x.b:\{f\mid x:A\to B[f,x]\}$

$\mathrm{\Gamma }⊢f:\{f\mid x:A\to B[f,x]\}$$\mathrm{\Gamma }⊢a:A$

$\mathrm{\Gamma }⊢f(a):B[f,a/f,x]$

$\mathrm{\Gamma }⊢a:A$

$\mathrm{\Gamma }⊢f_1:\{f\mid x:A\to B[f,x]\}$$\mathrm{\Gamma }⊢f_2:\{f\mid x:A\to B[f,x]\}$$\mathrm{\forall }a:A.\mathrm{\Gamma }⊢f_1(a)\equiv f_2(a):B[f_1,a/f,x]$

$\mathrm{\Gamma }⊢f_1\equiv f_2:\{f\mid x:A\to B[f,x]\}$

Cedille Core

The kinding rules for $\mathrm{\Pi }$, erased $\mathrm{\forall }$, dependent intersection, and heterogeneous equality are

$\mathrm{\Gamma }⊢T\Rightarrow \star$$\mathrm{\Gamma },x:T⊢T^{\prime }\Rightarrow \star$

$\mathrm{\Gamma }⊢\mathrm{\Pi }x:T.T^{\prime }\Rightarrow \star$

$\mathrm{\Gamma }⊢T\Rightarrow \star$$\mathrm{\Gamma },x:T⊢T^{\prime }\Rightarrow \star$

$\mathrm{\Gamma }⊢\mathrm{\forall }x:T.T^{\prime }\Rightarrow \star$

$\mathrm{\Gamma }⊢T\Rightarrow \star$$\mathrm{\Gamma },x:T⊢T^{\prime }\Rightarrow \star$

$\mathrm{\Gamma }⊢\iota x:T.T^{\prime }\Rightarrow \star$

$\mathrm{FV}(t,t^{\prime })\subseteq \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Gamma }⊢\{t\simeq t^{\prime }\}\Rightarrow \star$

Retained and erased functions use

$T{{⟶}^{\ast }}_{\mathrm{cbn}}\mathrm{\Pi }x:T_1.T_2$$\mathrm{\Gamma },x:T_1⊢t\Leftarrow T_2$

$\mathrm{\Gamma }⊢\lambda x.t\Leftarrow T$

$\mathrm{\Gamma }⊢f\Rightarrow \mathrm{\Pi }x:T_1.T_2$$\mathrm{\Gamma }⊢u\Leftarrow T_1$

$\mathrm{\Gamma }⊢fu\Rightarrow T_2[u/x]$

$(\lambda x.t)u⟶t[u/x]$

$T{{⟶}^{\ast }}_{\mathrm{cbn}}\mathrm{\forall }x:T_1.T_2$$\mathrm{\Gamma },x:T_1⊢t\Leftarrow T_2$$x\notin \mathrm{FV}(\mathrm{erase}(t))$

$\mathrm{\Gamma }⊢\mathrm{\Lambda }x.t\Leftarrow T$

$\mathrm{\Gamma }⊢f\Rightarrow \mathrm{\forall }x:T_1.T_2$$\mathrm{\Gamma }⊢u\Leftarrow T_1$

$\mathrm{\Gamma }⊢f-u\Rightarrow T_2[u/x]$

Rule CDLE-$\mathrm{\forall }$-$\beta$ states $\mathrm{erase}((\mathrm{\Lambda }x.t)-u)=\mathrm{erase}(t)$. Dependent intersections use

$T{{⟶}^{\ast }}_{\mathrm{cbn}}\iota x:T_1.T_2$$\mathrm{\Gamma }⊢t_1\Leftarrow T_1$$\mathrm{\Gamma }⊢t_2\Leftarrow T_2[t_1/x]$$\mathrm{erase}(t_1){=}_{\beta \eta }\mathrm{erase}(t_2)$

$\mathrm{\Gamma }⊢[t_1,t_2]\Leftarrow T$

$\mathrm{\Gamma }⊢t\Rightarrow \iota x:T.T^{\prime }$

$\mathrm{\Gamma }⊢t.1\Rightarrow T$

$\mathrm{\Gamma }⊢t\Rightarrow \iota x:T.T^{\prime }$

$\mathrm{\Gamma }⊢t.2\Rightarrow T^{\prime }[t.1/x]$

Rule CDLE-Isect-$\beta$ is $\mathrm{erase}([t_1,t_2].1)=\mathrm{erase}(t_1){=}_{\beta \eta }\mathrm{erase}(t_2)=\mathrm{erase}([t_1,t_2].2)$. Finally,

$T{{⟶}^{\ast }}_{\mathrm{cbn}}\{t_1\simeq t_2\}$$\mathrm{FV}(u)\subseteq \mathrm{dom}(\mathrm{\Gamma })$$\mathrm{erase}(t_1){=}_{\beta \eta }\mathrm{erase}(t_2)$

$\mathrm{\Gamma }⊢\beta \{u\}\Leftarrow T$

$\mathrm{\Gamma }⊢p\Rightarrow \{t_1\simeq t_2^{\prime }\}$$\mathrm{erase}(t_2^{\prime }){=}_{\beta \eta }\mathrm{erase}(t_2)$$\mathrm{\Gamma }⊢T[t_2/x]\Rightarrow \star$$\mathrm{\Gamma }⊢u\Leftarrow T[t_2/x]$$T[t_1/x]\cong T^{\prime }$

$\mathrm{\Gamma }⊢\rho p@x⟨t_2⟩.T-u\Leftarrow T^{\prime }$

$\mathrm{\Gamma }⊢p\Leftarrow \{t\simeq u\}$$\mathrm{\Gamma }⊢t\Leftarrow T$$\mathrm{FV}(u)\subseteq \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Gamma }⊢\varphi p-t\{u\}\Leftarrow T$

$\mathrm{\Gamma }⊢p\Rightarrow \{\lambda x.\lambda y.x\simeq \lambda x.\lambda y.y\}$

$\mathrm{\Gamma }⊢\delta -p\Leftarrow T$

$\mathrm{\Gamma }⊢T\Rightarrow \star$$\mathrm{\Gamma }⊢t\Leftarrow T$

$\mathrm{\Gamma }⊢\chi T-t\Rightarrow T$