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 with an element and a function such that
A codirected set or cofiltered (0,1)-precategory is a preorder or (0,1)-precategory with an element and a function 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 with
a term
a function
a family of dependent terms
A codirected type or cofiltered (0,1)-precategory is a preorder or (0,1)-precategory with
a term
a function
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.