Homotopy Type Theory UMyn8W7b (Rev #33)

Real numbers

Lattices and σ\sigma-frames

A lattice is a set LL with terms :L\bot:L, :L\top:L and functions :L\wedge:L, :L\vee:L, such that

  • (L,,)(L, \top, \wedge) and (L,,)(L, \bot, \vee) are commutative monoids

  • \wedge and \vee are idempotent: for all terms a:La:L, aa=aa \wedge a = a and aa=aa \vee a = a

  • for all a:La:L and b:Lb:L, a(ab)=aa \wedge (a \vee b) = a and a(ab)=aa \vee (a \wedge b) = a

A σ\sigma-complete lattice is a lattice LL with a function

n:()(n):(L)L\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to L) \to L

such that

  • for all n:n:\mathbb{N} and s:Ls:\mathbb{N} \to L,
s(n)( n:s(n))=s(n)s(n) \wedge \left(\Vee_{n:\mathbb{N}} s(n)\right) = s(n)
  • for all x:Lx:L and s:Ls:\mathbb{N} \to L, if s(n)x=s(n)s(n) \wedge x = s(n) for all n:n:\mathbb{N}, then
(( n:s(n))x= n:s(n))\left(\left(\Vee_{n:\mathbb{N}} s(n)\right) \wedge x = \Vee_{n:\mathbb{N}} s(n)\right)

A σ\sigma-frame is a σ\sigma-complete lattice with a function 𝓉:(L×(L))L\mathcal{t}:(L \times (\mathbb{N} \to L)) \to \mathbb{N} \to L such that

  • for all x:Lx:L and s:Ls:\mathbb{N} \to L, 𝓉(x,s)(n)=xs(n)\mathcal{t}(x,s)(n) = x \wedge s(n)

  • for all x:Lx:L and s:Ls:\mathbb{N} \to L,

x( n:s(n))= n:t(x,s)(n)x \wedge \left(\Vee_{n:\mathbb{N}} s(n)\right) = \Vee_{n:\mathbb{N}} t(x,s)(n)

Sierpinski space

Sierpinski space Σ\Sigma is an initial σ\sigma-frame, and thus could be generated as a higher inductive type.

Revision on May 8, 2022 at 20:16:38 by Anonymous?. See the history of this page for a list of all contributions to it.