A type , whose elements are called objects. Typically is coerced to in order to write for .
For each , a set , whose elements are called arrows or morphisms.
For each , a morphism , called the identity morphism.
For each , a function
called composition, and denoted infix by , or sometimes .
For each and , we have and .
For eagh ,
we have .
A precategory consists of the following.
An -groupoid , whose elements are called objects. Typically is coerced to in order to write for .
For each , a 0-truncated -groupoid , whose elements are called arrows or morphisms.
For each , a morphism , called the identity morphism.
For each , a function
called composition, and denoted infix by , or sometimes .
For each and , we have and .
For each ,
we have .
In homotopy type theory
A precategory consists of the following.
A type , whose elements are called objects. Typically is coerced to in order to write for .
For each , a set , whose elements are called arrows or morphisms.
For each , a morphism , called the identity morphism.
For each , a function
called composition, and denoted infix by , or sometimes .
For each and , we have and .
For each ,
we have .
Properties
There are two notions of “sameness” for objects of a precategory. On one hand we have an isomorphism between objects and on the other hand we have equality of objects and .
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 is a precategory and , then there is a map
Proof. By induction on identity, we may assume and are the same. But then we have , which is clearly an isomorphism.