Homotopy Type Theory
omega-complete poset > history (changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
<omega-complete poset
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)
Last revised on June 9, 2022 at 23:16:03.
See the history of this page for a list of all contributions to it.