# Contents

## Definition

TODO: …

The Sierpinski space $\mathbb{1}_\bot$ or $\Sigma$, also called the type of open propositions, is defined as the partial function classifier on the unit type?, or as the homotopy-initial $\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.