Set truncation in T_hott

For $\mathrm{\Gamma }⊢A\mathsf{type}$, set truncation has the following formation and point rules.

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

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

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

$\mathrm{\Gamma }⊢|a{|}_0:\Vert A{\Vert }_0$

$\mathrm{\Gamma }⊢u:\Vert A{\Vert }_0$$\mathrm{\Gamma }⊢v:\Vert A{\Vert }_0$$\mathrm{\Gamma }⊢p:{\mathsf{Id}}_{\Vert A{\Vert }_0}(u,v)$$\mathrm{\Gamma }⊢q:{\mathsf{Id}}_{\Vert A{\Vert }_0}(u,v)$

$\mathrm{\Gamma }⊢{\mathsf{sq}}_0(p,q):{\mathsf{Id}}_{{\mathsf{Id}}_{\Vert A{\Vert }_0}(u,v)}(p,q)$

The dependent eliminator takes a family $P$ over $\Vert A{\Vert }_0$, point data $d(a):P(|a{|}_0)$, and one dependent 2-path over every instance of ${\mathsf{sq}}_0$. It returns $\hat{d}:\prod _{x:\Vert A{\Vert }_0}P(x)$ with $\hat{d}(|a{|}_0)\equiv d(a)$. Path-constructor computation is propositional, in accordance with convention 68.4. For a set-valued family the dependent 2-path datum is unique, yielding lemma 68.36.