[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Shapes as types, to define extension types... $\underset{x:A}\mathcal{U} B(x), \underset{x:A}\mathrm{El} B(x)$ Univalence as Rezk completion... category: redirected to nlab