Homotopy Type Theory Sierpinski space > history (Rev #5)

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 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(ab)a:\Sigma, b:\Sigma \vdash \pi(a,b):isProp(a \leq b)

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

  • a family of dependent terms

    a:Σρ(a):aaa:\Sigma \vdash \rho(a):a \leq a

    representing the reflexive property of \leq.

  • a family of dependent terms

    a:Σ,b:Σ,c:Στ(a,b,c):(ab)×(bc)(ac)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):(ab)×(ba)(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):aa:\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):aaba:\Sigma, b:\Sigma \vdash i_a(a, b):a \leq a \vee b
    a:Σ,b:Σi b(a,b):baba:\Sigma, b:\Sigma \vdash i_b(a, b):b \leq a \vee b
    a:Σ,b:Σ,()():Σ×ΣΣ,i a(a,b):aab,i b(a,b):babi(a,b):(ab)(ab)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):aa:\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):abaa:\Sigma, b:\Sigma \vdash p_a(a, b):a \wedge b \leq a
    a:Σ,b:Σp b(a,b):abba:\Sigma, b:\Sigma \vdash p_b(a, b):a \wedge b \leq b
    a:Σ,b:Σ,()():Σ×ΣΣ,p a(a,b):aab,p b(a,b):babp(a,b):(ab)(ab)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.

See also

References

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