# Homotopy Type Theory directed type > history (changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

# Contents

Whenever editing is allowed on the 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.