The intensional base formers

Dependent products

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

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

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

$\mathrm{\Gamma }⊢\lambda (x:A).b:\prod _{x:A}B$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A⊢B\mathsf{type}$$\mathrm{\Gamma }⊢f:\prod _{x:A}B$$\mathrm{\Gamma }⊢a:A$

$\mathrm{\Gamma }⊢fa:B[a/x]$

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

$\mathrm{\Gamma }⊢(\lambda (x:A).b)a\equiv b[a/x]:B[a/x]$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A⊢B\mathsf{type}$$\mathrm{\Gamma }⊢f:\prod _{x:A}B$

$\mathrm{\Gamma }⊢f\equiv \lambda (x:A).fx:\prod _{x:A}B$

The corresponding named congruence rules restore the formation and typing presuppositions of both sides:

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

$\mathrm{\Gamma }⊢\prod _{x:A}B\equiv \prod _{x:A^{\prime }}{B}^{\prime }\mathsf{type}$

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

$\mathrm{\Gamma }⊢\lambda (x:A).b\equiv \lambda (x:A^{\prime }).b^{\prime }:\prod _{x:A}B$

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

$\mathrm{\Gamma }⊢fa\equiv f^{\prime }{a}^{\prime }:B[a/x]$

The derived evaluation form includes the fresh generic argument explicitly:

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A⊢B\mathsf{type}$$\mathrm{\Gamma }⊢f:\prod _{x:A}B$$z\notin \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Gamma },z:A⊢fz:B[z/x]$

Dependent sums and unit

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

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

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A⊢B\mathsf{type}$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢b:B[a/x]$

$\mathrm{\Gamma }⊢(a,b):\sum _{x:A}B$

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

$\mathrm{\Gamma }⊢{\mathsf{pr}}_1(p):A$

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

$\mathrm{\Gamma }⊢{\mathsf{pr}}_2(p):B[{\mathsf{pr}}_1(p)/x]$

$\mathrm{\Gamma },x:A⊢B\mathsf{type}$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢b:B[a/x]$

$\mathrm{\Gamma }⊢{\mathsf{pr}}_1((a,b))\equiv a:A$

$\mathrm{\Gamma },x:A⊢B\mathsf{type}$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢b:B[a/x]$

$\mathrm{\Gamma }⊢{\mathsf{pr}}_2((a,b))\equiv b:B[a/x]$

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

$\mathrm{\Gamma }⊢p\equiv ({\mathsf{pr}}_1(p),{\mathsf{pr}}_2(p)):\sum _{x:A}B$

The named term congruence rules, with every direct presupposition restored, are

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

$\mathrm{\Gamma }⊢(a,b)\equiv (a^{\prime },b^{\prime }):\sum _{x:A}B$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A⊢B\mathsf{type}$$\mathrm{\Gamma }⊢p:\sum _{x:A}B$$\mathrm{\Gamma }⊢p^{\prime }:\sum _{x:A}B$$\mathrm{\Gamma }⊢p\equiv p^{\prime }:\sum _{x:A}B$

$\mathrm{\Gamma }⊢{\mathsf{pr}}_1(p)\equiv {\mathsf{pr}}_1(p^{\prime }):A$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A⊢B\mathsf{type}$$\mathrm{\Gamma }⊢p:\sum _{x:A}B$$\mathrm{\Gamma }⊢p^{\prime }:\sum _{x:A}B$$\mathrm{\Gamma }⊢p\equiv p^{\prime }:\sum _{x:A}B$

$\mathrm{\Gamma }⊢{\mathsf{pr}}_2(p)\equiv {\mathsf{pr}}_2(p^{\prime }):B[{\mathsf{pr}}_1(p)/x]$

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

$\mathrm{\Gamma }⊢\mathbf{1}\mathsf{type}$

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

$\mathrm{\Gamma }⊢\star :\mathbf{1}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢u:\mathbf{1}$

$\mathrm{\Gamma }⊢u\equiv \star :\mathbf{1}$

Empty type, Booleans, and coproducts

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

$\mathrm{\Gamma }⊢\mathbf{0}\mathsf{type}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },z:\mathbf{0}⊢C\mathsf{type}$$\mathrm{\Gamma }⊢v:\mathbf{0}$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbf{0}}(z.C;v):C[v/z]$

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

$\mathrm{\Gamma }⊢\mathbf{2}\mathsf{type}$

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

$\mathrm{\Gamma }⊢\mathsf{tt}:\mathbf{2}$

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

$\mathrm{\Gamma }⊢\mathsf{ff}:\mathbf{2}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },z:\mathbf{2}⊢C\mathsf{type}$$\mathrm{\Gamma }⊢c_t:C[\mathsf{tt}/z]$$\mathrm{\Gamma }⊢c_f:C[\mathsf{ff}/z]$$\mathrm{\Gamma }⊢b:\mathbf{2}$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbf{2}}(z.C;c_t,c_f;b):C[b/z]$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },z:\mathbf{2}⊢C\mathsf{type}$$\mathrm{\Gamma }⊢c_t:C[\mathsf{tt}/z]$$\mathrm{\Gamma }⊢c_f:C[\mathsf{ff}/z]$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbf{2}}(z.C;c_t,c_f;\mathsf{tt})\equiv c_t:C[\mathsf{tt}/z]$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },z:\mathbf{2}⊢C\mathsf{type}$$\mathrm{\Gamma }⊢c_t:C[\mathsf{tt}/z]$$\mathrm{\Gamma }⊢c_f:C[\mathsf{ff}/z]$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbf{2}}(z.C;c_t,c_f;\mathsf{ff})\equiv c_f:C[\mathsf{ff}/z]$

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

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

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

$\mathrm{\Gamma }⊢\mathsf{inl}(a):A+B$

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

$\mathrm{\Gamma }⊢\mathsf{inr}(b):A+B$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢B\mathsf{type}$$\mathrm{\Gamma },z:A+B⊢C\mathsf{type}$$\mathrm{\Gamma }⊢f:\prod _{x:A}C[\mathsf{inl}(x)/z]$$\mathrm{\Gamma }⊢g:\prod _{y:B}C[\mathsf{inr}(y)/z]$$\mathrm{\Gamma }⊢s:A+B$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{+}(z.C;f,g;s):C[s/z]$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢B\mathsf{type}$$\mathrm{\Gamma },z:A+B⊢C\mathsf{type}$$\mathrm{\Gamma }⊢f:\prod _{x:A}C[\mathsf{inl}(x)/z]$$\mathrm{\Gamma }⊢g:\prod _{y:B}C[\mathsf{inr}(y)/z]$$\mathrm{\Gamma }⊢a:A$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{+}(z.C;f,g;\mathsf{inl}(a))\equiv fa:C[\mathsf{inl}(a)/z]$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢B\mathsf{type}$$\mathrm{\Gamma },z:A+B⊢C\mathsf{type}$$\mathrm{\Gamma }⊢f:\prod _{x:A}C[\mathsf{inl}(x)/z]$$\mathrm{\Gamma }⊢g:\prod _{y:B}C[\mathsf{inr}(y)/z]$$\mathrm{\Gamma }⊢b:B$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{+}(z.C;f,g;\mathsf{inr}(b))\equiv gb:C[\mathsf{inr}(b)/z]$

Natural numbers and W-types

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

$\mathrm{\Gamma }⊢\mathbb{N}\mathsf{type}$

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

$\mathrm{\Gamma }⊢\mathsf{0}:\mathbb{N}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢n:\mathbb{N}$

$\mathrm{\Gamma }⊢\mathsf{suc}(n):\mathbb{N}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },n:\mathbb{N}⊢C\mathsf{type}$$\mathrm{\Gamma }⊢c_0:C[\mathsf{0}/n]$$\mathrm{\Gamma }⊢c_s:\prod _{k:\mathbb{N}}(C[k/n]\to C[\mathsf{suc}(k)/n])$$\mathrm{\Gamma }⊢m:\mathbb{N}$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbb{N}}(n.C;c_0,c_s;m):C[m/n]$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },n:\mathbb{N}⊢C\mathsf{type}$$\mathrm{\Gamma }⊢c_0:C[\mathsf{0}/n]$$\mathrm{\Gamma }⊢c_s:\prod _{k:\mathbb{N}}(C[k/n]\to C[\mathsf{suc}(k)/n])$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbb{N}}(n.C;c_0,c_s;\mathsf{0})\equiv c_0:C[\mathsf{0}/n]$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },n:\mathbb{N}⊢C\mathsf{type}$$\mathrm{\Gamma }⊢c_0:C[\mathsf{0}/n]$$\mathrm{\Gamma }⊢c_s:\prod _{k:\mathbb{N}}(C[k/n]\to C[\mathsf{suc}(k)/n])$$\mathrm{\Gamma }⊢m:\mathbb{N}$

$\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbb{N}}(n.C;c_0,c_s;\mathsf{suc}(m))\equiv c_{s}m({\mathsf{ind}}_{\mathbb{N}}(n.C;c_0,c_s;m)):C[\mathsf{suc}(m)/n]$

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

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

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A⊢B\mathsf{type}$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢f:B[a/x]\to {\mathsf{W}}_{x:A}B$

$\mathrm{\Gamma }⊢\mathsf{sup}(a,f):{\mathsf{W}}_{x:A}B$

For the next two rules abbreviate

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A⊢B\mathsf{type}$$\mathrm{\Gamma },w:W⊢C\mathsf{type}$$\mathrm{\Gamma }⊢h:{\mathsf{Step}}_C$$\mathrm{\Gamma }⊢t:W$

$\mathrm{\Gamma }⊢{\mathsf{E}}_C(h,t):C[t/w]$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A⊢B\mathsf{type}$$\mathrm{\Gamma },w:W⊢C\mathsf{type}$$\mathrm{\Gamma }⊢h:{\mathsf{Step}}_C$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢f:B[a/x]\to W$

$\mathrm{\Gamma }⊢{\mathsf{E}}_C(h,\mathsf{sup}(a,f))\equiv haf(\lambda y.{\mathsf{E}}_C(h,fy)):C[\mathsf{sup}(a,f)/w]$

The extensional source card used for representation

The separate extensional source calculus in chapter 28 restores every direct presupposition of equality reflection:

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

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

Russell universes

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

$\mathrm{\Gamma }⊢{\mathcal{U}}_i\mathsf{type}$

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

$\mathrm{\Gamma }⊢{\mathcal{U}}_j:{\mathcal{U}}_i$

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

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

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$\mathrm{\Gamma }⊢B:{\mathcal{U}}_i$$\mathrm{\Gamma }⊢A\equiv B:{\mathcal{U}}_i$

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

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:A\mathsf{ctx}$$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$\mathrm{\Gamma },x:A⊢B:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢\prod _{x:A}B:{\mathcal{U}}_i$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:A\mathsf{ctx}$$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$\mathrm{\Gamma },x:A⊢B:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢\sum _{x:A}B:{\mathcal{U}}_i$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:A\mathsf{ctx}$$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$\mathrm{\Gamma },x:A⊢B:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢{\mathsf{W}}_{x:A}B:{\mathcal{U}}_i$

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

$\mathrm{\Gamma }⊢A+B:{\mathcal{U}}_i$

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

$\mathrm{\Gamma }⊢\mathbf{0}:{\mathcal{U}}_i$

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

$\mathrm{\Gamma }⊢\mathbf{1}:{\mathcal{U}}_i$

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

$\mathrm{\Gamma }⊢\mathbf{2}:{\mathcal{U}}_i$

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

$\mathrm{\Gamma }⊢\mathbb{N}:{\mathcal{U}}_i$

The optional cumulative-membership delta used by section 74.4 is

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$i\le j$

$\mathrm{\Gamma }⊢A:{\mathcal{U}}_j$

The optional strict lifting delta of definition 29.10 is

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

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_{i}A:{\mathcal{U}}_{i+1}$

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

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_{i}A\equiv A\mathsf{type}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\equiv A^{\prime }:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_{i}A\equiv {\mathsf{Lift}}_i{A}^{\prime }:{\mathcal{U}}_{i+1}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:A\mathsf{ctx}$$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$\mathrm{\Gamma },x:A⊢B:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_i(\prod _{x:A}B)\equiv \prod _{x:{\mathsf{Lift}}_{i}A}{\mathsf{Lift}}_{i}B:{\mathcal{U}}_{i+1}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:A\mathsf{ctx}$$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$\mathrm{\Gamma },x:A⊢B:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_i(\sum _{x:A}B)\equiv \sum _{x:{\mathsf{Lift}}_{i}A}{\mathsf{Lift}}_{i}B:{\mathcal{U}}_{i+1}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:A\mathsf{ctx}$$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$\mathrm{\Gamma },x:A⊢B:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_i({\mathsf{W}}_{x:A}B)\equiv {\mathsf{W}}_{x:{\mathsf{Lift}}_{i}A}{\mathsf{Lift}}_{i}B:{\mathcal{U}}_{i+1}$

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

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_i(A+B)\equiv {\mathsf{Lift}}_{i}A+{\mathsf{Lift}}_{i}B:{\mathcal{U}}_{i+1}$

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

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_i\mathbf{0}\equiv \mathbf{0}:{\mathcal{U}}_{i+1}$

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

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_i\mathbf{1}\equiv \mathbf{1}:{\mathcal{U}}_{i+1}$

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

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_i\mathbf{2}\equiv \mathbf{2}:{\mathcal{U}}_{i+1}$

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

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_i\mathbb{N}\equiv \mathbb{N}:{\mathcal{U}}_{i+1}$

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

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_i{\mathcal{U}}_j\equiv {\mathcal{U}}_j:{\mathcal{U}}_{i+1}$

In each dependent code, Lift-El and context conversion identify the lifted binder with the original one.

Tarski universes

The alternative presentation of definition 75.1 replaces U-El by decoding:

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

$\mathrm{\Gamma }⊢{\mathcal{U}}_i\mathsf{type}$

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

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

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢a:{\mathcal{U}}_i$$\mathrm{\Gamma }⊢a^{\prime }:{\mathcal{U}}_i$$\mathrm{\Gamma }⊢a\equiv a^{\prime }:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢\mathsf{El}(a)\equiv \mathsf{El}(a^{\prime })\mathsf{type}$

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

$\mathrm{\Gamma }⊢⌜{\mathcal{U}}_j⌝:{\mathcal{U}}_i$

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

$\mathrm{\Gamma }⊢\mathsf{El}(⌜{\mathcal{U}}_j⌝)\equiv {\mathcal{U}}_j\mathsf{type}$

Its dependent codes and their strict decodings are

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:\mathsf{El}(a)\mathsf{ctx}$$\mathrm{\Gamma }⊢a:{\mathcal{U}}_i$$\mathrm{\Gamma },x:\mathsf{El}(a)⊢b:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢⌜\mathrm{\Pi }⌝(a,x.b):{\mathcal{U}}_i$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:\mathsf{El}(a)\mathsf{ctx}$$\mathrm{\Gamma }⊢a:{\mathcal{U}}_i$$\mathrm{\Gamma },x:\mathsf{El}(a)⊢b:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢⌜\mathrm{\Sigma }⌝(a,x.b):{\mathcal{U}}_i$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:\mathsf{El}(a)\mathsf{ctx}$$\mathrm{\Gamma }⊢a:{\mathcal{U}}_i$$\mathrm{\Gamma },x:\mathsf{El}(a)⊢b:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢⌜\mathsf{W}⌝(a,x.b):{\mathcal{U}}_i$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:\mathsf{El}(a)\mathsf{ctx}$$\mathrm{\Gamma }⊢a:{\mathcal{U}}_i$$\mathrm{\Gamma },x:\mathsf{El}(a)⊢b:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢\mathsf{El}(⌜\mathrm{\Pi }⌝(a,x.b))\equiv \prod _{x:\mathsf{El}(a)}\mathsf{El}(b)\mathsf{type}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:\mathsf{El}(a)\mathsf{ctx}$$\mathrm{\Gamma }⊢a:{\mathcal{U}}_i$$\mathrm{\Gamma },x:\mathsf{El}(a)⊢b:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢\mathsf{El}(⌜\mathrm{\Sigma }⌝(a,x.b))\equiv \sum _{x:\mathsf{El}(a)}\mathsf{El}(b)\mathsf{type}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:\mathsf{El}(a)\mathsf{ctx}$$\mathrm{\Gamma }⊢a:{\mathcal{U}}_i$$\mathrm{\Gamma },x:\mathsf{El}(a)⊢b:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢\mathsf{El}(⌜\mathsf{W}⌝(a,x.b))\equiv {\mathsf{W}}_{x:\mathsf{El}(a)}\mathsf{El}(b)\mathsf{type}$

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

$\mathrm{\Gamma }⊢⌜+⌝(a,b):{\mathcal{U}}_i$

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

$\mathrm{\Gamma }⊢\mathsf{El}(⌜+⌝(a,b))\equiv \mathsf{El}(a)+\mathsf{El}(b)\mathsf{type}$

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

$\mathrm{\Gamma }⊢⌜\mathbf{0}⌝:{\mathcal{U}}_i$

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

$\mathrm{\Gamma }⊢⌜\mathbf{1}⌝:{\mathcal{U}}_i$

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

$\mathrm{\Gamma }⊢⌜\mathbf{2}⌝:{\mathcal{U}}_i$

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

$\mathrm{\Gamma }⊢⌜\mathbb{N}⌝:{\mathcal{U}}_i$

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

$\mathrm{\Gamma }⊢\mathsf{El}(⌜\mathbf{0}⌝)\equiv \mathbf{0}\mathsf{type}$

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

$\mathrm{\Gamma }⊢\mathsf{El}(⌜\mathbf{1}⌝)\equiv \mathbf{1}\mathsf{type}$

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

$\mathrm{\Gamma }⊢\mathsf{El}(⌜\mathbf{2}⌝)\equiv \mathbf{2}\mathsf{type}$

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

$\mathrm{\Gamma }⊢\mathsf{El}(⌜\mathbb{N}⌝)\equiv \mathbb{N}\mathsf{type}$

The representative congruence scheme is

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma },x:\mathsf{El}(a)\mathsf{ctx}$$\mathrm{\Gamma }⊢a:{\mathcal{U}}_i$$\mathrm{\Gamma },x:\mathsf{El}(a)⊢b:{\mathcal{U}}_i$$\mathrm{\Gamma },x:\mathsf{El}(a)⊢b^{\prime }:{\mathcal{U}}_i$$\mathrm{\Gamma },x:\mathsf{El}(a)⊢b\equiv b^{\prime }:{\mathcal{U}}_i$

$\mathrm{\Gamma }⊢⌜\mathrm{\Pi }⌝(a,x.b)\equiv ⌜\mathrm{\Pi }⌝(a,x.b^{\prime }):{\mathcal{U}}_i$

It applies to every classified argument of every code constructor, with TU-El-Eq and context conversion when a dependent domain changes.

The Hurkens interface

The separate ${\mathsf{U}}^{-}$ signature of definition 76.1 contains $$U_1,{\mathsf{El}}_1,{\mathrm{\Pi }}_1,{\mathrm{\Pi }}_2,{\lambda }_1,{\cdot }_1,{\lambda }_2,{\cdot }_2,u_0,{\mathsf{El}}_0,{\mathrm{\Pi }}_0,{\mathrm{\Pi }}_{01},{\lambda }_0,{\cdot }_0,{\lambda }_{01},{\cdot }_{01}.$$ Here $U_1$ is a type, ${\mathsf{El}}_1(A)$ is a type for $A:U_1$, $u_0:U_1$, $U_0:={\mathsf{El}}_1(u_0)$, and ${\mathsf{El}}_0(a)$ is a type for $a:U_0$. The four code formers are The operations have the full signatures The chapter’s strengthened judgmental presentation supplies exactly $$({\lambda }_{1}x.t){\cdot }_{1}a\equiv t[a/x],({\lambda }_{2}A.t){\cdot }_{2}B\equiv t[B/A].$$ Spiwack’s source instead states corresponding equality axioms and inserts transports. Neither ${\lambda }_0/{\cdot }_0$ nor ${\lambda }_{01}/{\cdot }_{01}$ has a beta equation. This card is not cumulative with either universe presentation above.

Identity types

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

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

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

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

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

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

When the optional strict lifting package and identity types are both present, add

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

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_i({\mathsf{Id}}_A(a,b))\equiv {\mathsf{Id}}_{{\mathsf{Lift}}_{i}A}(a,b):{\mathcal{U}}_{i+1}$

$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A,y:A,p:{\mathsf{Id}}_A(x,y)⊢C\mathsf{type}$$\mathrm{\Gamma },z:A⊢c:C[z/x,z/y,{\mathsf{refl}}_z/p]$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢b:A$$\mathrm{\Gamma }⊢q:{\mathsf{Id}}_A(a,b)$

$\mathrm{\Gamma }⊢\mathsf{J}(x.y.p.C;z.c;q):C[a/x,b/y,q/p]$

$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A,y:A,p:{\mathsf{Id}}_A(x,y)⊢C\mathsf{type}$$\mathrm{\Gamma },z:A⊢c:C[z/x,z/y,{\mathsf{refl}}_z/p]$$\mathrm{\Gamma }⊢a:A$

$\mathrm{\Gamma }⊢\mathsf{J}(x.y.p.C;z.c;{\mathsf{refl}}_a)\equiv c[a/z]:C[a/x,a/y,{\mathsf{refl}}_a/p]$

The chapter’s congruence instances use

$\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{Id}}_A(a,b)\equiv {\mathsf{Id}}_{A^{\prime }}(a^{\prime },b^{\prime })\mathsf{type}$

and, for $\mathrm{\Delta }:=\mathrm{\Gamma },x:A,y:A,p:{\mathsf{Id}}_A(x,y)$,

$\mathrm{\Gamma }⊢A\equiv A^{\prime }\mathsf{type}$$\mathrm{\Delta }⊢C\equiv C^{\prime }\mathsf{type}$$\mathrm{\Gamma },z:A⊢c\equiv c^{\prime }:C[z/x,z/y,{\mathsf{refl}}_z/p]$$\mathrm{\Gamma }⊢a\equiv a^{\prime }:A$$\mathrm{\Gamma }⊢b\equiv b^{\prime }:A$$\mathrm{\Gamma }⊢q\equiv q^{\prime }:{\mathsf{Id}}_A(a,b)$

$\mathrm{\Gamma }⊢\mathsf{J}(x.y.p.C;z.c;q)\equiv \mathsf{J}(x.y.p.C^{\prime };z.c^{\prime };q^{\prime }):C[a/x,b/y,q/p]$

Context conversion places the primed data in the displayed contexts.

The based rules derived using $\mathrm{\Sigma }$-types are

$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma },,y:A,,p:{\mathsf{Id}}_A(a,y)⊢C\mathsf{type}$$\mathrm{\Gamma }⊢c:C[a/y,{\mathsf{refl}}_a/p]$$\mathrm{\Gamma }⊢q:{\mathsf{Id}}_A(a,b)$

$\mathrm{\Gamma }⊢{\mathsf{J}}^{\prime }(y.p.C;c;q):C[b/y,q/p]$

$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma },,y:A,,p:{\mathsf{Id}}_A(a,y)⊢C\mathsf{type}$$\mathrm{\Gamma }⊢c:C[a/y,{\mathsf{refl}}_a/p]$

$\mathrm{\Gamma }⊢{\mathsf{J}}^{\prime }(y.p.C;c;{\mathsf{refl}}_a)\equiv c:C[a/y,{\mathsf{refl}}_a/p]$