An attempt to prove that the free semigroup on one generator is commutative.

Nat.agda

{-# OPTIONS --cubical --safe #-}

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism using (Iso; isoToPath)

data N : Set where
  one : N
  _+_ : N → N → N
  assoc : (a b c : N) → (a + b) + c ≡ a + (b + c)

data N' : Set where
  one' : N'
  s : N' → N'

_+'_ : N' → N' → N'
one' +' b = s b
s a +' b = s (a +' b)

assoc' : ∀ a b c → (a +' b) +' c ≡ a +' (b +' c)
assoc' one' b c i = s (b +' c)
assoc' (s a) b c i = s (assoc' a b c i)

to : N' → N
to one' = one
to (s a) = one + to a

from : N → N'
from one = one'
from (a + b) = from a +' from b
from (assoc a b c i) = assoc' (from a) (from b) (from c) i

from∘to : ∀ a → from (to a) ≡ a
from∘to one' i = one'
from∘to (s a) i = s (from∘to a i)

add-lemma : ∀ a b → to (a +' b) ≡ to a + to b
add-lemma one' b = refl
add-lemma (s a) b = (λ i → one + (add-lemma a b i)) ∙ sym (assoc one (to a) (to b))

to∘from : ∀ a → to (from a) ≡ a
to∘from one = refl
to∘from (a + b) = add-lemma (from a) (from b) ∙ (λ i → to∘from a i + to∘from b i)
to∘from (assoc a b c j) = {!!} -- I have no clue how to prove this lol

iso : Iso N N'
iso .Iso.fun = from
iso .Iso.inv = to
iso .Iso.rightInv = from∘to
iso .Iso.leftInv = to∘from

path : N ≡ N'
path = isoToPath iso

-- (_+_ : N → N → N) ≡ (_+'_ : N' → N' → N')
+-path : PathP (λ i → path i → path i → path i) _+_ _+'_
+-path = toPathP (λ i a b → from∘to a i +' from∘to b i)

+'-suc-r : ∀ a b → s (a +' b) ≡ a +' s b
+'-suc-r one' b i = s (s b)
+'-suc-r (s a) b i = s (+'-suc-r a b i)

+'-comm : ∀ a b → a +' b ≡ b +' a
+'-comm one' one' = refl
+'-comm one' (s b) = cong s (+'-comm one' b)
+'-comm (s a) b = cong s (+'-comm a b) ∙ +'-suc-r b a

+-comm : ∀ a b → a + b ≡ b + a
+-comm = transport (sym (λ i → (a b : path i) → +-path i a b ≡ +-path i b a)) +'-comm