HoTT additions

Book HoTT retains the intensional base and adds univalence and higher inductive types. The headline univalence rule is

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

$\mathrm{\Gamma }⊢{\mathsf{univalence}}_{A,B}:\mathsf{isEquiv}({\mathsf{idtoeqv}}_{A,B})$

with $\mathsf{idtoeqv}:{\mathsf{Id}}_{{\mathcal{U}}_i}(A,B)\to (A\simeq B)$.

For the circle, the formation and introduction rules are

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

$\mathrm{\Gamma }⊢{\mathbb{S}}^1\mathsf{type}$

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

$\mathrm{\Gamma }⊢\mathsf{base}:{\mathbb{S}}^1$

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

$\mathrm{\Gamma }⊢\mathsf{loop}:{\mathsf{Id}}_{{\mathbb{S}}^1}(\mathsf{base},\mathsf{base})$

Its dependent eliminator takes a point over $\mathsf{base}$ and a dependent path over $\mathsf{loop}$; point computation is judgmental and path computation is typal.