[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Shapes as types, to define extension types... The univalent Tarski universe containing the type family $(A; x:A \vdash B(x))$ is a higher inductive-inductive type $(\mathrm{Univ}(A, B); x:\mathrm{Univ}(A, B) \vdash \mathrm{El}_{A, B}(x))$ generated by * a function $\eta:A \to \mathrm{Univ}(A, B)$ * a depeendent function $\delta:\prod_{x:A} \mathrm{El}_{A, B}(\eta(x)) \simeq B(x)$ * a dependent function $\upsilon:\prod_{x:\mathrm{Univ}(A, B)} \prod_{y:\mathrm{Univ}(A, B)} \mathrm{isEquiv}(\mathrm{transport}_{\mathrm{El}_{A, B}}(x,y))$ category: redirected to nlab