Homotopy Type Theory H-precategory > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Contents

Definition

A homotopy precategory $A$ consists of the following.

• A type $A_0$, whose elements are called objects. Typically $A$ is coerced to $A_0$ in order to write $x:A$ for $x:A_0$.

• For each $a,b:A$, a type $hom_A(a,b)$, whose elements are called arrows or morphisms.

• For each $a:A$, a morphism $1_a:hom_A(a,a)$, called the identity morphism.

• For each $a,b,c:A$, a function

  $$hom_A(b,c) \to hom_A(a,b) \to hom_A(a,c)$$

  called composition, and denoted infix by $g \mapsto f \mapsto g \circ f$, or sometimes $gf$.

• For each $a,b:A$ and $f:hom_A(a,b)$, we have $f=1_b \circ f$ and $f=f\circ 1_a$.

• For each $a,b,c,d:A$,

  $$f:hom_A(a,b),\ g:hom_A(b,c),\ h:hom_A(c,d)$$

  we have $h\circ (g\circ f)=(h\circ g)\circ f$.

See also

• quiver

• H-spaceoid

• A3-space

• concrete homotopy precategory?

• precategory

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)