Showing changes from revision #8 to #9:
Added | Removed | Changed
Whenever editing is allowed on the nLab again, this article should be ported over there.
A precategory consists of the following.
A preset , 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 .
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 .
In homotopy type thoery, 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 . In set theory, if the preset is an -groupoid, there a notion of path space of objects and 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.
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.