Homotopy Type Theory directed type > history (Rev #6, changes)

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

Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

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

In set theory

  • a term ι:P\iota:P

  • a function ()():P×PP(-)\oplus(-):P \times P \to P

  • a family of dependent terms

    a:P,b:Pd(a,b):(aab)×(bab)a:P, b:P \vdash d(a, b):(a \leq a \oplus b) \times (b \leq a \oplus b)

A directed set or filtered (0,1)-precategory is a preorder or (0,1)-precategory (P,)(P, \leq) with an element ιP\iota \in P and a function ()()P P×P(-)\oplus(-) \in P^{P \times P} such that

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

aP.bP.(aab)(bab)\forall a \in P. \forall b \in P. (a \leq a \oplus b) \wedge (b \leq a \oplus b)
  • a term ι:P\iota:P

  • a function ()():P×PP(-)\otimes(-):P \times P \to P

  • a family of dependent terms

    a:P,b:Pd(a,b):(aba)×(abb)a:P, b:P \vdash d(a, b):(a \otimes b \leq a) \times (a \otimes b \leq b)

A codirected set or cofiltered (0,1)-precategory is a preorder or (0,1)-precategory (P,)(P, \leq) with an element ιP\iota \in P and a function ()()P P×P(-)\otimes(-) \in P^{P \times P} such that

aP.bP.(aba)(abb)\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,)(P, \leq) with

  • a term ι:P\iota:P

  • a function ()():P×PP(-)\oplus(-):P \times P \to P

  • a family of dependent terms

    a:P,b:Pd(a,b):(aab)×(bab)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,)(P, \leq) with

  • a term ι:P\iota:P

  • a function ()():P×PP(-)\otimes(-):P \times P \to P

  • a family of dependent terms

    a:P,b:Pd(a,b):(aba)×(abb)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

Revision on April 14, 2022 at 05:45:22 by Anonymous?. See the history of this page for a list of all contributions to it.