Showing changes from revision #2 to #3: Added | Removed | Changed

Contents

Definition

A directed type or filtered (0,1)-precategory is a preorder or (0,1)-precategory $(P, \leq)$ with

• a term $\iota:\Vert P \Vert$

• a family function of dependent terms$(-)\oplus(-):P \times P \to P$

  $$a:P, b:P \vdash d(a, b):\Vert \sum_{c:P} (a \leq c) \times (b \leq c) \Vert$$

• a family of dependent terms

  $$a:P, b:P \vdash d(a, b):(a \leq a \oplus b) \times (b \leq a \oplus b)$$

A codirected type or cofiltered (0,1)-precategory is a preorder or (0,1)-precategory $(P, \leq)$ with

• a term $\iota:\Vert P \Vert$

• a family function of dependent terms$(-)\otimes(-):P \times P \to P$

  $$a:P, b:P \vdash d(a, b):\Vert \sum_{c:P} (c \leq a) \times (c \leq b) \Vert$$

• a family of dependent terms

  $$a:P, b:P \vdash d(a, b):(a \otimes b \leq a) \times (a \otimes b \leq b)$$

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.

See also

• preorder

• net