Post #1816235

@MartinEscardo @dwarn Here's my account: https://martinescardo.github.io/TypeTopology/gist.ThereAreNoHigherSemilattices2.html My main take-away is the following observation. A loop space is trivial if it can be equipped with a binary operation ⋆ such that - it has an interchange law: (p ⋆ q) ∙ (r ⋆ s) ＝ (p ∙ r) ⋆ (q ∙ s); - it is idempotent, commutative and associative. Proving that an idempotent, commutative and associative binary operation on a pointed type induces such an operation ⋆ on its loop space is then quite tricky when it comes to commutativity and associativity. I elaborated David's argument as follows: first prove that ⋆ is commutative up to conjugation, then use idempotency to show that conjugation acts trivially, so that ⋆ really is commutative (without conjugation), and similarly (but slightly more involved) for associativity. The intellectual credit naturally lies with David, but hopefully my elaboration/account is helpful for others too!