Showing changes from revision #1 to #2:
Added | Removed | Changed
The oidification of an A3-space
A homotopy precategory consists of the following.
A type , whose elements are called objects. Typically is coerced to in order to write for .
For each , a type , 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 .
concrete homotopy precategory?
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)