HoTT/HoTT-Agda — pull request #8 by ystael (2014-03-28 03:11:06+00:00)
Title: simple transcription of Eckmann-Hilton argument (book 2.1.6)

This is a straightforward transcription of the commutativity of composition in loop spaces from book theorem 2.1.6, because I didn't find it elsewhere in the library. I was unable to make it go through with the horizontal compositions that were already there in PathGroupoid (∙2 etc); in fact, I was unable to prove some simple lemmas about them for reasons that I don't understand yet.

If this theorem is already in the library somewhere that I missed, I apologize for the trouble.