CCHM cubical type theory

Contexts admit a dimension variable and a face restriction:

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

$\mathrm{\Gamma },i:\mathbb{I}\mathsf{ctx}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢\phi :\mathbb{F}$

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

Path formation and introduction are

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

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

$\mathrm{\Gamma },i:\mathbb{I}⊢A\mathsf{type}$$\mathrm{\Gamma },i:\mathbb{I}⊢t:A$

$\mathrm{\Gamma }⊢⟨i⟩t:{\mathsf{PathP}}_{i.A}(t[0/i],t[1/i])$

and composition has the headline rule

$\mathrm{\Gamma },i:\mathbb{I}⊢A\mathsf{type}$$\mathrm{\Gamma }⊢\phi :\mathbb{F}$$\mathrm{\Gamma },i:\mathbb{I},\phi ⊢u:A$$\mathrm{\Gamma }⊢a_0:A[0/i]$$\mathrm{\Gamma },\phi ⊢u[0/i]\equiv a_0:A[0/i]$

$\mathrm{\Gamma }⊢{\mathsf{comp}}^{i}A[\phi \mapsto u]a_0:A[1/i]$