Showing changes from revision #14 to #15:
Added | Removed | Changed
< H-space
Sometimes we can equip a type with a certain structure, called a H-space, allowing us to derive some nice properties about the type or even construct fibrations
A H-Space consists of
Let be a connected? H-space. Then for every , the maps? are equivalences.
Proof. We define by circle induction:
where is defined in Lemma 6.4.2 of the HoTT book. We now need to show that for every . Showing is quite simple, the other way requires some more manipulation. Both of which are done in the book.
Every loop space is naturally a H-space with path concatenation as the operation. In fact every loop space is a group.
The type of maps? has the structure of a H-space, with basepoint , operation function composition.
An A3-space is an H-space with an equality for every , , representing associativity up to homotopy.
A unital magma is a 0-truncated H-space.
Classically, an H-space is a homotopy type equipped with the structure of a unital magma in the homotopy category (only).
Last revised on June 9, 2022 at 14:45:04. See the history of this page for a list of all contributions to it.