If the free group on a set A is commutative, then A is a proposition

FreeGroupComm.agda

open import Cubical.Algebra.Group.Free
open import Cubical.Data.Bool
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.List renaming (elim to elimList)
open import Cubical.Data.Sum
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude
open import Cubical.HITs.FreeGroup
open import Cubical.HITs.FreeGroup.NormalForm
open import Cubical.HITs.PropositionalTruncation renaming (rec to rec₁)
open import Cubical.HITs.SetQuotients renaming ([_] to [_]/)

module FreeGroupComm where

module _ {ℓ} (A : Type ℓ) (isSetA : isSet A) where
  open NormalForm A
  open NF (freeGroupGroup A) η

  -- same idea as ηInj; in fact we should have
  -- η a · η b ≡ η c · η d → a ≡ c × b ≡ d
  lemma : ∀ a b → Path (FreeGroup A) (η a · η b) (η b · η a) → a ≡ b
  lemma a b p =
    rec₁ (isSetA _ _)
      (λ x → case ⇊1g⇒HasRedex _ _ (x .≡ε) of λ where
        (inl x) → cong snd x
        (inr (inl x)) → sym (cong snd x)
        (inr (inr (inl x))) → cong snd x
        (inr (inr (inr (inl ()))))
        (inr (inr (inr (inr ())))))
    $ Iso.fun (≡→red _ _)
    $ isoInvInjective (fst GroupIso-FG-L/↘↙)
      [ (true , _) ∷ (true , _) ∷ [] ]/ [ (true , _) ∷ (true , _) ∷ [] ]/
    $ cong (η a ·_) (·IdR _) ∙∙ p ∙∙ cong (η b ·_) (sym (·IdR _))

  FreeGroupComm→isProp : ((x y : FreeGroup A) → x · y ≡ y · x) → isProp A
  FreeGroupComm→isProp H a b = lemma a b (H (η a) (η b))