Showing changes from revision #3 to #4:
Added | Removed | Changed
Idea
Let be an abelian group, and a natural number?. The Eilenberg-MacLane space is the unique space that has and its other homotopy groups? trivial.
These spaces are a basic tool in classical algebraic topology, they can be used to define cohomology.
Definition
Let be an group, the Eilenberg-MacLane space , the higher inductive 1-type with the following constructors:
is a point of , is a function that constructs a path from to for each element of . says the path constructed from the identity element is the trivial loop. Finally, 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 for some type , it suffices to give
a point
a family of loops
a path
a path
a proof that is a 1-type.
Then satisfies the equations
It should be noted that the above can be compressed, to specify a function , it suffices to give: