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 it’s 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:

  • base:K(G,1)base : K(G,1)
  • loop:G(base=base)loop : G \to (base = base)
  • id:loop(e)=refl baseid : loop(e) = refl_{base}
  • comp: (x,y:G)loop(xy)=loop(y)loop(x)comp : \prod_{(x,y:G)} loop(x \cdot y) = loop(y) \circ loop(x)

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:

  • x,y:K(G,1) p,q:x=y r,s:p=qr=s\displaystyle \prod_{x,y:K(G,1)} \prod_{p,q:x=y} \prod_{r,s:p=q} r = s

Recursion principle

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

  • a point c:Cc : C
  • a family of loops l:G(c=c)l : G \to (c = c)
  • a path l(e)=idl(e)=id
  • a path l(xy)=l(y)l(x)l(x \cdot y) = l(y) \circ l(x)
  • a proof that CC is a 1-type.

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:

  • a proof that CC is a 1-type
  • a point c:Cc : C
  • a group homomorphism from GG to Ω(C,c)\Omega(C,c)


See also


category: homotopy theory

Last revised on January 19, 2019 at 13:39:40. See the history of this page for a list of all contributions to it.