Homotopy Type Theory
Sierpinski space > history (Rev #4, changes)
Showing changes from revision #3 to #4:
Added | Removed | Changed
Contents
Definition
The TODO: … 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 .
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 ⋁ n : ℕ ( − ) ( n ) : ( ℕ → Σ ) → Σ \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 : Σ , b : Σ ⊢ π ( a , b ) : isProp ( a ≤ b ) a:\Sigma, b:\Sigma \vdash \pi(a,b):isProp(a \leq b)
representing that each type a ≤ b a \leq b is a proposition .
a family of dependent terms
a : Σ ⊢ ρ ( a ) : a ≤ a a:\Sigma \vdash \rho(a):a \leq a
representing the reflexive property of ≤ \leq .
a family of dependent terms
a : Σ , b : Σ , c : Σ ⊢ τ ( a , b , c ) : ( a ≤ b ) × ( b ≤ c ) → ( a ≤ c ) 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 : Σ , b : Σ ⊢ σ ( a , b ) : ( a ≤ b ) × ( b ≤ a ) → ( a = b ) 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 : Σ ⊢ t ( a ) : ⊥ ≤ a a:\Sigma \vdash t(a):\bot \leq a
representing that ⊥ \bot is initial in the poset.
three families of dependent terms
a : Σ , b : Σ ⊢ i a ( a , b ) : a ≤ a ∨ b a:\Sigma, b:\Sigma \vdash i_a(a, b):a \leq a \vee b a : Σ , b : Σ ⊢ i b ( a , b ) : b ≤ a ∨ b a:\Sigma, b:\Sigma \vdash i_b(a, b):b \leq a \vee b a : Σ , b : Σ , ( − ) ⊕ ( − ) : Σ × Σ → Σ , i a ( a , b ) : a ≤ a ⊕ b , i b ( a , b ) : b ≤ a ⊕ b ⊢ i ( a , b ) : ( a ∨ b ) ≤ ( a ⊕ 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 : ℕ , s : ℕ → Σ ⊢ i ( n , s ) : s ( n ) ≤ ⋁ n : ℕ s ( n ) n:\mathbb{N}, s:\mathbb{N} \to \Sigma \vdash i(n, s):s(n) \leq \Vee_{n:\mathbb{N}} s(n) x : Σ , s : ℕ → Σ ⊢ i ( s , x ) : ∏ n : ℕ ( s ( n ) ≤ x ) → ( ⋁ n : ℕ s ( n ) ≤ x ) 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 : Σ ⊢ t ( a ) : a ≤ ⊤ a:\Sigma \vdash t(a):a \leq \top
representing that ⊤ \top is terminal in the poset.
three families of dependent terms
a : Σ , b : Σ ⊢ p a ( a , b ) : a ∧ b ≤ a a:\Sigma, b:\Sigma \vdash p_a(a, b):a \wedge b \leq a a : Σ , b : Σ ⊢ p b ( a , b ) : a ∧ b ≤ b a:\Sigma, b:\Sigma \vdash p_b(a, b):a \wedge b \leq b a : Σ , b : Σ , ( − ) ⊗ ( − ) : Σ × Σ → Σ , p a ( a , b ) : a ≤ a ⊗ b , p b ( a , b ) : b ≤ a ⊗ b ⊢ p ( a , b ) : ( a ⊗ b ) ≤ ( a ∧ 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 : Σ , s : ℕ → Σ ⊢ i ( s , x ) : ( ∏ n : ℕ ( s ( n ) ≤ x ) ) → ( ⋁ n : ℕ s ( n ) ≤ x ) 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.
Properties
The Sierpinski space is homotopy-equivalent to the type of semidecidable propositions in a universe 𝒰 \mathcal{U} .
Σ ≅ ∑ P : 𝒰 isProp ( P ) × isSemidecidable ( P ) \Sigma \cong \sum_{P:\mathcal{U}} isProp(P) \times isSemidecidable(P)
See also
References
Revision on March 13, 2022 at 00:25:03 by
Anonymous? .
See the history of this page for a list of all contributions to it.