[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Boolean extensionality is the following set of rules: $$\mathrm{ext}_\mathbb{2}^{0, 0}:(0 =_\mathbb{2} 0) \simeq \mathbb{1} \qquad \mathrm{ext}_\mathbb{2}^{0, 1}:(0 =_\mathbb{2} 1) \simeq \mathbb{0}$$ $$\mathrm{ext}_\mathbb{2}^{1, 0}:(1 =_\mathbb{2} 0) \simeq \mathbb{0} \qquad \mathrm{ext}_\mathbb{2}^{1, 1}:(1 =_\mathbb{2} 1) \simeq \mathbb{1}$$ Natural numbers extensionality is the following set of rules: $$\mathrm{ext}_\mathbb{N}:\prod_{m:\mathbb{N}} \prod_{n:\mathbb{N}} (m =_\mathbb{N} n) \simeq (\mathrm{Eq}_\mathbb{N}(m, n) =_\mathbb{2} 1)$$ A graph is a type $V$ with a function $E:V \times V \to \mathbb{2}$. Now we need to define finite types... Binomial types $$\left(\begin{array}{c}A \\ B\end{array}\right) \coloneqq \sum_{f:A \to \mathbb{2}} \left[B \simeq \sum_{a:A} f(a) =_\mathbb{2} 1\right]$$ category: redirected to nlab