Homotopy Type Theory H-space > history (Rev #8, changes)

Showing changes from revision #7 to #8: Added | ~~Removed~~ | ~~Chan~~ged

Idea

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

Definition

A H-Space consists of

A type $A$ ,
A basepoint $e:A$
A binary operation $\mu : A \to A \to A$
for every $a:A$ , equalities $\mu(e,a)=a$ and $\mu(a,e)=a$

Properties

Let $A$ be a connected? H-space. Then for every $a:A$ , the maps? $\mu(a,-),\mu(-,a):A \to A$ are equivalences.

Examples

There is a H-space structure on the~~There is a H-space structure on the circle. See Lemma 8.5.8 of the HoTT book. (TODO: Write out construction).~~
circle . See Lemma 8.5.8 of theHoTT 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? $A \to A$ has the structure of a H-space, with basepoint $id_A$ , operation function composition.~~

Proof. We define $\mu : S^1 \to S^1 \to S^1$ by circle induction:

\mu(base)\equiv id_{S^1}\qquad ap_{\mu}\equiv funext(h)

where $h : \prod_{x : S^1} x = x$ is defined in Lemma 6.4.2 of the HoTT book. We now need to show that $\mu(x,e)=mu(e,x)=x$ for every $x : S^1$ . Showing $\mu(e,x)=x$ 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? $A \to A$ has the structure of a H-space, with basepoint $id_A$ , operation function composition.

References

HoTT book

category: homotopy theory

Revision on January 19, 2019 at 15:46:09 by Ali Caglayan. See the history of this page for a list of all contributions to it.