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Σ\Sigmaset 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 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

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:Σ,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 binary operation

    a family of dependent terms

    ()():Σ×ΣΣ(-)\vee(-):\Sigma \times \Sigma \to \Sigma
    a:Σρ(a):aaa:\Sigma \vdash \rho(a):a \leq a

    representing the reflexive property of \leq.

  • a function

    a family of dependent terms

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

    a family of dependent terms

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

    a family of dependent terms

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

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:51:04 by Anonymous?. See the history of this page for a list of all contributions to it.