Eilenberg-Mac Lane Spaces in HoTT - Daniel Licata