Homotopy Type Theory omega-complete poset > history (Rev #1)

Contents

Definition

A ω\omega-complete poset or countably cocomplete (0,1)-category is a poset (P,)(P, \leq) with

  • a term :P\bot:P

  • a family of dependent terms

    a:Pt(a):aa:P \vdash t(a):\bot \leq a

    representing that \bot is initial in the poset.

  • a function

    n:()(n):(P)L\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to P) \to L
  • a family of dependent terms

    n:,s:Pi(n,s):s(n) n:s(n)n:\mathbb{N}, s:\mathbb{N} \to P \vdash i(n, s):s(n) \leq \Vee_{n:\mathbb{N}} s(n)
  • 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 that denumerable/countable joins exist in the poset.

See also

References

  • Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (abs:1610.09254)

Revision on March 12, 2022 at 00:51:38 by Anonymous?. See the history of this page for a list of all contributions to it.