Free

Martin Escardo, July 2026.

The free egroup on a setoid.

Its underlying type is the type FA of words on the generators, and its
equivalence relation is convertibility _∿_. The operation is
concatenation _β—¦_, and we check that it is a congruence for _∿_, that
the group laws hold up to _∿_, and that the generators are inserted by
Ξ·. We then prove that it is free, in the sense that every setoid map
from the generators into an egroup extends along Ξ· to a homomorphism,
uniquely up to the equivalence relation of that egroup.


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

open import MLTT.Spartan
open import MLTT.List renaming (_∷_ to _β€’_ ; _++_ to _β—¦_ ; ++-assoc to β—¦-assoc)
open import Relations.SRTclosure

module EGroups.Free
        {𝓀 : Universe}
        (A : 𝓀 ⁺ Μ‡ )
        (_β‰ˆ_ : A β†’ A β†’ 𝓀 Μ‡ )
        (β‰ˆr : reflexive  _β‰ˆ_)
        (β‰ˆs : symmetric  _β‰ˆ_)
        (β‰ˆt : transitive _β‰ˆ_)
       where

open import EGroups.Reduction A _β‰ˆ_ β‰ˆr β‰ˆs β‰ˆt
open import EGroups.Setoid
open import EGroups.Type


Identities give convertibilities, and convertibility is a congruence
for cons, a special case of the congruence for concatenation.


＝-gives-∿ : {s t : FA} β†’ s ＝ t β†’ s ∿ t
＝-gives-∿ {s} refl = srt-reflexive _β–·_ s

β€’-∿ : (x : X) {s t : FA} β†’ s ∿ t β†’ (x β€’ s) ∿ (x β€’ t)
β€’-∿ x e = ∿-β—¦-right (x β€’ []) e


We record the two basic cancellations as convertibilities.


cancel : (x : X) β†’ (x β€’ (x ⁻) β€’ []) ∿ []
cancel x = srt-extension _β–·_ (x β€’ (x ⁻) β€’ []) []
            ([] , [] , x , (x ⁻) , refl , refl , β‰ˆ[X]-refl (x ⁻))

cancel⁻ : (x : X) (s : FA) β†’ ((x ⁻) β€’ x β€’ s) ∿ s
cancel⁻ x s = srt-extension _β–·_ ((x ⁻) β€’ x β€’ s) s
               ([] , s , (x ⁻) , x , refl , refl , to-β‰ˆ[X] ((inv-invol x) ⁻¹))


The word inverse reverses the word and inverts each letter.


inv : FA β†’ FA
inv []      = []
inv (x β€’ s) = inv s β—¦ ((x ⁻) β€’ [])

inv-left : (x : FA) β†’ (inv x β—¦ x) ∿ []
inv-left []      = srt-reflexive _β–·_ []
inv-left (a β€’ s) =
 srt-transitive _β–·_ (inv (a β€’ s) β—¦ (a β€’ s)) (inv s β—¦ ((a ⁻) β€’ a β€’ s)) []
  (＝-gives-∿ (β—¦-assoc (inv s) ((a ⁻) β€’ []) (a β€’ s)))
  (srt-transitive _β–·_ (inv s β—¦ ((a ⁻) β€’ a β€’ s)) (inv s β—¦ s) []
    (∿-β—¦-right (inv s) (cancel⁻ a s))
    (inv-left s))

inv-right : (x : FA) β†’ (x β—¦ inv x) ∿ []
inv-right []      = srt-reflexive _β–·_ []
inv-right (a β€’ s) =
 srt-transitive _β–·_
  ((a β€’ s) β—¦ inv (a β€’ s)) (a β€’ ((s β—¦ inv s) β—¦ ((a ⁻) β€’ []))) []
  (＝-gives-∿ (ap (a β€’_) ((β—¦-assoc s (inv s) ((a ⁻) β€’ [])) ⁻¹)))
  (srt-transitive _β–·_ (a β€’ ((s β—¦ inv s) β—¦ ((a ⁻) β€’ []))) (a β€’ ((a ⁻) β€’ [])) []
    (β€’-∿ a (∿-β—¦-left (inv-right s) ((a ⁻) β€’ [])))
    (cancel a))


We assemble the free egroup.


underlying-setoid-of-free-egroup : Setoid (𝓀 ⁺) (𝓀 ⁺)
underlying-setoid-of-free-egroup = FA
                                 , _∿_
                                 , srt-reflexive  _β–·_
                                 , srt-symmetric  _β–·_
                                 , srt-transitive _β–·_

free-egroup : EGroup (𝓀 ⁺) (𝓀 ⁺)
free-egroup = underlying-setoid-of-free-egroup
            , _β—¦_
            , (Ξ» {x} {x'} {y} {y'} β†’ β—¦-cong-∿ {x} {x'} {y} {y'})
            , (Ξ» x y z β†’ ＝-gives-∿ (β—¦-assoc x y z))
            , []
            , (Ξ» x β†’ srt-reflexive _β–·_ x)
            , (Ξ» x β†’ ＝-gives-∿ (([]-right-neutral x) ⁻¹))
            , (Ξ» x β†’ inv x , inv-left x , inv-right x)


The underlying type of the free egroup is FA, and its insertion of
generators is Ξ· : A β†’ FA.


Ξ·α΄³ : A β†’ ⟨ free-egroup ⟩
Ξ·α΄³ = Ξ·


The universal property. Given an egroup 𝓖 and a setoid map f from the
setoid of generators to the underlying setoid of 𝓖, we extend f to a
homomorphism from the free egroup, and show that the extension is
unique up to the equivalence relation of 𝓖.

The extension h is defined by recursion on words, sending a generator
to its value under f and a formally inverted generator to the inverse
of that value. That f is a setoid map is needed already to see that h
identifies the two sides of a reduction, because we cancel adjacent
letters whose generators are merely β‰ˆ-related.


module free-egroup-universal-property
        {π“₯ 𝓦 : Universe}
        (𝓖 : EGroup π“₯ 𝓦)
        (f : A β†’ ⟨ 𝓖 ⟩)
        (f-resp : {a b : A} β†’ a β‰ˆ b β†’ f a β‰ˆβŸ¨ 𝓖 ⟩ f b)
       where

 open egroup-theory 𝓖
 open β‰ˆ-reasoning (underlying-relation 𝓖) (erefl 𝓖) (etrans 𝓖)

 private
  _*_    = emultiplication-of 𝓖
  *-cong = econgruence-of 𝓖
  eα΄³     = eunit-of 𝓖
  invα΄³   = einv 𝓖

 h : FA β†’ ⟨ 𝓖 ⟩
 h []            = eα΄³
 h ((β‚€ , a) β€’ s) = f a * h s
 h ((₁ , a) β€’ s) = invα΄³ (f a) * h s


The map h respects the letter-wise relation on words, and it is a
homomorphism from concatenation to the operation of 𝓖.


 h-respects-β‰ˆ[FA] : (s t : FA) β†’ s β‰ˆ[FA] t β†’ h s β‰ˆβŸ¨ 𝓖 ⟩ h t
 h-respects-β‰ˆ[FA] [] [] ⋆ = erefl 𝓖 eα΄³
 h-respects-β‰ˆ[FA] ((β‚€ , a) β€’ s) ((β‚€ , b) β€’ t) ((refl , q) , r) =
  *-cong (f-resp q) (h-respects-β‰ˆ[FA] s t r)
 h-respects-β‰ˆ[FA] ((₁ , a) β€’ s) ((₁ , b) β€’ t) ((refl , q) , r) =
  *-cong (β‰ˆ-inv-cong (f a) (f b) (f-resp q)) (h-respects-β‰ˆ[FA] s t r)

 h-is-hom : (s t : FA) β†’ h (s β—¦ t) β‰ˆβŸ¨ 𝓖 ⟩ (h s * h t)
 h-is-hom [] t = esym 𝓖 _ _ (eunit-left 𝓖 (h t))
 h-is-hom ((β‚€ , a) β€’ s) t =
  f a * h (s β—¦ t)   β‰ˆ[ *-cong (erefl 𝓖 (f a)) (h-is-hom s t) ]
  f a * (h s * h t) β‰ˆ[ esym 𝓖 _ _ (eassoc 𝓖 (f a) (h s) (h t)) ]
  (f a * h s) * h t β‰ˆβˆŽ
 h-is-hom ((₁ , a) β€’ s) t =
  invα΄³ (f a) * h (s β—¦ t)   β‰ˆ[ *-cong (erefl 𝓖 (invα΄³ (f a))) (h-is-hom s t) ]
  invα΄³ (f a) * (h s * h t) β‰ˆ[ esym 𝓖 _ _ (eassoc 𝓖 (invα΄³ (f a)) (h s) (h t)) ]
  (invα΄³ (f a) * h s) * h t β‰ˆβˆŽ


A redex is sent to the unit, and hence h identifies the two sides of a
reduction, of a reduction sequence, and finally of a convertibility.
The last step uses the Church-Rosser property modulo _β‰ˆ_, whose two
reducts are related by _β‰ˆ[FA]_ rather than by the identity type, which
is why we needed h to respect _β‰ˆ[FA]_.


 h-redex : (x y : X) β†’ y β‰ˆ[X] (x ⁻) β†’ h (x β€’ y β€’ []) β‰ˆβŸ¨ 𝓖 ⟩ eα΄³
 h-redex (β‚€ , a) (₁ , b) (refl , q) =
  f a * (invα΄³ (f b) * eα΄³) β‰ˆ[ I ]
  f a * invα΄³ (f b)        β‰ˆ[ II ]
  f a * invα΄³ (f a)        β‰ˆ[ einv-right 𝓖 (f a) ]
  eα΄³                      β‰ˆβˆŽ
   where
    I  = *-cong (erefl 𝓖 (f a)) (eunit-right 𝓖 (invα΄³ (f b)))
    II = *-cong (erefl 𝓖 (f a)) (β‰ˆ-inv-cong (f b) (f a) (f-resp q))
 h-redex (₁ , a) (β‚€ , b) (refl , q) =
  invα΄³ (f a) * (f b * eα΄³) β‰ˆ[ I ]
  invα΄³ (f a) * f b        β‰ˆ[ II ]
  invα΄³ (f a) * f a        β‰ˆ[ einv-left 𝓖 (f a) ]
  eα΄³                      β‰ˆβˆŽ
   where
    I  = *-cong (erefl 𝓖 (invα΄³ (f a))) (eunit-right 𝓖 (f b))
    II = *-cong (erefl 𝓖 (invα΄³ (f a))) (f-resp q)

 h-identifies-β–·-related-points : {s t : FA} β†’ s β–· t β†’ h s β‰ˆβŸ¨ 𝓖 ⟩ h t
 h-identifies-β–·-related-points (u , v , x , y , refl , refl , c) =
  h (u β—¦ x β€’ y β€’ v)            β‰ˆ[ h-is-hom u (x β€’ y β€’ v) ]
  h u * h (x β€’ y β€’ v)          β‰ˆ[ I ]
  h u * (h (x β€’ y β€’ []) * h v) β‰ˆ[ II ]
  h u * (eα΄³ * h v)             β‰ˆ[ III ]
  h u * h v                    β‰ˆ[ esym 𝓖 _ _ (h-is-hom u v) ]
  h (u β—¦ v)                    β‰ˆβˆŽ
   where
    I   = *-cong (erefl 𝓖 (h u)) (h-is-hom (x β€’ y β€’ []) v)
    II  = *-cong (erefl 𝓖 (h u)) (*-cong (h-redex x y c) (erefl 𝓖 (h v)))
    III = *-cong (erefl 𝓖 (h u)) (eunit-left 𝓖 (h v))

 h-identifies-▷⋆-related-points : (s t : FA) β†’ s ▷⋆ t β†’ h s β‰ˆβŸ¨ 𝓖 ⟩ h t
 h-identifies-▷⋆-related-points s t (n , i) = Ξ³ n s t i
  where
   Ξ³ : (n : β„•) (s t : FA) β†’ iteration _β–·_ n s t β†’ h s β‰ˆβŸ¨ 𝓖 ⟩ h t
   Ξ³ 0        s s refl        = erefl 𝓖 (h s)
   Ξ³ (succ n) s t (z , d , i) =
    etrans 𝓖 (h s) (h z) (h t) (h-identifies-β–·-related-points d) (Ξ³ n z t i)

 h-identifies-∿-related-points : (s t : FA) β†’ s ∿ t β†’ h s β‰ˆβŸ¨ 𝓖 ⟩ h t
 h-identifies-∿-related-points s t c = Ξ³ (Church-Rosserβ‰ˆ s t c)
  where
   Ξ³ : (Ξ£ zβ‚€ κž‰ FA , Ξ£ z₁ κž‰ FA , (s ▷⋆ zβ‚€) Γ— (t ▷⋆ z₁) Γ— (zβ‚€ β‰ˆ[FA] z₁))
     β†’ h s β‰ˆβŸ¨ 𝓖 ⟩ h t
   Ξ³ (zβ‚€ , z₁ , Οƒ , Ο„ , ez) =
    h s  β‰ˆ[ h-identifies-▷⋆-related-points s zβ‚€ Οƒ ]
    h zβ‚€ β‰ˆ[ h-respects-β‰ˆ[FA] zβ‚€ z₁ ez ]
    h z₁ β‰ˆ[ esym 𝓖 _ _ (h-identifies-▷⋆-related-points t z₁ Ο„) ]
    h t  β‰ˆβˆŽ


Hence h is a homomorphism from the free egroup which extends f along
the insertion of generators.


 free-map : ⟨ free-egroup ⟩ β†’ ⟨ 𝓖 ⟩
 free-map = h

 free-map-is-hom : is-hom free-egroup 𝓖 free-map
 free-map-is-hom = (Ξ» {s} {t} β†’ h-identifies-∿-related-points s t)
                 , (Ξ» {s} {t} β†’ h-is-hom s t)

 free-map-triangle : (a : A) β†’ free-map (Ξ·α΄³ a) β‰ˆβŸ¨ 𝓖 ⟩ f a
 free-map-triangle a = eunit-right 𝓖 (f a)


Any homomorphism extending f agrees with the extension up to the
equivalence relation of 𝓖. As in Groups.Free, the argument derives
preservation of the unit and of inverses from the other assumptions.


 free-map-is-unique : (g : ⟨ free-egroup ⟩ β†’ ⟨ 𝓖 ⟩)
                    β†’ is-hom free-egroup 𝓖 g
                    β†’ ((a : A) β†’ g (Ξ·α΄³ a) β‰ˆβŸ¨ 𝓖 ⟩ f a)
                    β†’ (s : ⟨ free-egroup ⟩) β†’ g s β‰ˆβŸ¨ 𝓖 ⟩ free-map s
 free-map-is-unique g g-hom@(_ , g-mult) g-tri = u
  where
   u : (s : FA) β†’ g s β‰ˆβŸ¨ 𝓖 ⟩ h s
   u []            = homs-preserve-unit free-egroup 𝓖 g g-hom
   u ((β‚€ , a) β€’ s) =
    g (Ξ·α΄³ a β—¦ s)   β‰ˆ[ g-mult {Ξ·α΄³ a} {s} ]
    g (Ξ·α΄³ a) * g s β‰ˆ[ *-cong (g-tri a) (u s) ]
    f a * h s      β‰ˆβˆŽ
   u ((₁ , a) β€’ s) =
    g (inv (Ξ·α΄³ a) β—¦ s)   β‰ˆ[ g-mult {inv (Ξ·α΄³ a)} {s} ]
    g (inv (Ξ·α΄³ a)) * g s β‰ˆ[ *-cong I (u s) ]
    invα΄³ (f a) * h s     β‰ˆβˆŽ
     where
      I : g (inv (Ξ·α΄³ a)) β‰ˆβŸ¨ 𝓖 ⟩ invα΄³ (f a)
      I = g (inv (Ξ·α΄³ a))  β‰ˆ[ homs-preserve-inv free-egroup 𝓖 g g-hom (Ξ·α΄³ a) ]
          invα΄³ (g (Ξ·α΄³ a)) β‰ˆ[ β‰ˆ-inv-cong (g (Ξ·α΄³ a)) (f a) (g-tri a) ]
          invα΄³ (f a)      β‰ˆβˆŽ

 free-map-is-uniqueβ‚‚ : (gβ‚€ g₁ : ⟨ free-egroup ⟩ β†’ ⟨ 𝓖 ⟩)
                     β†’ is-hom free-egroup 𝓖 gβ‚€
                     β†’ is-hom free-egroup 𝓖 g₁
                     β†’ ((a : A) β†’ gβ‚€ (Ξ·α΄³ a) β‰ˆβŸ¨ 𝓖 ⟩ f a)
                     β†’ ((a : A) β†’ g₁ (Ξ·α΄³ a) β‰ˆβŸ¨ 𝓖 ⟩ f a)
                     β†’ (s : ⟨ free-egroup ⟩) β†’ gβ‚€ s β‰ˆβŸ¨ 𝓖 ⟩ g₁ s
 free-map-is-uniqueβ‚‚ gβ‚€ g₁ iβ‚€ i₁ tβ‚€ t₁ s =
  etrans 𝓖 (gβ‚€ s) (free-map s) (g₁ s)
   (free-map-is-unique gβ‚€ iβ‚€ tβ‚€ s)
   (esym 𝓖 (g₁ s) (free-map s) (free-map-is-unique g₁ i₁ t₁ s))