Showing changes from revision #6 to #7:
Added | Removed | Changed
Whenever editing is allowed on the nLab again, this article should be ported over there.
A directed set or filtered (0,1)-precategory is a preorder or (0,1)-precategory $(P, \leq)$ with an element $\iota \in P$ and a function $(-)\oplus(-) \in P^{P \times P}$ such that
A codirected set or cofiltered (0,1)-precategory is a preorder or (0,1)-precategory $(P, \leq)$ with an element $\iota \in P$ and a function $(-)\otimes(-) \in P^{P \times P}$ such that
If the directed set or codirected set is a poset, then it is called a directed poset or codirected poset, or a filtered (0,1)-category or cofiltered (0,1)-category.
A directed type or filtered (0,1)-precategory is a preorder or (0,1)-precategory $(P, \leq)$ with
a term $\iota:P$
a function $(-)\oplus(-):P \times P \to P$
a family of dependent terms
A codirected type or cofiltered (0,1)-precategory is a preorder or (0,1)-precategory $(P, \leq)$ with
a term $\iota:P$
a function $(-)\otimes(-):P \times P \to P$
a family of dependent terms
If the directed type or codirected type is 0-truncated it is called a directed set or codirected set, and if the directed type or codirected type is a poset, then it is called a directed poset or codirected poset, or a filtered (0,1)-category or cofiltered (0,1)-category.
Last revised on June 9, 2022 at 21:38:18. See the history of this page for a list of all contributions to it.