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

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



H-spaces Sometimes are we simply can types equip equipped with the structure of a magma (from classical Algebra). They are useful classically in constructing fibrations.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 ofH-Space consists of

  • A type AA,
  • A basepoint e:Ae:A
  • A binary operation μ:AAA\mu : A \to A \to A
  • for every a:Aa:A, equalities μ(e,a)=a\mu(e,a)=a and μ(a,e)=a\mu(a,e)=a


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


  • There is a H-space structure on the circle. See Lemma 8.5.8 of the HoTT book. (TODO: Write out construction).

  • 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? AAA \to A has the structure of a H-space, with basepoint id Aid_A, operation function composition.

See also

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).


HoTT book

category: homotopy theory

Revision on January 1, 2019 at 20:51:23 by Ali Caglayan. See the history of this page for a list of all contributions to it.