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

Contents

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

Definition

In set theory

Sierpinski space Σ\Sigma, also called the set of open propositions, is defined as the initial object in the category of $\sigma$-frames.

In homotopy type theory

The Sierpinski space Σ\Sigma, also called the type of open propositions, is defined 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 14, 2022 at 02:51:04 by Anonymous?. See the history of this page for a list of all contributions to it.