[[!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 dependent 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))$ $$\mathrm{tot}:\prod_{f:A \to B} \left(\prod_{x:A} C(x) \to D(f(x))\right) \to \left(\sum_{x:A} C(x) \to \sum_{x:A} D(f(x))\right)$$ category: redirected to nlab