[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Shapes as types, to define extension types... \section{Identity types} What are the uniqueness rules for identity types? the J rule is the center of contraction. category: redirected to nlab