[[!redirects precategories]] ## 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 precategory $A$ consists of the following. * A preset $A_0$, whose elements are called objects. Typically $A$ is coerced to $A_0$ in order to write $x \in A$ for $x \in A_0$. * For each $a,b \in A$, a set $hom_A(a,b)$, whose elements are called **arrows** or **morphisms**. * For each $a \in A$, a morphism $1_a \in hom_A(a,a)$, called the **identity morphism**. * For each $a,b,c \in 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 \in A$ and $f \in hom_A(a,b)$, we have $f=1_b \circ f$ and $f=f\circ 1_a$. * For each $a,b,c,d \in A$, $$f \in hom_A(a,b),\ g \in hom_A(b,c),\ h \in hom_A(c,d)$$ we have $h\circ (g\circ f)=(h\circ g)\circ f$. ### In homotopy type theory ### 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 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$. ## Properties ## In homotopy type thoery, there are two notions of "sameness" for objects of a precategory. On one hand we have an [[isomorphism in a precategory|isomorphism]] between objects $a$ and $b$ on the other hand we have equality of objects $a$ and $b$. In set theory, if the preset $A$ is an $\infty$-groupoid, there a notion of path space of objects $a$ and $b$ which corresponds to equality of objects in homotopy type thoery. However, for general presets there is only one notion of "sameness" for objects in a precategory. 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 ## * Every [[category]] is a precategory. * A [[dagger precategory]] is a precategory that is not a category. ## See also ## * [[category]] * [[Rezk completion]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) category: category theory