Extensional type theory: the delta

ETT extends the raw binding signature by ${\mathsf{Eq}}_A(a,b)$ of arity $(0,0,0)$ and the annotated constructor ${\mathsf{eqrefl}}_a$ of arity $(0)$. We print the latter as $\mathsf{refl}$ when its expected type determines $a$.

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢b:A$

$\mathrm{\Gamma }⊢{\mathsf{Eq}}_A(a,b)\mathsf{type}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢a:A$

$\mathrm{\Gamma }⊢\mathsf{refl}:{\mathsf{Eq}}_A(a,a)$

When Russell universes are present, the additional closure rule is

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢b:A$

$\mathrm{\Gamma }⊢{\mathsf{Eq}}_A(a,b):{\mathcal{U}}_i$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢b:A$$\mathrm{\Gamma }⊢p:{\mathsf{Eq}}_A(a,b)$

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

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢b:A$$\mathrm{\Gamma }⊢p:{\mathsf{Eq}}_A(a,b)$

$\mathrm{\Gamma }⊢p\equiv \mathsf{refl}:{\mathsf{Eq}}_A(a,b)$

The classified congruence rules are

$\mathrm{\Gamma }⊢A\equiv A^{\prime }\mathsf{type}$$\mathrm{\Gamma }⊢a\equiv a^{\prime }:A$$\mathrm{\Gamma }⊢b\equiv b^{\prime }:A$

$\mathrm{\Gamma }⊢{\mathsf{Eq}}_A(a,b)\equiv {\mathsf{Eq}}_{A^{\prime }}(a^{\prime },b^{\prime })\mathsf{type}$

$\mathrm{\Gamma }⊢a\equiv a^{\prime }:A$

$\mathrm{\Gamma }⊢{\mathsf{eqrefl}}_a\equiv {\mathsf{eqrefl}}_{a^{\prime }}:{\mathsf{Eq}}_A(a,a)$

The optional ETT propositional-truncation delta is the following. In Tr-E, the equality premise says that $C$ is a proposition. Its raw signature adds $\Vert A\Vert$ and $|a|$ of arity $(0)$ and the recursor ${\mathsf{rec}}_{\Vert A\Vert }(x.c,t)$ of arity $(1,0)$, binding $x$ in $c$.

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$

$\mathrm{\Gamma }⊢\Vert A\Vert \mathsf{type}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢a:A$

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

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢p:\Vert A\Vert$$\mathrm{\Gamma }⊢q:\Vert A\Vert$

$\mathrm{\Gamma }⊢p\equiv q:\Vert A\Vert$

Its classified congruence rules are

$\mathrm{\Gamma }⊢A\equiv A^{\prime }\mathsf{type}$

$\mathrm{\Gamma }⊢\Vert A\Vert \equiv \Vert A^{\prime }\Vert \mathsf{type}$

$\mathrm{\Gamma }⊢a\equiv a^{\prime }:A$

$\mathrm{\Gamma }⊢|a|\equiv |a^{\prime }|:\Vert A\Vert$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢C\mathsf{type}$$\mathrm{\Gamma },y:C,z:C\mathsf{ctx}$$\mathrm{\Gamma },y:C,z:C⊢y\equiv z:C$$\mathrm{\Gamma },x:A⊢c:C$$\mathrm{\Gamma }⊢t:\Vert A\Vert$

$\mathrm{\Gamma }⊢{\mathsf{rec}}_{\Vert A\Vert }(x.c,t):C$

After conversion of the primed data to the displayed common types, recursor congruence is

$\mathrm{\Gamma }⊢C\equiv C^{\prime }\mathsf{type}$$\mathrm{\Gamma },y:C,z:C⊢y\equiv z:C$$\mathrm{\Gamma },x:A⊢c\equiv c^{\prime }:C$$\mathrm{\Gamma }⊢t\equiv t^{\prime }:\Vert A\Vert$

$\mathrm{\Gamma }⊢{\mathsf{rec}}_{\Vert A\Vert }(x.c,t)\equiv {\mathsf{rec}}_{\Vert A\Vert }(x.c^{\prime },t^{\prime }):C$

There is no separate computation rule: both the recursor applied to $|a|$ and $c[a/x]$ inhabit the proposition $C$, so the displayed proof-irrelevance premise already makes them judgmentally equal. No base rule is removed; equality reflection makes transport silent and derives UIP and function extensionality.