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.