[[!redirects directed set]] [[!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} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ## ### In set theory ### 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 $$\forall a \in P. \forall b \in P. (a \leq a \oplus b) \wedge (b \leq a \oplus b)$$ 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 $$\forall a \in P. \forall b \in P. (a \otimes b \leq a) \wedge (a \otimes b \leq b)$$ 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__. ### In homotopy type thoery ### 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: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:P$ * a function $(-)\otimes(-):P \times P \to P$ * 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__. ## Examples ## * The [[natural numbers]] $\mathbb{N}$ with addition $+$ and less than or equal to $\leq$ is a directed type. * The positive [[rational numbers]] $\mathbb{Q}_{+}$ with addition $+$ and less than or equal to $\leq$ is a directed type. * The negative [[rational numbers]] $\mathbb{Q}_{-}$ with addition $+$ and greater than or equal to $\geq$ is a directed type. * The positive [[integers]] $\mathbb{Z}_{+}$ with multiplicaiton $\cdot$ and less than or equal to $\leq$ is a directed type. ## See also ## * [[preorder]] * [[net]]