Post #1816228

2026-02-23 21:15 UTC

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.

Replies (4)

@antoinechambertloir@mathstodon.xyz 2026-02-23 21:17

@MartinEscardo @dwarn I like this, because it does not seem clear to me that once algebra is done within hott, every basic algebraic structure should a priori be a set. Maybe it's because higher groups are much more complicated than classical groups, but still.

Open ##1816229
@ToucanIan@mathstodon.xyz 2026-02-25 02:11

@MartinEscardo thanks for this! I tried and failed to do the very same thing. @dwarn

Open ##1816233
@de_Jong_Tom@mathstodon.xyz 2026-02-25 10:47

@MartinEscardo @dwarn To really understand it, I've been working on my own retelling. If I manage to complete it, I'll share it here. Thanks to both of you for sharing!

Open ##1816234
@jakub_et_al@mathstodon.xyz 2026-02-28 15:56

@MartinEscardo @dwarn This thread forced me to finally learn some agda, and try to write some proofs. I am attempting to reprove another statement from Taylor's paper. If a topological space admits a majority operation 𝑚 satisfying 𝑚(𝑥,𝑥,𝑦)=𝑚(𝑥,𝑦,𝑥)=𝑚(𝑦,𝑦,𝑥)=𝑥, then it is weakly-equivalent to a discrete set. Naturally, for homotopy types this would translate to three equations like 𝑒₁ : Π(𝑥,𝑦 : 𝐴) 𝑚(𝑦,𝑥,𝑥)=𝑥 𝑒₂ : Π(𝑥,𝑦 : 𝐴) 𝑚(𝑥,𝑦,𝑥)=𝑥 𝑒₃ : Π(𝑥,𝑦 : 𝐴) 𝑚(𝑥,𝑥,𝑦)=𝑥 I managed to make 𝑚 act idempotently on the loop space, but encountered an interesting problem: There are a few ways how to prove that 𝑚 is idempotent, and it is not clear which choice to make! I would need something like Π(𝑥:𝐴) 𝑒₁(𝑥,𝑥) = 𝑒₂(𝑥,𝑥). But maybe this is a consequence of what we mean when we write the above majority identities.

Open ##1816240