[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Shapes as types, to define extension types... \section{Type theory} Identity types, dependent function types and function types, negative dependent pair types and negative pair types, equivalence types, and the interval type. \section{Free groups} Similar to how free monoids are lists, free groups are like lists but with the function type replaced with an equivalence type. \section{Ring theory} \subsection{Rings} $\mathbb{Z}$ \subsection{Invertible elements and group of invertible elements} $\mathbb{Z}^\times \coloneqq \{1, -1\}$ \subsection{Principal ideals} $\mathbb{N} \coloneqq \mathbb{Z}/\mathbb{Z}^\times$ \subsection{Regular elements and monoid of regular elements} $\mathrm{Reg}(\mathbb{Z}) \coloneqq \{x \in \mathbb{N} \vert x \neq 0\}$ \subsection{Regular principal ideals} $\mathbb{N}_+ \coloneqq \mathrm{Reg}(\mathbb{Z})/\mathbb{Z}^\times$ category: redirected to nlab