Structural rules

Contexts and variables

$\cdot \mathsf{ctx}$

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

$\mathrm{\Gamma },x:A\mathsf{ctx}$

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

$\mathrm{\Gamma },x:A⊢x:A$

Presuppositions

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

$\mathrm{\Gamma }\mathsf{ctx}$

$\mathrm{\Gamma },x:A\mathsf{ctx}$

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

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

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

$\mathrm{\Gamma }⊢A\equiv B\mathsf{type}$

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

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

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

The omitted right-hand presuppositions follow by symmetry: from $\mathrm{\Gamma }⊢A\equiv B\mathsf{type}$ derive $\mathrm{\Gamma }⊢B\mathsf{type}$, and from $\mathrm{\Gamma }⊢a\equiv b:A$ derive $\mathrm{\Gamma }⊢b:A$.

Equivalence and conversion

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

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

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

$\mathrm{\Gamma }⊢B\equiv A\mathsf{type}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢B\mathsf{type}$$\mathrm{\Gamma }⊢C\mathsf{type}$$\mathrm{\Gamma }⊢A\equiv B\mathsf{type}$$\mathrm{\Gamma }⊢B\equiv C\mathsf{type}$

$\mathrm{\Gamma }⊢A\equiv C\mathsf{type}$

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

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

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

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

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

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

Derived conversion and assumption (primitive economically)

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

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

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

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

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$(x:A)\in \mathrm{\Gamma }$

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

These three rules are not primitive in the official presentation: they are the derived rules of lemma 26.31, lemma 26.32, lemma 26.34. They are recorded here because they are used constantly and become primitive in the economical presentation of definition 26.35.

Weakening, substitution, and context conversion

In the next rules $\mathcal{J}$ is any of the four judgment theses of convention 26.17, and all contexts occurring in premises are required to be well formed.

$\mathrm{\Gamma },x:A,\mathrm{\Delta }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },\mathrm{\Delta }⊢\mathcal{J}$

$\mathrm{\Gamma },x:A,\mathrm{\Delta }⊢\mathcal{J}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:A,\mathrm{\Delta }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma },x:A,\mathrm{\Delta }⊢\mathcal{J}$

$\mathrm{\Gamma },\mathrm{\Delta }[a/x]⊢\mathcal{J}[a/x]$

$\mathrm{\Gamma },x:A,\mathrm{\Delta }\mathsf{ctx}$$\mathrm{\Gamma }⊢A^{\prime }\mathsf{type}$$\mathrm{\Gamma }⊢A\equiv A^{\prime }\mathsf{type}$$\mathrm{\Gamma },x:A,\mathrm{\Delta }⊢\mathcal{J}$

$\mathrm{\Gamma },x:A^{\prime },\mathrm{\Delta }⊢\mathcal{J}$

Derived renaming and interchange

The freshness and independence side conditions belong to the reference rules:

$\mathrm{\Gamma },x:A,\mathrm{\Delta }\mathsf{ctx}$$\mathrm{\Gamma },x:A,\mathrm{\Delta }⊢\mathcal{J}$$x^{\prime }\notin \mathrm{FV}(\mathrm{\Gamma },A,\mathrm{\Delta },\mathcal{J})$

$\mathrm{\Gamma },x^{\prime }:A,\mathrm{\Delta }[x^{\prime }/x]⊢\mathcal{J}[x^{\prime }/x]$

$\mathrm{\Gamma },x:A,y:B,\mathrm{\Delta }\mathsf{ctx}$$\mathrm{\Gamma }⊢B\mathsf{type}$$\mathrm{\Gamma },x:A,y:B,\mathrm{\Delta }⊢\mathcal{J}$

$\mathrm{\Gamma },y:B,x:A,\mathrm{\Delta }⊢\mathcal{J}$

$\mathrm{\Gamma },x:A,\mathrm{\Delta }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢a^{\prime }:A$$\mathrm{\Gamma }⊢a\equiv a^{\prime }:A$$\mathrm{\Gamma },x:A,\mathrm{\Delta }⊢B\mathsf{type}$

$\mathrm{\Gamma },\mathrm{\Delta }[a/x]⊢B[a/x]\equiv B[a^{\prime }/x]\mathsf{type}$

$\mathrm{\Gamma },x:A,\mathrm{\Delta }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢a^{\prime }:A$$\mathrm{\Gamma }⊢a\equiv a^{\prime }:A$$\mathrm{\Gamma },x:A,\mathrm{\Delta }⊢B\mathsf{type}$$\mathrm{\Gamma },x:A,\mathrm{\Delta }⊢b:B$

$\mathrm{\Gamma },\mathrm{\Delta }[a/x]⊢b[a/x]\equiv b[a^{\prime }/x]:B[a/x]$

Congruence scheme

The phrase congruence in every argument is interpreted through a classified parameter telescope, as in definition 26.36. Write $\mathcal{P}=(p_1:J_1,\dots ,p_n:J_n)$, where each $J_i$ is either a type formation judgment or a term typing judgment in a displayed local context; both that context and the classifier may depend on $p_1,\dots ,p_{i-1}$. Given a primed telescope ${\mathcal{P}}^{\prime }$, compare the parameters in order. A type parameter is compared by type equality in the local context already transported along the earlier equalities. A term parameter is compared at the unprimed classifier after transporting the primed classifier and local context along those same earlier equalities. For a type former $F$ and a term former $f:F$, the resulting rules are

$\mathcal{P}\equiv {\mathcal{P}}^{\prime }\text{in classified order}$

$\mathrm{\Gamma }⊢F(\overrightarrow{p})\equiv F({\overrightarrow{p}}^{\prime })\mathsf{type}$

$\mathcal{P}\equiv {\mathcal{P}}^{\prime }\text{in classified order}$

$\mathrm{\Gamma }⊢f(\overrightarrow{p})\equiv f({\overrightarrow{p}}^{\prime }):F(\overrightarrow{p})$

where the primed result in Cong-Tm is first converted along Cong-Ty. Thus $\mathcal{P}\equiv {\mathcal{P}}^{\prime }$ abbreviates one precisely classified equality premise per parameter; it is not a new judgment.

For reference, the classified telescopes of the annotated inductive eliminators are as follows. Every entry is in ambient context $\mathrm{\Gamma }$; a context in brackets is local to that parameter.

• For ${\mathsf{ind}}_{\mathbf{0}}(z.C;v)$: first $C\mathsf{type}[z:\mathbf{0}]$, then $v:\mathbf{0}$.

• For ${\mathsf{ind}}_{\mathbf{2}}(z.C;c_t,c_f;b)$: first $C\mathsf{type}[z:\mathbf{2}]$, followed in order by $c_t:C[\mathsf{tt}/z]$, $c_f:C[\mathsf{ff}/z]$, and $b:\mathbf{2}$.

• For ${\mathsf{ind}}_{+}(z.C;f,g;s)$: first $A\mathsf{type}$ and $B\mathsf{type}$, then

• For ${\mathsf{ind}}_{\mathbb{N}}(n.C;c_0,c_s;m)$: first $C\mathsf{type}[n:\mathbb{N}]$, then $$c_0:C[\mathsf{0}/n],c_s:\prod _{k:\mathbb{N}}(C[k/n]\to C[\mathsf{suc}(k)/n]),m:\mathbb{N}.$$

For ${\mathsf{ind}}_{\mathsf{W}}(w.C;h,t)$ the telescope is $$\begin{array}{c}A\mathsf{type};B\mathsf{type}[x:A];W:={\mathsf{W}}_{x:A}B;C\mathsf{type}[w:W];\\ h:\prod _{a:A}\prod _{\alpha :B[a/x]\to W}((\prod _{y:B[a/x]}C[\alpha (y)/w])\to C[\mathsf{sup}(a,\alpha )/w]);t:W.\end{array}$$ Applying the ordered scheme to these lists supplies motive equality beneath its binder, branch equalities in their substituted fibers, equality of the scrutinee, and conversion of the primed result to the unprimed result type.

Illustrative stable binding extension

The structurally stable operator used to test the congruence scheme has the full rules

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢C\mathsf{type}$$\mathrm{\Gamma },y:C⊢D\mathsf{type}$

$\mathrm{\Gamma }⊢Q(C;y.D)\mathsf{type}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢C\mathsf{type}$$\mathrm{\Gamma }⊢C^{\prime }\mathsf{type}$$\mathrm{\Gamma }⊢C\equiv C^{\prime }\mathsf{type}$$\mathrm{\Gamma },y:C⊢D\mathsf{type}$$\mathrm{\Gamma },y:C⊢D^{\prime }\mathsf{type}$$\mathrm{\Gamma },y:C⊢D\equiv D^{\prime }\mathsf{type}$$\mathrm{\Gamma },y:C^{\prime }⊢D^{\prime }\mathsf{type}$

$\mathrm{\Gamma }⊢Q(C;y.D)\equiv Q(C^{\prime };y.D^{\prime })\mathsf{type}$