# Homotopy Type Theory H-space (Rev #6, changes)

Showing changes from revision #5 to #6: Added | Removed | Changed

# Contents

## Idea

H-spaces are simply types equipped with the structure of a magma (from classical Algebra). They are useful classically in constructing 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.

synthetic homotopy theory?Synthetic homotopy theory hopf fibration

### On the nlab

Classically, an H-space is a homotopy type equipped with the structure of a unital magma in the homotopy category (only).

## References

HoTT book

category: homotopy theory

Revision on October 8, 2018 at 17:24:11 by Ali Caglayan. See the history of this page for a list of all contributions to it.