Homotopy Type Theory
H-spaceoid > history (Rev #3, changes)
Showing changes from revision #2 to #3:
Added | Removed | Changed
Contents
Idea
The oidification of an H-space
Definition
An H-spaceoid 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 .
See also
Revision on June 7, 2022 at 21:24:43 by
Anonymous?.
See the history of this page for a list of all contributions to it.