Homotopy Type Theory
Eilenberg-MacLane space

Idea

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 it’s other homotopy groups trivial.

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

Definition

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:

Properties

See also

References

category: homotopy theory