$$\Gamma, i : \mathbb{I} \vdash A \;\; \mathrm{type} \quad \Gamma \vdash a : A[i \mapsto 0] \quad \Gamma \vdash b : A[i \mapsto 1] \over \Gamma \vdash \mathsf{Path} \; A \; a \; b \;\; \mathrm{type}$$

$$\Gamma, i : \mathbb{I} \vdash u : A \over \Gamma \vdash \langle i \rangle \; u : \mathsf{Path} \; A \; u[i \mapsto 0] \; u[i \mapsto 1]$$