Post #1816240

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