Homotopy Type Theory
omega-complete poset > history (Rev #1)
Contents
Definition
A -complete poset or countably cocomplete (0,1)-category is a poset with
-
a term
-
a family of dependent terms
representing that is initial in the poset.
-
a function
-
a family of dependent terms
-
a family of dependent terms
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 05:51:38 by
Anonymous?.
See the history of this page for a list of all contributions to it.