Post #908431

2026-02-18 11:59 UTC

A HoTT exercise: let \( A \) be a type with a binary operation \( * : A \to A \to A \). Suppose that \( * \) is associative, commutative, and idempotent, in the sense that \( \Pi_{a\, b\, c : A} a * (b * c) = (a * b) * c \), \( \Pi_{a\, b : A} a * b = b * a \) and \( \Pi_{a : A} a * a = a \). Show that \( A \) is an hset (and hence a semilattice in the ordinary sense).

Replies (4)

@dwarn@mathstodon.xyz 2026-02-18 15:48

A bunch of cool results on idempotents in a homotopical setting can be found in e.g. Kerodon, but the one above seems to have gone unnoticed. I gave a proof last year in response to a question from Georg Lehner at https://mathoverflow.net/q/496917 . Yesterday I took the time to formalise it in Agda: https://dwarn.se/agda/Idem.html . A weaker result appears in recent papers of Lehner and Antieau (Theorem 5.6 of https://arxiv.org/pdf/2507.00221 and https://arxiv.org/pdf/2508.13106 ).

Open ##1816211
@ToucanIan@mathstodon.xyz 2026-02-19 19:31

@dwarn I have so far failed to come up with an alternative proof showing that there is an Id-collapsible map on the type. Now that I see your solution as a formalization of a homotopical proof maybe thinking about loop spaces is essential.

Open ##1816223
@MartinEscardo@mathstodon.xyz 2026-02-22 17:48

@dwarn Conjecture. Associativity is not needed to reach the same conclusion.

Open ##1816224
@MartinEscardo@mathstodon.xyz 2026-02-23 21:15

Paraphrasing @dwarn , "there are no higher semi-lattices". I found this rather surprising and interesting, and so I wanted to fully understand it. Here is my elaboration of David's Agda file, in which I add some diagrams and some explanation in English prose, and rename some things that I hope are correct and what David intended. https://martinescardo.github.io/TypeTopology/gist.ThereAreNoHigherSemilattices.html If you wondered about David's result, this may help. I had to spend a couple of hours this evening to understand it, and the above link is the result of my underdstanding.

Open ##1816228