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

Showing changes from revision #14 to #15: Added | Removed | Changed

## 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$
• A left unitor
$\lambda:\prod_{(a:A)} \mu(e,a)=a$
• A right unitor
$\rho:\prod_{(a:A)} \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 circle. See Lemma 8.5.8 of the HoTT book.

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.

• An A3-space $A$ is an H-space with an equality $\mu(\mu(a, b),c)=\mu(a,\mu(b,c))$ for every $a:A$, $b:A$, $c:A$ representing associativity up to homotopy.

• A unital magma is a 0-truncated H-space.