Cartesian cubical core

The interval is cartesian: in addition to $0,1:\mathbb{I}$, a dimension variable may be weakened, contracted, or exchanged. It has no primitive reversal or connection. Cofibrations and their principal truth rules are:

$\mathrm{\Gamma }⊢r:\mathbb{I}$$\mathrm{\Gamma }⊢s:\mathbb{I}$

$\mathrm{\Gamma }⊢r=s\mathsf{cof}$

$\mathrm{\Gamma }⊢\phi \mathsf{cof}$$\mathrm{\Gamma }⊢\psi \mathsf{cof}$

$\mathrm{\Gamma }⊢\phi \vee \psi \mathsf{cof}$

$\mathrm{\Gamma },i:\mathbb{I}⊢\phi \mathsf{cof}$

$\mathrm{\Gamma }⊢\mathrm{\forall }i.\phi \mathsf{cof}$

$\mathrm{\Gamma }⊢r=s\mathsf{true}$

$\mathrm{\Gamma }⊢r\equiv s:\mathbb{I}$

$\mathrm{\Gamma }⊢0=1\mathsf{true}$$\mathrm{\Gamma }⊢A\mathsf{type}$

$\mathrm{\Gamma }⊢\mathsf{abort}:A$

The ordinary introduction rules for $\vee$ and $\mathrm{\forall }$, the hypothesis rule in $\mathrm{\Gamma },\phi$, proof-irrelevant congruence, case splitting with an agreement premise on overlaps, and substitution closure complete the cofibration calculus.

Every type has coercion and homogeneous composition:

$\mathrm{\Gamma },i:\mathbb{I}⊢A\mathsf{type}$$\mathrm{\Gamma }⊢r:\mathbb{I}$$\mathrm{\Gamma }⊢s:\mathbb{I}$$\mathrm{\Gamma }⊢a:A[r/i]$

$\mathrm{\Gamma }⊢{\mathsf{coe}}_{i.A}^{r\to s}(a):A[s/i]$

$\mathrm{\Gamma }⊢r\equiv s:\mathbb{I}$$\mathrm{\Gamma }⊢a:A[r/i]$

$\mathrm{\Gamma }⊢{\mathsf{coe}}_{i.A}^{r\to s}(a)\equiv a:A[s/i]$

$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢r:\mathbb{I}$$\mathrm{\Gamma }⊢s:\mathbb{I}$$\mathrm{\Gamma }⊢\phi \mathsf{cof}$$\mathrm{\Gamma },\phi ,i:\mathbb{I}⊢t:A$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma },\phi ⊢t[r/i]\equiv a:A$

$\mathrm{\Gamma }⊢{\mathsf{hcom}}_A^{r\to s}[\phi \mapsto i.t](a):A$

$\mathrm{\Gamma }⊢r\equiv s:\mathbb{I}$

$\mathrm{\Gamma }⊢{\mathsf{hcom}}_A^{r\to s}[\phi \mapsto i.t](a)\equiv a:A$

$\mathrm{\Gamma }⊢\phi \mathsf{true}$

$\mathrm{\Gamma }⊢{\mathsf{hcom}}_A^{r\to s}[\phi \mapsto i.t](a)\equiv t[s/i]:A$

All typing premises of hcom are presupposed in its two equations. Heterogeneous composition is derived by coercing the cap and each tube face to the target fiber before applying $\mathsf{hcom}$.

For $r:\mathbb{I}$, $A$ and $e:A\simeq B$ under $r=0$, and total $B$, the V-type rules are those of definition 81.22: formation ${\mathsf{V}}_r(A,B,e)$, compatible introduction ${\mathsf{Vin}}_r(a,b)$, and elimination ${\mathsf{Vout}}_r(v):B$. Their endpoint equations identify $\mathsf{V}$ with $A$ at $r=0$ and $B$ at $r=1$; moreover $${\mathsf{Vout}}_r({\mathsf{Vin}}_r(a,b))\equiv b,v\equiv {\mathsf{Vin}}_r(v,{\mathsf{Vout}}_r(v)).$$ Closure of the Kan universe under V and the mutually recursive Kan clauses for its codes are part of the exact semantic signature imported in theorem 81.29; this appendix does not infer an omitted clause from an executable example.