[[!redirects precategories]] * table of contents {:toc} ## Definition ## A 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 set $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 eagh $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$. ## Properties ## There are two notions of "sameness" for objects of a precategory. On one hand we have an [[isomorphism]] between objects $a$ and $b$ on the other hand we have equality of objects $a$ and $b$. There is a special kind of precategory called a [[category]] where these two notions of equality coincide and some very nice properties arise. ###Lemma 9.1.4 (idtoiso)### if $A$ is a precategory and $a,b:A$, then there is a map $$idtoiso : (a=b) \to (a \cong b)$$ *Proof.* By induction on identity, we may assume $a$ and $b$ are the same. But then we have $1_a:hom_A(a,a)$, which is clearly an isomorphism. $\square$ ## Examples ## See [[category]] ## See also ## [[Category theory]] [[category]] [[Rezk completion]] ## References ## [[HoTT Book]] category: category theory