Martin Escardo, July 2026.

Given a large, locally small setoid, we show that the free egroup on it
is large, in the sense that no egroup whose underlying type and
equivalence relation are both small is isomorphic to it.

We then give an example, which is what the EGroups development is for,
by taking the universe as a setoid under type equivalence.

\begin{code}

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

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

module EGroups.Large where

open import UF.Equiv hiding (_β‰…_)
open import UF.Size
open import Relations.SRTclosure
open import Various.LawvereFPT

open import EGroups.Setoid
open import EGroups.Type
open import EGroups.Size

module large-free-egroup
        {𝓀 : Universe}
        (A : 𝓀 ⁺ Μ‡ )
        (_β‰ˆ_ : A β†’ A β†’ 𝓀 Μ‡ )
        (β‰ˆr : reflexive  _β‰ˆ_)
        (β‰ˆs : symmetric  _β‰ˆ_)
        (β‰ˆt : transitive _β‰ˆ_)
       where

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

\end{code}

We introduce the setoid of generators, together with three lemmas.
First, β‰ˆ-related generators are convertible, via a β–·-peak. Second, if
two generators are β‰ˆ[FA]-related, then their underlying unsigned
elements are β‰ˆ-related. Third, a generator witness for s exhibits s as
convertible to a single generator.

\begin{code}

 𝔸 : Setoid (𝓀 ⁺) 𝓀
 𝔸 = A , _β‰ˆ_ , β‰ˆr , β‰ˆs , β‰ˆt

 Ξ·-∿ : (a a' : A) β†’ a β‰ˆ a' β†’ Ξ· a ∿ Ξ· a'
 Ξ·-∿ a a' e = srt-transitive _β–·_ (Ξ· a) w (Ξ· a')
               (srt-symmetric _β–·_ w (Ξ· a) (srt-extension _β–·_ w (Ξ· a) I))
               (srt-extension _β–·_ w (Ξ· a') I')
  where
   w : FA
   w = (β‚€ , a) β€’ (₁ , a') β€’ (β‚€ , a') β€’ []

   I' : w β–· Ξ· a'
   I' = [] ,
       ((β‚€ , a') β€’ []) ,
       (β‚€ , a) ,
       (₁ , a') ,
       refl ,
       refl ,
       (refl , β‰ˆs a a' e)

   I : w β–· Ξ· a
   I = ((β‚€ , a) β€’ []) ,
        [] ,
        (₁ , a') ,
        (β‚€ , a') ,
        refl ,
        refl , (
        refl , β‰ˆr a')

 Ξ·-β‰ˆ[FA]β†’β‰ˆ : {a a' : A} β†’ Ξ· a β‰ˆ[FA] Ξ· a' β†’ a β‰ˆ a'
 Ξ·-β‰ˆ[FA]β†’β‰ˆ ((_ , e) , _) = e

 generatorβ†’βˆΏ : (s : FA) (w : generator s) β†’ s ∿ Ξ· (underlying-generator w)
 generatorβ†’βˆΏ s (n , ρ , a , p) = rt-gives-srt _β–·_ s (Ξ· a) (n , I)
  where
   I : iteration _β–·_ n s (Ξ· a)
   I = transport (iteration _β–·_ n s) (p ⁻¹) (chain-lemmaβ†’ s n ρ)

\end{code}

We now prove the theorem. If some egroup 𝓖 whose underlying type and
equivalence relation are both small is isomorphic to the free egroup,
then 𝔸 is a small setoid. The map ΞΊ = G ∘ Ξ· into βŸ¨π“–βŸ© is both
β‰ˆ-respecting and β‰ˆ-reflecting, so 𝔸 is setoid-isomorphic to the small
setoid of generators inside βŸ¨π“–βŸ©.

\begin{code}

 small-copy-gives-small-setoid
  : (𝓖 : EGroup 𝓀 𝓀) β†’ 𝓖 β‰… free-egroup β†’ is-small-setoid 𝓀 𝔸
 small-copy-gives-small-setoid 𝓖 (F , (F-resp , _) , G , (G-resp , _) , FG , GF)
  = T , iso
  where
   ΞΊ : A β†’ ⟨ 𝓖 ⟩
   ΞΊ a = G (Ξ· a)

   ΞΊ-respects : (a a' : A) β†’ a β‰ˆ a' β†’ ΞΊ a β‰ˆβŸ¨ 𝓖 ⟩ ΞΊ a'
   κ-respects a a' e = G-resp (η-∿ a a' e)

   ΞΊ-reflects : (a a' : A) β†’ ΞΊ a β‰ˆβŸ¨ 𝓖 ⟩ ΞΊ a' β†’ a β‰ˆ a'
   ΞΊ-reflects a a' r =
    Ξ·-β‰ˆ[FA]β†’β‰ˆ
     (η-identifies-∿-related-points a a'
       (srt-transitive _β–·_ (Ξ· a) (F (G (Ξ· a'))) (Ξ· a')
         (srt-transitive _β–·_ (Ξ· a) (F (G (Ξ· a))) (F (G (Ξ· a')))
           (srt-symmetric _β–·_ (F (G (Ξ· a))) (Ξ· a) (FG (Ξ· a)))
           (F-resp r))
         (FG (Ξ· a'))))

   abstract
    is-gen : ⟨ 𝓖 ⟩ β†’ 𝓀 Μ‡
    is-gen y = resized (generator (F y)) (generator-is-small (F y))

    to-gen : (y : ⟨ 𝓖 ⟩) β†’ is-gen y β†’ generator (F y)
    to-gen y = ⌜ resizing-condition (generator-is-small (F y)) ⌝

    from-gen : (y : ⟨ 𝓖 ⟩) β†’ generator (F y) β†’ is-gen y
    from-gen y = ⌜ resizing-condition (generator-is-small (F y)) ⌝⁻¹

    to-from-gen : (y : ⟨ 𝓖 ⟩) (w : generator (F y))
                β†’ to-gen y (from-gen y w) ＝ w
    to-from-gen y =
     inverses-are-sections
      ⌜ resizing-condition (generator-is-small (F y)) ⌝
      (⌜⌝-is-equiv (resizing-condition (generator-is-small (F y))))

   ∣T∣ : 𝓀 Μ‡
   ∣T∣ = Ξ£ y κž‰ ⟨ 𝓖 ⟩ , is-gen y

   _β‰ˆα΅€_ : ∣T∣ β†’ ∣T∣ β†’ 𝓀 Μ‡
   (y , _) β‰ˆα΅€ (y' , _) = y β‰ˆβŸ¨ 𝓖 ⟩ y'

   T : Setoid 𝓀 𝓀
   T = ∣T∣
     , _β‰ˆα΅€_
     , (Ξ» (y , _) β†’ erefl 𝓖 y)
     , (Ξ» (y , _) (y' , _) r β†’ esym 𝓖 y y' r)
     , (Ξ» (y , _) (y' , _) (y'' , _) r r' β†’ etrans 𝓖 y y' y'' r r')

   gen-of : (a : A) β†’ generator (F (ΞΊ a))
   gen-of a = βˆΏβ†’generator (srt-symmetric _β–·_ (F (G (Ξ· a))) (Ξ· a) (FG (Ξ· a)))

   to : A β†’ ∣T∣
   to a = ΞΊ a , from-gen (ΞΊ a) (gen-of a)

   from : ∣T∣ β†’ A
   from (y , w) = underlying-generator (to-gen y w)

   to-resp : is-setoid-map 𝔸 T to
   to-resp {a} {a'} e = ΞΊ-respects a a' e

   from-resp : is-setoid-map T 𝔸 from
   from-resp {y , w} {y' , w'} r =
    Ξ·-β‰ˆ[FA]β†’β‰ˆ
     (η-identifies-∿-related-points (from (y , w)) (from (y' , w'))
       (srt-transitive _β–·_ (Ξ· (from (y , w))) (F y') (Ξ· (from (y' , w')))
         (srt-transitive _β–·_ (Ξ· (from (y , w))) (F y) (F y')
           (srt-symmetric _β–·_ (F y) (Ξ· (from (y , w)))
             (generatorβ†’βˆΏ (F y) (to-gen y w)))
           (F-resp r))
         (generatorβ†’βˆΏ (F y') (to-gen y' w'))))

   to-from : (t : ∣T∣) β†’ to (from t) β‰ˆα΅€ t
   to-from (y , w) =
    etrans 𝓖 (ΞΊ aβ‚€) (G (F y)) y
      (esym 𝓖 (G (F y)) (ΞΊ aβ‚€) (G-resp (generatorβ†’βˆΏ (F y) (to-gen y w))))
      (GF y)
    where
     aβ‚€ : A
     aβ‚€ = underlying-generator (to-gen y w)

   from-to : (a : A) β†’ from (to a) β‰ˆ a
   from-to a =
    transport (Ξ» z β†’ z β‰ˆ a)
     (ap (underlying-generator {F (κ a)}) ((to-from-gen (κ a) (gen-of a)) ⁻¹))
     (underlying-generator-βˆΏβ†’generator
       (srt-symmetric _β–·_ (F (G (Ξ· a))) (Ξ· a) (FG (Ξ· a))))

   iso : 𝔸 β‰…Λ’ T
   iso = record
          { to        = to
          ; from      = from
          ; to-resp   = to-resp
          ; from-resp = from-resp
          ; to-from   = to-from
          ; from-to   = from-to
          }

\end{code}

Taking the contrapositive, if 𝔸 is a large setoid then the free egroup
on 𝔸, which lives in the next universe, has no small copy.

\begin{code}

 large-setoid-gives-large-egroup
  : is-large-setoid 𝓀 𝔸
  β†’ (𝓖 : EGroup 𝓀 𝓀) β†’ Β¬ (𝓖 β‰… free-egroup)
 large-setoid-gives-large-egroup 𝔸-large 𝓖 iso
  = 𝔸-large (small-copy-gives-small-setoid 𝓖 iso)

 there-is-a-large-egroup
  : is-large-setoid 𝓀 𝔸
  β†’ Ξ£ 𝓕 κž‰ EGroup (𝓀 ⁺) (𝓀 ⁺) , ((𝓖 : EGroup 𝓀 𝓀) β†’ Β¬ (𝓖 β‰… 𝓕))
 there-is-a-large-egroup 𝔸-large
  = free-egroup , large-setoid-gives-large-egroup 𝔸-large

\end{code}

An example of a large egroup, which is what the EGroups development is for.

We instantiate the above with the universe 𝓀, taken as a setoid
under type equivalence _≃_. This gives an egroup in the next universe
𝓀⁺ that is isomorphic to no egroup in the universe 𝓀, in a Spartan
MLTT with no HoTT/UF assumptions.

\begin{code}

module _ (𝓀 : Universe) where

 open large-free-egroup
       (𝓀 Μ‡ ) _≃_ ≃-refl (Ξ» X Y β†’ ≃-sym) (Ξ» X Y Z β†’ _●_)
      renaming (𝔸 to π•Œ)

\end{code}

The universe setoid π•Œ = (𝓀 Μ‡ , _≃_) is large.

\begin{code}

 universe-setoid-is-large : is-large-setoid 𝓀 π•Œ
 universe-setoid-is-large (T , iso) =
  generalized-Coquand.Lemmaβ‚‚ ∣ T ∣
   (_β‰…Λ’_.from iso) (_β‰…Λ’_.to iso) (_β‰…Λ’_.from-to iso)

\end{code}

Therefore the free egroup on the universe setoid, which lives in the
next universe, is isomorphic to no egroup whose underlying type and
equivalence relation are both small.

\begin{code}

 large-egroup-in-the-next-universe
  : Ξ£ 𝓕 κž‰ EGroup (𝓀 ⁺) (𝓀 ⁺) , ((𝓖 : EGroup 𝓀 𝓀) β†’ Β¬ (𝓖 β‰… 𝓕))
 large-egroup-in-the-next-universe
  = there-is-a-large-egroup universe-setoid-is-large

\end{code}