Skip to content

gist.MajoritiesOnlyActOnSets2

Tom de Jong, 16 & 18 March 2026.

We show that the proof given by Jakub Opršal in gist.MajoritiesOnlyActOnSets
factors through a simple lemma about loop spaces (see the module
Ω-trivial-criterion).


{-# OPTIONS --safe --without-K #-}

module gist.MajoritiesOnlyActOnSets2 where

open import Agda.Primitive renaming (Set to Type)


To be compatible with Jakub's file, we also build on Martín's file
gist.ThereAreNoHigherSemilattices, but with minimal imports.


open import gist.ThereAreNoHigherSemilattices
 using (_＝_ ; _∙_ ; refl ; sym ; ap ; ap₂ ; eq-congr)


We introduce a little additional boilerplate on top of our minimal imports.


_＝⟨_⟩_ : {X : Type} (x : X) {y z : X} → x ＝ y → y ＝ z → x ＝ z
_ ＝⟨ p ⟩ q = p ∙ q

_∎ : {X : Type} (x : X) → x ＝ x
_∎ _ = refl

infix  1 _∎
infixr 0 _＝⟨_⟩_

refl-left-neutral : {X : Type} {x y : X} (p : x ＝ y) → refl ∙ p ＝ p
refl-left-neutral refl = refl

refl-right-neutral : {X : Type} {x y : X} (p : x ＝ y) → p ∙ refl ＝ p
refl-right-neutral refl = refl

module _
        {A : Type}
        {a b : A}
       where

 conjugate-loop : a ＝ b → a ＝ a → b ＝ b
 conjugate-loop p = eq-congr p p

 conjugate-loop-refl : (p : a ＝ b) → conjugate-loop p refl ＝ refl
 conjugate-loop-refl refl = refl

 NB₁ : (p : a ＝ b) (q : a ＝ a) → conjugate-loop p q ＝ (sym p) ∙ q ∙ p
 NB₁ refl q = sym (refl-left-neutral (q ∙ refl) ∙ refl-right-neutral q)


We now present the lemma about trivial loop spaces.


module _
        (A : Type)
        (a₀ b₀ : A)
       where

 Ωᵃ : Type
 Ωᵃ = a₀ ＝ a₀

 Ωᵇ : Type
 Ωᵇ = b₀ ＝ b₀

 module Ω-trivial-criterion
         (f                            : Ωᵃ → Ωᵃ → Ωᵇ)
         (γ                            : b₀ ＝ a₀)
         (idempotent-up-to-conjugation : (p : Ωᵃ)
                                       → conjugate-loop γ (f p p) ＝ p)
         (left-nilpotent               : (p : Ωᵃ) → f p refl ＝ refl)
         (right-nilpotent              : (q : Ωᵃ) → f refl q ＝ refl)
         (homomorphism                 : (p q r s : Ωᵃ)
                                       → f (p ∙ r) (q ∙ s) ＝ f p q ∙ f r s)
        where

  nilpotent : (p : Ωᵃ) → f p p ＝ refl
  nilpotent p =
   f p p                   ＝⟨ I    ⟩
   f (p ∙ refl) (refl ∙ p) ＝⟨ II   ⟩
   f p refl ∙ f refl p     ＝⟨ III  ⟩
   refl ∙ refl             ＝⟨ refl ⟩
   refl                    ∎
    where
     I   = sym (ap₂ f (refl-right-neutral p) (refl-left-neutral p))
     II  = homomorphism p refl refl p
     III = ap₂ _∙_ (left-nilpotent p) (right-nilpotent p)

  Ω-trivial : (p : Ωᵃ) → p ＝ refl
  Ω-trivial p =
   p                        ＝⟨ sym (idempotent-up-to-conjugation p) ⟩
   conjugate-loop γ (f p p) ＝⟨ ap (conjugate-loop γ) (nilpotent p) ⟩
   conjugate-loop γ refl    ＝⟨ conjugate-loop-refl γ ⟩
   refl                     ∎


Finally, we show that it applies to Jakub's setting: any type with a ternary
majority operation must be a set.


open import gist.MajoritiesOnlyActOnSets

majorities-only-act-on-sets : (M : Type) (m : M → M → M → M)
                            → ((a b : M) → m b a a ＝ a)
                            → ((a b : M) → m a b a ＝ a)
                            → ((a b : M) → m a a b ＝ a)
                            → (m₀ : M) → (p : m₀ ＝ m₀) → p ＝ refl
majorities-only-act-on-sets M m eq₀ eq₁ eq₂ m₀ =
 Ω-trivial
  M
  m₀
  (m m₀ m₀ m₀)
  f
  idem₁
  side₁-is-p
  side₀-is-refl
  side₂-is-refl
  (λ p q r s → sym (m'-is-homo p r refl refl q s))
   where
    open Ω-trivial-criterion
    open type-with-majority M m eq₀ eq₁ eq₂ m₀
    f : (m₀ ＝ m₀) → (m₀ ＝ m₀) → m m₀ m₀ m₀ ＝ m m₀ m₀ m₀
    f p q = m' p refl q