Homotopy Type Theory directed type > history (Rev #2)

Contents

Definition

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

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

  • a family of dependent terms

    a:P,b:Pd(a,b): c:P(ac)×(bc)a:P, b:P \vdash d(a, b):\Vert \sum_{c:P} (a \leq c) \times (b \leq c) \Vert

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

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

  • a family of dependent terms

    a:P,b:Pd(a,b): c:P(ca)×(cb)a:P, b:P \vdash d(a, b):\Vert \sum_{c:P} (c \leq a) \times (c \leq b) \Vert

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

Revision on March 11, 2022 at 09:17:25 by Anonymous?. See the history of this page for a list of all contributions to it.