created: 2025-08-02

This is how we formalize the Eckmann-Hilton Argument in Arend:

The Eckmann-Hilton Argument, says, that two monoids (*, e₁) and (∘, e₂) on the same set A, which satisfy an interchange law, are in fact the same and commutative.

More precisely, for all a, b : A we have

• Their operations behave the same a * b = a ∘ b,
• They have the same identity e₁ = e₂,
• And they are commutative a ∘ b = b ∘ a.

The interchange-law we require, is
(a * b) ∘ (c * d) = a ∘ c * b ∘ d.

EH-Structure

First, we formalize a structure, which represents our two monoids.
For simplicity, we define the operations on the same type, instead of two types which are equal. That simplifies the proof immensely.

\import Algebra.Meta
\import Algebra.Monoid
\import Arith.Nat
\import Category
\import Function.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Prelude

\module EH \where {
  \record EHStructure (A : \Type)
    | \infixl 7 * : A -> A -> A
    | \fixl 8 o \alias \infixl 8 ∘ : A -> A -> A
    | e1 : A  -- unit for *
    | e2 : A  -- unit for ∘
    | *-left {x : A} : e1 * x = x
    | *-right {x : A} : x * e1 = x
    | *-assoc {x y z : A} : (x * y) * z = x * (y * z)
    | o-left {x : A} : e2 ∘ x = x
    | o-right {x : A} : x ∘ e2 = x
    | o-assoc {x y z : A} : (x ∘ y) ∘ z = x ∘ (y ∘ z)
    | interchange {a b c d : A} : (a * b) ∘ (c * d) = a ∘ c * b ∘ d

EH lists all the usual monoid-axioms, and the interchange.

Somewhat arbitrary lemmas

From here, we need some simple lemmas to rewrite equalities inside an operation:
b = c ⟹ a ∘ b = a ∘ c and
a = c ⟹ a ∘ b = c ∘ b.

  \func ap-left-lemma {A : \Type} {* : A -> A -> A} {a b c : A} (p : a = c) :  *
 a b = * c b => rewrite p idp

  \func ap-right-lemma {A : \Type} {* : A -> A -> A} {a b c : A} (p : b = c) :  
* a b = * a c => rewrite p idp

(Note: There is probably a much simpler way to do there rewrites, that using these two lemmas.)

Proofs of Eckmann-Hilton

The actual rewriting process to show the required properties, even though trivial on paper, requires some more work when formalized.

Here we write a ==< eq1 >== b ==< eq2 >== c ==< eq3 >== d for the equality-chain
$$\begin{align} a & =_{< eq_1 >} b \\ & =_{< eq_2 >} c \\ & =_{< eq_3 >} d \end{align}$$
which represents a proof term for a = d.

Unit insertion lemmas

we need
a * b = (a ∘ e₂) * (e₂ ∘ b)

  \func eckmannHilton-add-*-units-inner
    {A : \Type}
    (S : EHStructure A)
    (a b : A)
    : a S.* b = (a S.∘ S.e2) S.* (S.e2 S.∘ b) =>
    a * b           ==< ap-left-lemma  {S.A} {S.*} (inv S.o-right) >==
    a ∘ S.e2 S.* b  ==< ap-right-lemma {S.A} {S.*} (inv S.o-left)  >== 
    idp

and
a * b = (e₂ ∘ a) * (b ∘ e₂)
which do nothing more, than fill units into

  \func eckmannHilton-add-*-units-outer
    {A : \Type}
    (S : EHStructure A)
    (a b : A)
    : a S.* b = (S.e2 S.∘ a) S.* (b S.∘ S.e2) =>
    a * b           ==< ap-left-lemma  {S.A} {S.*} (inv S.o-left)  >==
    S.e2 ∘ a S.* b  ==< ap-right-lemma {S.A} {S.*} (inv S.o-right) >== 
    idp

The corresponding equalities with exchanged operations, use for convenience, already part of the proof of Eckmann-Hilton.
This is obviously not required, but simplified the rewriting. Note the shortened syntax here, which ommits the last >== idp.
Also, here we use the meta ‘tactic’ (in case you are, like me, more familiar with coq than Arend)
rewriteI to rewrite e₂ = e₁ in the calc term, i.e.
(a * e₁) ∘ b = (a * e₂) ∘ b.
In calc itself, we apply ap-right-lemma to rewrite under the operation ∘ with the left, (or resp. the right), unit law
b = b * e₁.
The eckmannHilton-add-o-units-outer function just omits the renaming, and applies the identities directly.

\func eckmannHilton-add-o-units-inner
    {A : \Type}
    (S : EHStructure A)
    (a b : A)
    : a S.∘ b = (a S.* S.e2) S.∘ (S.e2 S.* b) =>
    \let
      | e1-eq-e2 : S.e1 = S.e2 => eckmannHilton-unit-eq S
      | calc : a S.∘ b = (a S.* S.e1) S.∘ (S.e1 S.* b) =>
        a S.∘ b                 ==< ap-left-lemma  {S.A} {S.∘} (inv S.*-right) >==
        (a S.* S.e1) S.∘ b      ==< ap-right-lemma {S.A} {S.∘} (inv S.*-left)
    \in rewriteI e1-eq-e2 calc

  \func eckmannHilton-add-o-units-outer
    {A : \Type}
    (S : EHStructure A)
    (a b : A)
    : a S.∘ b = (S.e2 S.* a) S.∘ (b S.* S.e2) =>
    rewriteI (eckmannHilton-unit-eq S) (
        a S.∘ b                 ==< ap-left-lemma  {S.A} {S.∘} (inv S.*-left) >==
        (S.e1 S.* a) S.∘ b      ==< ap-right-lemma {S.A} {S.∘} (inv S.*-right)
    )

Equality of the unit elements

Now for the actual proof of the Eckmann-Hilton theorem.
We first show, that both units are the same.

$$\begin{align} e_1 &= e_1 * e_1 & - e_1 \text{is the unit}\\ &=(e_1 ∘ e_2)*(e_2 ∘ e_1) & - \text{the }\texttt{eckmannHilton-add-*-units-inner} \text{ lemma}\\ &=(e_1 * e_2) ∘ (e_2 * e_1) & - \text{interchange}\\ & = e_2 ∘ e_2 =e_2 \end{align}$$

  \func eckmannHilton-unit-eq
    {A : \Type}
    (S : EHStructure A)
    : S.e1 = S.e2 =>
    S.e1                                ==< inv S.*-right >==
    S.e1 S.* S.e1                       ==< eckmannHilton-add-*-units-inner S S.e1 S.e1 >==
    (S.e1 S.∘ S.e2) S.* (S.e2 S.∘ S.e1) ==< inv (S.interchange {S.e1} {S.e2} {S.e2} {S.e1}) >==
    (S.e1 S.* S.e2) S.∘ (S.e2 S.* S.e1) ==< ap-left-lemma  {S.A} {S.∘} S.*-left >==
    S.e2 S.∘ (S.e2 S.* S.e1)            ==< ap-right-lemma {S.A} {S.∘} *-right  >==
    S.e2 S.∘ S.e2                       ==< S.o-left {S.e2}

Pointwise equality of the operations

The equality of the operations on arbitrary elements in now trivial:
$$\begin{align} a*b & = (a∘1)*(1∘b) & - \text{add inner units (we have shown that they are the same)}\\ & =(a*1)∘(1*b) & - \text{interchange} \\ & =a∘b & - \text{remove the units} \end{align}$$

  \func eckmannHilton-ops-eq
    {A : \Type}
    (S : EHStructure A)
    :  \Pi (a b : A) -> a S.* b = a S.∘ b => \lam a b =>
      \let
        | expand : a S.* b = (a S.* S.e2) S.∘ (S.e2 S.* b) =>
          a S.* b                               ==< eckmannHilton-add-*-units-inner S a b >==
          (a S.∘ S.e2) S.* (S.e2 S.∘ b)         ==< inv(S.interchange {a} {S.e2} {S.e2} {b})
        | reduce :  (a S.* S.e2) S.∘ (S.e2 S.* b) = a S.∘ b => inv (eckmannHilton-add-o-units-inner S a b)
      \in
        a S.* b                       ==< expand >==
        (a S.* S.e2) S.∘ (S.e2 S.* b) ==< reduce >==
        a S.∘ b                       ==< idp

Equality of the operations as functions

Now we take advantage of the univalence-axiom, on which Arend is built.
For arbitrary types A and B, we have
$$A\tilde= B \implies A = B.$$ As can be shown, this implies function extensionality:

for any two f, g : A → B we have ∀a ∈ A : f(a) = g(a) ⟹ f =_{(A → B)} g as functions.
Or, if we rewrite this a dependent function: There exists an element in the type
$$ \prod\limits_{f,g:A\to B}\prod\limits_{a:A}\prod\limits_{ fa\ =_{\!B}\ ga}(f =_{A\to B} g).$$

As you can see, the actual argument used below is a bit different, since univalence is baked into Arend with the help of a special Interval type {0, 1} ∈ I. (The type I has more elements than 0 and 1, r : I ⊢ r = 0 ∨ r = 1 is not true)
We get our path directly from the path constructor,
which takes a function with the interval type (here i without type annotation).
The path is this function evaluated at both endpoints 0 and 1.

The ‘trick’ is to supply the elements a, b ∈ A inside the path.
So for ∀a, b ∈ A : a * b = a ∘ b, abbreviated pointwise, we effectively go from endpoint
(pointwise x y) @ 0 (i.e. *by ) to endpoint (pointwise x y) @ 1 (i.e. ∘).
This results in * = ∘.

  \func eckmannHilton-ops-ext-eq {A : \Type}
                                 (S : EHStructure A)
    : (S.*) = (S.∘) =>
    \let
      | pointwise => eckmannHilton-ops-eq S
    \in
      path (\lam i => \lam x y => pointwise x y @ i)

Proof of commutativity

Finally, we show that the opartion * is commutative:
$$\begin{align} a*b & = a\circ b \\ & = (1 * a) \circ (b * 1) \\ & = (1 * b) * (a * 1) & -\text{interchange}\\ & = b \circ a \end{align}$$

  \func eckmannHilton-commutativity
    {A : \Type}
    (S : EHStructure A) : \Pi (a b : A) -> a S.* b = b S.* a =>
    \lam a b =>
    a S.* b                         ==< eckmannHilton-ops-eq S a b >==
    a S.∘ b                         ==< eckmannHilton-add-o-units-outer S a b >==
    (S.e2 S.* a) S.∘ (b S.* S.e2)   ==< interchange >==
    S.e2 S.∘ b S.* a S.∘ S.e2       ==< inv (eckmannHilton-add-*-units-outer S b a)

}

With this we have shown that (*, e₁) = (∘, e₂) as monoids.

There is another way to understand this.
If we have two monoids, and one oparation is a monoid-morphism with respect to the other monoid (i.e. the interchange-axiom holds), then
the monoids are the same and commutative.
My personal favorite as far as formulations of EH go is: A monoid object in the category of monoids is commutative.

Another Note

This whole thing may well already be in the standard-library of Arend somewhere and I just haven’t found it.
But even then I’d like to try see for myself, if I can reasonably apply this argument to instances of the actual standard-library Monoid-class.
In the end, all of this is just an exercise ¯\_(ツ)_/¯