EGroups.FreeOnSetoid

Martin Escardo, July 2026.

The free egroup on a setoid, in pure MLTT.

EGroups.FreeOnType constructs the free egroup on a *type* A of
generators (with the identity type as the equality of
generators). Here we construct the free egroup on a *setoid* 𝔸, which
is the correct free-forgetful adjunction: the underlying-setoid
functor egroups → Setoids has a left adjoint.

The construction reuses the word-level free-group construction on the
underlying type ∣ 𝔸 ∣, imported from Groups.Free, but coarsens its
equivalence relation _∿_ so as to additionally identify generators
that are related in 𝔸. Explicitly, the equivalence relation _≍_ on
words is generated by _∿_ (cancellation of formal inverses) together
with the pointwise, letter-by-letter relation _≋_ coming from 𝔸.

For simplicity we take the equivalence relation of 𝔸 to live in the
same universe as its carrier.

TODO. Generalize this, if it is worth for any particular application.

\begin{code}

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

module EGroups.FreeOnSetoid where

open import MLTT.Spartan
open import MLTT.List renaming (_∷_ to _•_ ; _++_ to _◦_ ; ++-assoc to ◦-assoc)

open import Groups.Free using (module free-group-construction)
open import EGroups.Setoid
open import EGroups.Type
open import EGroups.MediatingMap

module _ (𝔸 : Setoid 𝓤 𝓤) where

 open free-group-construction ∣ 𝔸 ∣

\end{code}

The pointwise, letter-by-letter relation on words: two words are
_≋_-related when they have the same length, the same polarities, and
_≈⟦ 𝔸 ⟧_-related generators.

\begin{code}

 _≋_ : FA → FA → 𝓤 ̇
 []            ≋ []            = 𝟙
 []            ≋ (_ • _)       = 𝟘
 (_ • _)       ≋ []            = 𝟘
 ((n , a) • s) ≋ ((m , b) • t) = (n ＝ m) × (a ≈⟦ 𝔸 ⟧ b) × (s ≋ t)

 ≋-refl : (s : FA) → s ≋ s
 ≋-refl []            = ⋆
 ≋-refl ((n , a) • s) = refl , setoid-refl 𝔸 a , ≋-refl s

 ≋-sym : (s t : FA) → s ≋ t → t ≋ s
 ≋-sym []            []            _           = ⋆
 ≋-sym []            (x • t)       ()
 ≋-sym (x • s)       []            ()
 ≋-sym ((n , a) • s) ((m , b) • t) (p , q , r) =
  (p ⁻¹) , setoid-sym 𝔸 a b q , ≋-sym s t r

 ≋-trans : (s t u : FA) → s ≋ t → t ≋ u → s ≋ u
 ≋-trans []            []            []            _           _             = ⋆
 ≋-trans []            []            (x • u)       _           ()
 ≋-trans []            (x • t)       u             ()          _
 ≋-trans (x • s)       []            u             ()          _
 ≋-trans ((n , a) • s) ((m , b) • t) []            _           ()
 ≋-trans ((n , a) • s) ((m , b) • t) ((k , c) • u) (p , q , r) (p' , q' , r') =
  (p ∙ p') , setoid-trans 𝔸 a b c q q' , ≋-trans s t u r r'

 ≋-◦ : (s s' t t' : FA) → s ≋ s' → t ≋ t' → (s ◦ t) ≋ (s' ◦ t')
 ≋-◦ []            []            t t' _           e = e
 ≋-◦ []            (x • s')      t t' ()          e
 ≋-◦ (x • s)       []            t t' ()          e
 ≋-◦ ((n , a) • s) ((m , b) • s') t t' (p , q , r) e =
  p , q , ≋-◦ s s' t t' r e

 η-≋ : {a b : ∣ 𝔸 ∣} → a ≈⟦ 𝔸 ⟧ b → η a ≋ η b
 η-≋ q = refl , q , ⋆

\end{code}

The equivalence relation _≍_ on words, generated by _∿_ and _≋_.

\begin{code}

 data _≍_ : FA → FA → 𝓤 ̇ where
  ∿-gives-≍ : {s t : FA} → s ∿ t → s ≍ t
  ≋-gives-≍ : {s t : FA} → s ≋ t → s ≍ t
  ≍-trans   : {s t u : FA} → s ≍ t → t ≍ u → s ≍ u

 infix 0 _≍_

 ≍-refl : (s : FA) → s ≍ s
 ≍-refl s = ∿-gives-≍ (srt-reflexive _▷_ s)

 ≍-sym : (s t : FA) → s ≍ t → t ≍ s
 ≍-sym s t (∿-gives-≍ p) = ∿-gives-≍ (srt-symmetric _▷_ s t p)
 ≍-sym s t (≋-gives-≍ p) = ≋-gives-≍ (≋-sym s t p)
 ≍-sym s t (≍-trans p q) = ≍-trans (≍-sym _ t q) (≍-sym s _ p)

 ＝-gives-≍ : {s t : FA} → s ＝ t → s ≍ t
 ＝-gives-≍ {s} refl = ≍-refl s

 ◦-left-≍ : (s s' t : FA) → s ≍ s' → s ◦ t ≍ s' ◦ t
 ◦-left-≍ s s' t (∿-gives-≍ p) = ∿-gives-≍ (◦-cong-∿ p (srt-reflexive _▷_ t))
 ◦-left-≍ s s' t (≋-gives-≍ p) = ≋-gives-≍ (≋-◦ s s' t t p (≋-refl t))
 ◦-left-≍ s s' t (≍-trans {s} {u} {s'} p q) =
  ≍-trans (◦-left-≍ s u t p) (◦-left-≍ u s' t q)

 ◦-right-≍ : (s t t' : FA) → t ≍ t' → s ◦ t ≍ s ◦ t'
 ◦-right-≍ s t t' (∿-gives-≍ p) = ∿-gives-≍ (◦-cong-∿ (srt-reflexive _▷_ s) p)
 ◦-right-≍ s t t' (≋-gives-≍ p) = ≋-gives-≍ (≋-◦ s s t t' (≋-refl s) p)
 ◦-right-≍ s t t' (≍-trans {t} {u} {t'} p q) =
  ≍-trans (◦-right-≍ s t u p) (◦-right-≍ s u t' q)

 ◦-cong-≍ : {s s' t t' : FA} → s ≍ s' → t ≍ t' → s ◦ t ≍ s' ◦ t'
 ◦-cong-≍ {s} {s'} {t} {t'} d e =
  ≍-trans (◦-left-≍ s s' t d) (◦-right-≍ s' t t' e)

\end{code}

The free egroup on the setoid 𝔸: words with the operation of concatenation,
the empty word as unit, and finv as inverse, all up to _≍_.

\begin{code}

 free-egroup-setoid : EGroup 𝓤 𝓤
 free-egroup-setoid =
    (FA , _≍_ , (≍-refl , ≍-sym , (λ x y z → ≍-trans {x} {y} {z})))
  , _◦_
  , ( ◦-cong-≍
    , (λ s t u → ＝-gives-≍ (◦-assoc s t u))
    , ( []
      , (λ s → ≍-refl s)
      , (λ s → ＝-gives-≍ (([]-right-neutral s) ⁻¹))
      , (λ s → finv s , ∿-gives-≍ (finv-left-∿ s) , ∿-gives-≍ (finv-right-∿ s)) ) )

\end{code}

The universal property. Given a target egroup 𝓖 and a setoid map
f : 𝔸 → underlying-setoid 𝓖, the extension is the mediating map h of
EGroups.MediatingMap, which respects _≍_ because f respects the relation of 𝔸.

\begin{code}

 module universal-property
          (𝓖 : EGroup 𝓥 𝓦)
          (f : ∣ 𝔸 ∣ → ⟨ 𝓖 ⟩)
          (f-resp : is-setoid-map 𝔸 (underlying-setoid 𝓖) f)
        where

  open E-group-theory 𝓖
  open ≈-reasoning (underlying-relation 𝓖) (E-refl 𝓖) (E-trans 𝓖)
  open free-group-mediating-map ∣ 𝔸 ∣ ⟨ 𝓖 ⟩ (underlying-relation 𝓖)
        (E-refl 𝓖) (E-sym 𝓖) (E-trans 𝓖)
        (E-multiplication 𝓖) (E-is-congruence 𝓖) (E-assoc 𝓖)
        (E-unit 𝓖) (E-unit-left 𝓖) (E-unit-right 𝓖)
        (E-inv 𝓖) (E-inv-left 𝓖) (E-inv-right 𝓖)
        f

  h-resp-≋ : (s t : FA) → s ≋ t → h s ≈⟨ 𝓖 ⟩ h t
  h-resp-≋ []            []            _           = E-refl 𝓖 (h [])
  h-resp-≋ []            (x • t)       ()
  h-resp-≋ (x • s)       []            ()
  h-resp-≋ ((₀ , a) • s) ((₀ , b) • t) (refl , q , r) =
   E-is-congruence 𝓖 (f-resp q) (h-resp-≋ s t r)
  h-resp-≋ ((₁ , a) • s) ((₁ , b) • t) (refl , q , r) =
   E-is-congruence 𝓖 (≈-inv-cong (f a) (f b) (f-resp q)) (h-resp-≋ s t r)
  h-resp-≋ ((₀ , a) • s) ((₁ , b) • t) (() , q , r)
  h-resp-≋ ((₁ , a) • s) ((₀ , b) • t) (() , q , r)

  h-resp-≍ : (s t : FA) → s ≍ t → h s ≈⟨ 𝓖 ⟩ h t
  h-resp-≍ s t (∿-gives-≍ p)             = h-identifies-∿-related-points p
  h-resp-≍ s t (≋-gives-≍ p)             = h-resp-≋ s t p
  h-resp-≍ s t (≍-trans {s} {u} {t} p q) =
   E-trans 𝓖 (h s) (h u) (h t) (h-resp-≍ s u p) (h-resp-≍ u t q)

  free-map : ⟨ free-egroup-setoid ⟩ → ⟨ 𝓖 ⟩
  free-map = h

  free-map-is-hom : is-hom free-egroup-setoid 𝓖 free-map
  free-map-is-hom = (λ {x} {y} → h-resp-≍ x y)
                  , (λ {x} {y} → h-is-hom x y)

  free-map-triangle : (a : ∣ 𝔸 ∣) → free-map (η a) ≈⟨ 𝓖 ⟩ f a
  free-map-triangle a = E-unit-right 𝓖 (f a)

  free-map-is-unique : (g : ⟨ free-egroup-setoid ⟩ → ⟨ 𝓖 ⟩)
                     → is-hom free-egroup-setoid 𝓖 g
                     → ((a : ∣ 𝔸 ∣) → g (η a) ≈⟨ 𝓖 ⟩ f a)
                     → (s : ⟨ free-egroup-setoid ⟩) → g s ≈⟨ 𝓖 ⟩ free-map s
  free-map-is-unique g g-hom@(_ , g-mult) g-tri = u
   where
    g-pu : g [] ≈⟨ 𝓖 ⟩ E-unit 𝓖
    g-pu = homs-preserve-unit free-egroup-setoid 𝓖 g g-hom

    g-pi : (w : FA) → g (finv w) ≈⟨ 𝓖 ⟩ E-inv 𝓖 (g w)
    g-pi w = homs-preserve-inv free-egroup-setoid 𝓖 g g-hom w

    u : (s : FA) → g s ≈⟨ 𝓖 ⟩ free-map s
    u [] = g-pu
    u ((₀ , a) • s) =
     g (η a ◦ s)            ≈[ g-mult {η a} {s} ]
     g (η a) ·⟨ 𝓖 ⟩ g s     ≈[ E-is-congruence 𝓖 (g-tri a) (u s) ]
     f a ·⟨ 𝓖 ⟩ h s         ≈∎
    u ((₁ , a) • s) =
     g (finv (η a) ◦ s)          ≈[ g-mult {finv (η a)} {s} ]
     g (finv (η a)) ·⟨ 𝓖 ⟩ g s   ≈[ E-is-congruence 𝓖 lemma (u s) ]
     E-inv 𝓖 (f a) ·⟨ 𝓖 ⟩ h s    ≈∎
      where
       lemma : g (finv (η a)) ≈⟨ 𝓖 ⟩ E-inv 𝓖 (f a)
       lemma = g (finv (η a))    ≈[ g-pi (η a) ]
               E-inv 𝓖 (g (η a)) ≈[ ≈-inv-cong (g (η a)) (f a) (g-tri a) ]
               E-inv 𝓖 (f a)     ≈∎

\end{code}

As an immediate corollary, two homomorphisms out of the free egroup
that both extend f agree up to the equivalence relation.

\begin{code}

  free-map-is-unique₂ : (g₀ g₁ : ⟨ free-egroup-setoid ⟩ → ⟨ 𝓖 ⟩)
                      → is-hom free-egroup-setoid 𝓖 g₀
                      → is-hom free-egroup-setoid 𝓖 g₁
                      → ((a : ∣ 𝔸 ∣) → g₀ (η a) ≈⟨ 𝓖 ⟩ f a)
                      → ((a : ∣ 𝔸 ∣) → g₁ (η a) ≈⟨ 𝓖 ⟩ f a)
                      → (s : ⟨ free-egroup-setoid ⟩) → g₀ s ≈⟨ 𝓖 ⟩ g₁ s
  free-map-is-unique₂ g₀ g₁ i₀ i₁ t₀ t₁ s =
   E-trans 𝓖 (g₀ s) (free-map s) (g₁ s)
    (free-map-is-unique g₀ i₀ t₀ s)
    (E-sym 𝓖 (g₁ s) (free-map s) (free-map-is-unique g₁ i₁ t₁ s))

\end{code}

The universal property as an adjunction: restriction along η and
extension are mutually inverse setoid maps between the hom-setoid out of
the free egroup and the setoid of setoid maps from 𝔸 into the underlying
setoid of the target. This is the free-forgetful adjunction between
setoids and EGroups.

\begin{code}

 free-adjunction-setoid : (𝓖 : EGroup 𝓥 𝓦)
                        → hom-setoid free-egroup-setoid 𝓖
                        ≅ˢ setoid-map-setoid 𝔸 (underlying-setoid 𝓖)
 free-adjunction-setoid 𝓖 = record
                              { to        = to
                              ; from      = from
                              ; to-resp   = λ {x} {y} → to-resp {x} {y}
                              ; from-resp = λ {x} {y} → from-resp {x} {y}
                              ; to-from   = ε
                              ; from-to   = θ
                              }
  where
   open universal-property 𝓖

   S = hom-setoid free-egroup-setoid 𝓖
   T = setoid-map-setoid 𝔸 (underlying-setoid 𝓖)

   to : ∣ S ∣ → ∣ T ∣
   to (g , g-resp , _) = (λ a → g (η a)) ,
                         (λ {a} {b} q → g-resp (≋-gives-≍ (η-≋ q)))

   from : ∣ T ∣ → ∣ S ∣
   from (f , f-resp) = free-map f f-resp , free-map-is-hom f f-resp

   to-resp : is-setoid-map S T to
   to-resp p a = p (η a)

   from-resp : is-setoid-map T S from
   from-resp {f , f-resp} {f' , f'-resp} p s =
    free-map-is-unique f' f'-resp (free-map f f-resp) (free-map-is-hom f f-resp)
     (λ a → E-trans 𝓖 (free-map f f-resp (η a)) (f a) (f' a)
             (free-map-triangle f f-resp a) (p a)) s

   ε : (𝕗 : ∣ T ∣) → to (from 𝕗) ≈⟦ T ⟧ 𝕗
   ε (f , f-resp) a = free-map-triangle f f-resp a

   θ : (u : ∣ S ∣) → from (to u) ≈⟦ S ⟧ u
   θ u@(g , g-hom) s =
    let (tf , tf-resp) = to u
    in E-sym 𝓖 (g s) (free-map tf tf-resp s)
        (free-map-is-unique tf tf-resp g g-hom (λ a → E-refl 𝓖 (g (η a))) s)

\end{code}