#Contents# * table of contents {:toc} ## Definition ## The __Sierpinski space__ $1_\bot$ or $\Sigma$ is defined as the [[partial function classifier]] on the [[unit type]], or as the homotopy-initial [[sigma-frame|$\sigma$-frame]]. ### As a higher inductive-inductive type ### The __Sierpinski space__ $\Sigma$ is inductively generated by * a term $\bot:\Sigma$ * a binary operation $(-)\vee(-):\Sigma \times \Sigma \to \Sigma$ * a function $\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to \Sigma) \to \Sigma$ * a term $\top:\Sigma$ * a binary operation $(-)\wedge(-):\Sigma \times \Sigma \to \Sigma$ and the [[partial order]] [[type family]] $\leq$ is simultaneously inductively generated by * a family of dependent terms $$a:\Sigma, b:\Sigma \vdash \pi(a,b):isProp(a \leq b)$$ representing that each type $a \leq b$ is a [[proposition]]. * a family of dependent terms $$a:\Sigma \vdash \rho(a):a \leq a$$ representing the reflexive property of $\leq$. * a family of dependent terms $$a:\Sigma, b:\Sigma, c:\Sigma \vdash \tau(a, b, c):(a \leq b) \times (b \leq c) \to (a \leq c)$$ representing the transitive property of $\leq$. * a family of dependent terms $$a:\Sigma, b:\Sigma \vdash \sigma(a, b):(a \leq b) \times (b \leq a) \to (a = b)$$ representing the anti-symmetric property of $\leq$. * a family of dependent terms $$a:\Sigma \vdash t(a):\bot \leq a$$ representing that $\bot$ is initial in the poset. * three families of dependent terms $$a:\Sigma, b:\Sigma \vdash i_a(a, b):a \leq a \vee b$$ $$a:\Sigma, b:\Sigma \vdash i_b(a, b):b \leq a \vee b$$ $$a:\Sigma, b:\Sigma, (-)\oplus(-):\Sigma \times \Sigma \to \Sigma, i_a(a, b):a \leq a \oplus b, i_b(a, b):b \leq a \oplus b \vdash i(a,b):(a \vee b) \leq (a \oplus b)$$ representing that $\vee$ is a coproduct in the poset. * two families of dependent terms $$n:\mathbb{N}, s:\mathbb{N} \to \Sigma \vdash i(n, s):s(n) \leq \Vee_{n:\mathbb{N}} s(n)$$ $$x:\Sigma, s:\mathbb{N} \to \Sigma \vdash i(s, x):\prod_{n:\mathbb{N}}(s(n) \leq x) \to \left(\Vee_{n:\mathbb{N}} s(n) \leq x\right)$$ representing that $\Vee$ is a denumerable/countable coproduct in the poset. * a family of dependent terms $$a:\Sigma \vdash t(a):a \leq \top$$ representing that $\top$ is terminal in the poset. * three families of dependent terms $$a:\Sigma, b:\Sigma \vdash p_a(a, b):a \wedge b \leq a$$ $$a:\Sigma, b:\Sigma \vdash p_b(a, b):a \wedge b \leq b$$ $$a:\Sigma, b:\Sigma, (-)\otimes(-):\Sigma \times \Sigma \to \Sigma, p_a(a, b):a \leq a \otimes b, p_b(a, b):b \leq a \otimes b \vdash p(a,b):(a \otimes b) \leq (a \wedge b)$$ representing that $\wedge$ is a product in the poset. * a family of dependent terms $$x:\Sigma, s:\mathbb{N} \to \Sigma \vdash i(s, x):\left(\prod_{n:\mathbb{N}}(s(n) \leq x)\right) \to \left(\Vee_{n:\mathbb{N}} s(n) \leq x\right)$$ representing the countably infinitary distributive property. ## See also ## * [[partial function classifier]] * [[sigma-frame]] * [[Dedekind cut]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) * Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type ([abs:1610.09254](https://arxiv.org/abs/1610.09254))