[[!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: $$\mathrm{Fin}(n) \coloneqq \sum_{x:\mathbb{N}} x \lt n$$ category: redirected to nlab