{-# OPTIONS --safe --without-K #-}
{-
A self-contained proof of the following result (found at the bottom of the file):
Any type with a binary operation that is associative, commutative, and idempotent
is 0-truncated.
Checked with Agda version 2.6.4.3.
Written 17 February 2026.
-}

infix  _≡_
data _≡_ {A : Set} (a : A) : A → Set where
  rfl : a ≡ a

ap : {A B : Set} {a b : A} (f : A → B) → a ≡ b → f a ≡ f b
ap f rfl = rfl

infixr  _∙_
_∙_ : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
rfl ∙ rfl = rfl

eq-congr : {A : Set} {a b x y : A} → a ≡ x → b ≡ y → a ≡ b → x ≡ y
eq-congr rfl rfl p = p

eq-congr-∙ : {A : Set} {a b c x y z : A}
             {h1 : a ≡ x} {h2 : b ≡ y} {h3 : c ≡ z}
             (p : a ≡ b) (q : b ≡ c) →
             eq-congr h1 h3 (p ∙ q) ≡ eq-congr h1 h2 p ∙ eq-congr h2 h3 q
eq-congr-∙ {h1 = rfl} {h2 = rfl} {h3 = rfl} p q = rfl

eq-congr-rfl : {A : Set} {a x : A} (h : a ≡ x) →
               eq-congr h h rfl ≡ rfl
eq-congr-rfl rfl = rfl

bla : {A : Set} {a b x y : A} (ha : a ≡ a) (hb : b ≡ b)
      (hax : a ≡ x) (hby : b ≡ y) (p : a ≡ b) →
      eq-congr hax hby (eq-congr ha hb p)
      ≡ eq-congr (eq-congr hax hax ha) (eq-congr hby hby hb) (eq-congr hax hby p)
bla ha hb rfl rfl p = rfl

∙rfl : {A : Set} {a b : A} (p : a ≡ b) → p ∙ rfl ≡ p
∙rfl rfl = rfl

rfl∙ : {A : Set} {a b : A} (p : a ≡ b) → rfl ∙ p ≡ p
rfl∙ rfl = rfl

ap2 : {A B C : Set} (f : A → B → C) {a1 a2 : A} {b1 b2 : B}
      → a1 ≡ a2 → b1 ≡ b2 → f a1 b1 ≡ f a2 b2
ap2 f rfl rfl = rfl

assoc-4 : {A : Set} {a b c d e : A}
          {p : a ≡ b} {q : b ≡ c} {r : c ≡ d} {s : d ≡ e} →
          (p ∙ q) ∙ (r ∙ s) ≡ p ∙ (q ∙ r) ∙ s
assoc-4 {p = rfl} {q = rfl} {r = rfl} {s = rfl} = rfl

sym : {A : Set} {a b : A} → a ≡ b → b ≡ a
sym rfl = rfl

comm² : {A : Set} {a : A} {p q : a ≡ a} (h : p ∙ q ≡ q ∙ p) →
        (p ∙ p) ∙ (q ∙ q) ≡ (q ∙ q) ∙ (p ∙ p)
comm² {p = p} {q = q} h = eq-congr (sym assoc-4) (sym assoc-4)
          (eq-congr (ap (λ x → p ∙ x ∙ q) (sym h))
          (ap (λ x → q ∙ x ∙ p) h)
          (eq-congr assoc-4 assoc-4 ((ap (λ x → x ∙ x)) h)))

eq-congr-sym : {A : Set} {a b x y : A} {hax : a ≡ x} {hby : b ≡ y}
               {p : a ≡ b} {q : x ≡ y} →
               eq-congr hax hby p ≡ q → p ≡ eq-congr (sym hax) (sym hby) q
eq-congr-sym {hax = rfl} {hby = rfl} rfl = rfl

congr-∙  : {A : Set} {a b u v x y : A} (l1 : a ≡ u) (l2 : u ≡ x)
           (r1 : b ≡ v) (r2 : v ≡ y) (p : a ≡ b) →
           eq-congr (l1 ∙ l2) (r1 ∙ r2) p ≡ eq-congr l2 r2 (eq-congr l1 r1 p)
congr-∙ rfl rfl rfl rfl p = rfl

eq-congr-sq : {A : Set} {a b x y : A} (p : a ≡ b) (q : a ≡ x) (r : b ≡ y) →
            q ∙ eq-congr q r p ≡ p ∙ r
eq-congr-sq rfl rfl rfl = rfl

∙-cancel : {A : Set} {a b c : A} (p : a ≡ b) (q1 q2 : b ≡ c) →
           p ∙ q1 ≡ p ∙ q2 → q1 ≡ q2
∙-cancel rfl q1 q2 h = eq-congr (rfl∙ q1) (rfl∙ q2) h

module _
  (A : Set)
  (_*_ : A → A → A)
  (idem : (a : A) → a * a ≡ a)
  (comm : (a b : A) → a * b ≡ b * a)
  (assoc : (a b c : A) → (a * b) * c ≡ a * (b * c))
  (x₀ : A)
  where

  ΩA : Set
  ΩA = x₀ ≡ x₀

  *-paths : {a1 a2 b1 b2 : A} → a1 ≡ a2 → b1 ≡ b2 →
            a1 * b1 ≡ a2 * b2
  *-paths = ap2 _*_

  *-paths≡∙ : {a1 a2 b1 b2 : A} (p : a1 ≡ a2) (q : b1 ≡ b2) →
              *-paths p q ≡ ap (_* b1) p ∙ ap (a2 *_) q
  *-paths≡∙ rfl rfl = rfl

  eq-congr' : x₀ * x₀ ≡ x₀ * x₀ → x₀ ≡ x₀
  eq-congr' = eq-congr (idem x₀) (idem x₀)

  *-loop : ΩA → ΩA → ΩA
  *-loop p q = eq-congr' (*-paths p q)

  f g : ΩA → ΩA
  f p = eq-congr' (ap (_* x₀) p)
  g q = eq-congr' (ap (x₀ *_) q)

  *-loop≡∙ : (p q : x₀ ≡ x₀) → *-loop p q ≡ f p ∙ g q
  *-loop≡∙ p q = ap eq-congr' (*-paths≡∙ _ _)
                  ∙ eq-congr-∙ (ap (_* x₀) p) (ap (x₀ *_) q)

  idem-paths : {a b : A} (p : a ≡ b) →
               eq-congr (idem a) (idem b) (*-paths p p) ≡ p
  idem-paths rfl = eq-congr-rfl (idem _)

  idem-loop : (p : ΩA) → *-loop p p ≡ p
  idem-loop = idem-paths

  comm-paths : {a b x y : A} (p : a ≡ x) (q : b ≡ y) →
               eq-congr (comm a b) (comm x y) (*-paths p q)
               ≡ *-paths q p
  comm-paths rfl rfl = eq-congr-rfl _

  t : ΩA
  t = eq-congr' (comm x₀ x₀)

  comm-loop' : (p q : ΩA) →
              eq-congr t t (*-loop p q) ≡ *-loop q p
  comm-loop' p q = eq-congr
    (bla (comm x₀ x₀) (comm x₀ x₀) (idem x₀) (idem x₀) (*-paths p q))
    rfl (ap eq-congr' (comm-paths p q))

  t-center : (p : ΩA) → eq-congr t t p ≡ p
  t-center p = eq-congr (ap (eq-congr t t) (idem-loop p)) (idem-loop p) (comm-loop' p p)

  comm-loop : (p q : ΩA) → *-loop p q ≡ *-loop q p
  comm-loop p q = eq-congr (t-center _) rfl (comm-loop' p q)

  fg-swap : (p q : ΩA) → f p ∙ g q ≡ f q ∙ g p
  fg-swap p q = eq-congr (*-loop≡∙ p q) (*-loop≡∙ q p) (comm-loop p q)

  f-rfl : f rfl ≡ rfl
  f-rfl = eq-congr-rfl _

  g-rfl : g rfl ≡ rfl
  g-rfl = eq-congr-rfl _

  f≡g : (p : ΩA) → f p ≡ g p
  f≡g p = eq-congr (ap (f p ∙_) g-rfl ∙ ∙rfl _) (ap (_∙ g p) f-rfl ∙ rfl∙ _)
           (fg-swap p rfl)

  idem-loop-ff : (p : ΩA) → f p ∙ f p ≡ p
  idem-loop-ff p = ap (f p ∙_) (f≡g p) ∙ eq-congr (*-loop≡∙ p p) rfl (idem-loop p)

  ff-comm : (p q : ΩA) → f p ∙ f q ≡ f q ∙ f p
  ff-comm p q = eq-congr (ap (f p ∙_) (sym (f≡g q))) (ap (f q ∙_) (sym (f≡g p)))
                (fg-swap p q)

  loop-comm : (p q : ΩA) → p ∙ q ≡ q ∙ p
  loop-comm p q = eq-congr (ap2 _∙_ (idem-loop-ff p) (idem-loop-ff q))
                  (ap2 _∙_ (idem-loop-ff q) (idem-loop-ff p))
                  (comm² (ff-comm p q))

  assoc-paths : {a b c x y z : A} (p : a ≡ x) (q : b ≡ y) (r : c ≡ z) →
                eq-congr (assoc a b c) (assoc x y z) (*-paths (*-paths p q) r)
                ≡ *-paths p (*-paths q r)
  assoc-paths rfl rfl rfl = eq-congr-rfl _

  blabla : {a b c d e : A} (hab : a * b ≡ c) (hcd : c * d ≡ e)
           (p : a ≡ a) (q : b ≡ b) (r : d ≡ d) →
           eq-congr (*-paths hab rfl ∙ hcd) (*-paths hab rfl ∙ hcd)
           (*-paths (*-paths p q) r) ≡
           eq-congr hcd hcd (*-paths (eq-congr hab hab (*-paths p q)) r)
  blabla rfl rfl p q r = rfl

  idem3 : (x₀ * x₀) * x₀ ≡ x₀
  idem3 = *-paths (idem x₀) rfl ∙ idem x₀

  foo : (p q r : ΩA) →
        eq-congr idem3 idem3 (*-paths (*-paths p q) r) ≡ *-loop (*-loop p q) r
  foo p q r = blabla (idem x₀) (idem x₀) p q r

  blabla' : {a b c d e : A} (hab : a * b ≡ c) (hcd : d * c ≡ e)
           (p : a ≡ a) (q : b ≡ b) (r : d ≡ d) →
           eq-congr (*-paths rfl hab ∙ hcd) (*-paths rfl hab ∙ hcd)
           (*-paths r (*-paths p q)) ≡
           eq-congr hcd hcd (*-paths r (eq-congr hab hab (*-paths p q)))
  blabla' rfl rfl p q r = rfl

  idem3' : x₀ * (x₀ * x₀) ≡ x₀
  idem3' = *-paths rfl (idem x₀) ∙ idem x₀

  foo' : (p q r : ΩA) →
        eq-congr idem3' idem3' (*-paths p (*-paths q r)) ≡ *-loop p (*-loop q r)
  foo' p q r = blabla' (idem x₀) (idem x₀) q r p

  t' : ΩA
  t' = sym idem3 ∙ (assoc x₀ x₀ x₀ ∙ idem3')

  *-loop-assoc' : (p q r : ΩA) →
               eq-congr t' t' (*-loop (*-loop p q) r) ≡ *-loop p (*-loop q r)
  *-loop-assoc' p q r = eq-congr
    (sym (congr-∙ (assoc x₀ x₀ x₀) idem3' _ idem3' _)
      ∙ sym (congr-∙ (sym idem3) _ _ _ _))
    (foo' p q r)
    (ap (eq-congr idem3' idem3') (ap (eq-congr (assoc x₀ x₀ x₀) _)
    (sym (eq-congr-sym (foo p q r))) ∙ assoc-paths p q r))

  *-loop-rfl : (p : ΩA) → *-loop p rfl ≡ f p
  *-loop-rfl p = *-loop≡∙ p rfl ∙ ap (f p ∙_) g-rfl ∙ ∙rfl (f p)

  *-loop-assoc : (p q r : ΩA) → *-loop (*-loop p q) r ≡ *-loop p (*-loop q r)
  *-loop-assoc p q r = ∙-cancel t' _ _ (loop-comm _ _ ∙ sym (eq-congr-sq _ _ _))
                       ∙ *-loop-assoc' p q r

  ff≡f : (p : ΩA) → f (f p) ≡ f p
  ff≡f p = eq-congr (*-loop-rfl _ ∙ ap f (*-loop-rfl p))
           (ap (*-loop p) (*-loop-rfl rfl ∙ f-rfl) ∙ *-loop-rfl p)
           (*-loop-assoc p rfl rfl)

  f-null : (p : ΩA) → f p ≡ rfl
  f-null p = ∙-cancel (f p) (f p) rfl ((ap2 _∙_ (sym (ff≡f p)) (sym (ff≡f p)) ∙ idem-loop-ff (f p)) ∙ sym (∙rfl (f p)))

  Ω-null : (p : x₀ ≡ x₀) → p ≡ rfl
  Ω-null p = sym (idem-loop-ff p) ∙ ap2 _∙_ (f-null p) (f-null p) ∙ ∙rfl rfl