Jakub Opršal

@dwarn There many more varieties of topological algebras that have that property. Universal algebra later established a condition SD(∧), i.e., varieties with *meet semidistributive congruence lattices*, that precisely describes those varieties. Essentially, Taylor techniques show that any equation, that is satified by the algebra, has to be satisfied by its homotopy groups. There are no non-trivial models for an SD(∧) variety in groups.

@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.

@dwarn I was wondering whether your setting might be different, and whether that actually matters. I think there might be quite a low-level proof that should work always. I wanted to formalise some of these statements myself. Maybe a project for the summer.