[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Shapes as types, to define extension types... Idea: the interval as the terminal object with two elements... Formation rules for the interval type: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{I} \; \mathrm{type}}$$ Introduction rules for the interval type: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{I}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathbb{I}}$$ Elimination rules for the interval type: for every other type $A$ with terms $x:A$ and $y:A$, there is a function $x:A \to \mathbb{I}$ such that $x = 0$ and $y = 1$. category: redirected to nlab