Showing changes from revision #6 to #7:
Added | Removed | Changed
Whenever editing is allowed on the nLab again, this article should be ported over there.
A precategory consists of the following.
An A preset -groupoid , whose elements are called objects. Typically , whose is elements coerced are to called objects. Typically is in coerced order to write in for order to write for .
For each , a 0-truncated set-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 .
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 .
There In homotopy type thoery, there are two notions of “sameness” for objects of a precategory. On one hand we have anisomorphism 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.
Category theory category Rezk completion