Homotopy Type Theory
Eilenberg-MacLane space


Let GG be an abelian group?, and nn a natural number?. The Eilenberg-MacLane space K(G,n)K(G,n) is the unique space that has π n(K(G,n))G\pi_n(K(G,n))\cong G and its other homotopy groups trivial.

These spaces are a basic tool in classical algebraic topology, they can be used to define cohomology.


Let GG be an group, the Eilenberg-MacLane space K(G,1)K(G,1), the higher inductive 1-type with the following constructors:

basebase is a point of K(G,1)K(G,1), looploop is a function that constructs a path from basebase to basebase for each element of GG. idid says the path constructed from the identity element is the trivial loop. Finally, compcomp says that the path constructed from group multiplication of elements is the concatenation of paths.

It should be noted that this type is 1-truncated? which could be added as another constructor:

Recursion principle

To define a function f:K(G,1)Cf : K(G,1) \to C for some type CC, it suffices to give

Then ff satisfies the equations

f(base)cf(base) \equiv c
ap f(loop(x))=l(x)ap_{f} (loop(x))=l(x)

It should be noted that the above can be compressed, to specify a function f:K(G,1)Cf : K(G,1) \to C, it suffices to give:


See also


category: homotopy theory