Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Start of Eilenberg-MacLane space article.
Naming of the constructors is not really ideal, but I don’t like the ones in the original paper. The recursion principle is there it may need some more explaining. I have neglected the induction principle for now.
Also I have made an arbitary group, yet the construction of higher EM-spaces require it to be abelian. Given the definition of the higher EM-spaces I don’t see what is stopping it from being non-abelian. I would guess that would have as the abelianisation of . Which may be interesting.
Yes, if you write down the construction of “” for nonabelian , then you should end up with when . Given the construction , this should be a special case of the Hurewicz theorem.
@Mike Do you know if anybody has written down a proof of Hurewicz in HoTT yet? Even if it’s on an evelope?
I don’t think so.
1 to 4 of 4