[[!redirects filtered (0,1)-precategory]] [[!redirects codirected type]] [[!redirects cofiltered (0,1)-precategory]] [[!redirects directed poset]] [[!redirects filtered (0,1)-category]] [[!redirects codirected poset]] [[!redirects cofiltered (0,1)-category]] #Contents# * table of contents {:toc} ## 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 of dependent terms $$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, \leq)$ with * a term $\iota:\Vert P \Vert$ * a family of dependent terms $$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 ## * [[preorder]] * [[net]]