[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Type theory (dependent function types, dependent sum types, identity types, function extensionality) -> Predicate logic -> Set theory -> Number theory We could replace the natural numbers with the directed circle... $\overrightarrow{S^1}$ generated by $\mathrm{base}:\overrightarrow{S^1}$ and $\mathrm{loop}:\mathrm{hom}(\mathrm{base}, \mathrm{base})$ category: redirected to nlab