# Homotopy Type Theory Sierpinski space > history (Rev #6, changes)

Showing changes from revision #5 to #6: Added | Removed | Changed

# Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

## Definition

TODO: …

### In set theory

The Sierpinski space  \mathbb{1}_\bot \Sigma , or also called the$\Sigma$set of open propositions , also is called defined as the initial object in thetype of open propositionscategory , is of defined as the partial $\sigma$-frames function classifier on the unit type?, or as the homotopy-initial $\sigma$-frame.

### As In a homotopy higher inductive-inductive type theory

The Sierpinski space $\Sigma$ , is also inductively called generated the bytype of open propositions, is defined as the homotopy-initial $\sigma$-frame.

• 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$

#### As a higher inductive-inductive type

and The thepartial orderSierpinski space type family$\Sigma$ is inductively generated by$\leq$ is simultaneously inductively generated by

• a term

a family of dependent terms

$\bot:\Sigma$
$a:\Sigma, b:\Sigma \vdash \pi(a,b):isProp(a \leq b)$

representing that each type $a \leq b$ is a proposition.

• a binary operation

a family of dependent terms

$(-)\vee(-):\Sigma \times \Sigma \to \Sigma$
$a:\Sigma \vdash \rho(a):a \leq a$

representing the reflexive property of $\leq$.

• a function

a family of dependent terms

$\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to \Sigma) \to \Sigma$
$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 term

a family of dependent terms

$\top:\Sigma$
$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 binary operation

a family of dependent terms

$(-)\wedge(-):\Sigma \times \Sigma \to \Sigma$
$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.

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.

## References

Revision on April 13, 2022 at 22:51:04 by Anonymous?. See the history of this page for a list of all contributions to it.