Martin Escardo
15 February 2021.
In collaboration with Marc Bezem, Thierry Coquand and Peter Dybjer.
This module has the technical lemmas necessary to prove the
following:
For any universe 𝓤, there is a group in the successor universe 𝓤⁺
which is not isomorphic to any group in 𝓤.
Of course, in the other direction, any group in 𝓤 has an isomorphic
copy in 𝓤⁺, so the above says that there are strictly more groups in
𝓤⁺ than in 𝓤.
In the module BuraliForti we use the group freely generated by
the (large but locally small) type of ordinals for that purpose.
We work in a spartan Martin-Löf type theory, with the assumption that
propositional truncations exist and that the univalence axiom
holds. No other features of HoTT/UF are needed.
In particular, quotients, which we use to construct free groups, are
constructed using propositional truncation and function extensionality
and propositional extensionality in the module UF.LargeQuotient. This
construction of quotients increases the universe level by one (but its
universal property eliminates into any universe), so that the group
freely generated by a type A in a universe 𝓤 lives in the next
universe 𝓤⁺ (but again its universal property eliminates into any
universe).
In this file with work with a given locally small type A : 𝓤⁺ for an
arbitrary universe 𝓤 and we show that the free group constructed in
the module Group.Free, which lives in the universe 𝓤⁺⁺, has a
copy in the same universe 𝓤⁺ where A lives, provided A is locally
small (meaning that its identity types, which live in 𝓤⁺, have
equivalent copies in 𝓤). Moreover, we show that if the group freely
generated by A has a copy in the universe 𝓤, then A itself must have a
copy in 𝓤. We then apply this in the module BuraliForti by
taking A to be the type of ordinals in the universe 𝓤, which doesn't
have a copy in 𝓤, from which we conclude that the free group also
doesn't have a copy in 𝓤.
For that purpose, we need to know, in particular, that the inclusion
of generators is injective, which is proved in the module
Group.Free. But this is is not enough: for example, the unique
map P → 𝟙 is an embedding if P is a proposition, and the terminal
type 𝟙 is of course small, but P doesn't need to be small - cf. work
with Tom de Jong on size matters https://arxiv.org/abs/2102.08812,
from which we borrow other techniques in the development below.
\begin{code}
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness --auto-inline #-}
open import MLTT.Spartan
open import UF.PropTrunc
open import UF.Univalence
module Groups.FreeOverLargeLocallySmallSet
(pt : propositional-truncations-exist)
(ua : Univalence)
where
open import UF.FunExt
open import UF.UA-FunExt
open import UF.Subsingletons
open import UF.Base
open import UF.Embeddings
open import UF.Equiv hiding (_≅_)
open import UF.EquivalenceExamples
open import UF.Size
open import MLTT.List
open import Groups.SRTclosure
open import Groups.Type
open import Groups.Free
fe : Fun-Ext
fe = Univalence-gives-Fun-Ext ua
pe : Prop-Ext
pe = Univalence-gives-Prop-Ext ua
open import UF.Large-Quotient pt fe pe
open FreeGroupInterface pt fe pe
\end{code}
The last three assumptions in the following module parameters are a
slight weakening of the local smallness condition on the type A.
\begin{code}
module resize-free-group
{𝓤 : Universe}
(A : 𝓤 ⁺ ̇)
(A-is-set : is-set A)
(_＝₀_ : A → A → 𝓤 ̇ )
(refl₀ : (a : A) → a ＝₀ a)
(from-＝₀ : (a b : A) → a ＝₀ b → a ＝ b)
where
open free-group-construction A
private
𝓤⁺ = 𝓤 ⁺
𝓤⁺⁺ = 𝓤⁺ ⁺
\end{code}
Our free group is constructed as a quotient of a set of words FA by a
certain equivalence relation _∾_ : FA → FA → 𝓤⁺. To reduce the size of
the quotient, we reduce the size of (propositional) values of this
equivalence relation using the assumed relation _＝₀_ and functions
refl₀ and from-＝₀.
At this point, in order to understand the following constructions, it
is necessary to first understand the constructions in the module
FreeGroup, because here we resize down several of the
constructions performed in that file, exploiting the (weakened version
of the) local smalless of the type A.
\begin{code}
_＝[X]_ : X → X → 𝓤 ̇
(m , a) ＝[X] (n , b) = (m ＝ n) × (a ＝₀ b)
from-＝[X] : {x y : X} → x ＝[X] y → x ＝ y
from-＝[X] {m , a} {n , b} (p , q) = to-×-＝ p (from-＝₀ a b q)
to-＝[X] : {x y : X} → x ＝ y → x ＝[X] y
to-＝[X] {m , a} {m , a} refl = refl , refl₀ a
_＝[FA]_ : FA → FA → 𝓤 ̇
[] ＝[FA] [] = 𝟙
[] ＝[FA] (y ∷ t) = 𝟘
(x ∷ s) ＝[FA] [] = 𝟘
(x ∷ s) ＝[FA] (y ∷ t) = (x ＝[X] y) × (s ＝[FA] t)
from-＝[FA] : {s t : FA} → s ＝[FA] t → s ＝ t
from-＝[FA] {[]} {[]} e = refl
from-＝[FA] {x ∷ s} {y ∷ t} (p , q) = ap₂ _∷_ (from-＝[X] p) (from-＝[FA] q)
to-＝[FA] : {s t : FA} → s ＝ t → s ＝[FA] t
to-＝[FA] {[]} {[]} p = ⋆
to-＝[FA] {x ∷ s} {y ∷ t} p = to-＝[X] (equal-heads p) ,
to-＝[FA] (equal-tails p)
_◗_ : FA → FA → 𝓤 ̇
[] ◗ t = 𝟘
(x ∷ []) ◗ t = 𝟘
(x ∷ y ∷ s) ◗ t = (y ＝[X] (x ⁻)) × (s ＝[FA] t)
_▶_ : FA → FA → 𝓤 ̇
[] ▶ t = 𝟘
(x ∷ s) ▶ [] = (x ∷ s) ◗ []
(x ∷ s) ▶ (y ∷ t) = ((x ∷ s) ◗ (y ∷ t)) + (x ＝[X] y × (s ▶ t))
▶-lemma : (x y : X) (s : List X) → y ＝ x ⁻ → (x ∷ y ∷ s) ▶ s
▶-lemma x _ [] refl = to-＝[X] {x ⁻} refl , ⋆
▶-lemma x _ (z ∷ s) refl = inl (to-＝[X] {x ⁻} refl ,
to-＝[X] {z} refl ,
to-＝[FA] {s} refl)
\end{code}
The reduction relation _▷_ is defined in the module FreeGroup,
and its propositional, symmetric, reflexive, transitive closure gives
the relation _∾_ that we use in order to quotient the type FA to get
the group freely generated by A.
We now show that _▶_ defined above is logically equivalent to _▷_.
\begin{code}
▶-gives-▷ : {s t : FA} → s ▶ t → s ▷ t
▶-gives-▷ {[]} {t} r = 𝟘-elim r
▶-gives-▷ {x ∷ y ∷ s} {[]} (p , q) = [] , s , x ,
ap (λ - → x ∷ - ∷ s) (from-＝[X] p) ,
((from-＝[FA] q)⁻¹)
▶-gives-▷ {x ∷ y ∷ s} {z ∷ t} (inl (p , q)) = γ (from-＝[X] p) (from-＝[FA] q)
where
γ : y ＝ x ⁻ → s ＝ z ∷ t → x ∷ y ∷ s ▷ z ∷ t
γ p q = [] , s , x , ap (λ - → x ∷ (- ∷ s)) p , (q ⁻¹)
▶-gives-▷ {x ∷ s} {y ∷ t} (inr (p , r)) = γ (from-＝[X] p) IH
where
IH : s ▷ t
IH = ▶-gives-▷ r
γ : x ＝ y → s ▷ t → (x ∷ s) ▷ (y ∷ t)
γ refl = ∷-▷ x
▷-gives-▶ : {s t : FA} → s ▷ t → s ▶ t
▷-gives-▶ (u , v , x , refl , refl) = f u v x
where
f : (u v : FA) (x : X) → (u ++ [ x ] ++ [ x ⁻ ] ++ v) ▶ (u ++ v)
f [] [] x = to-＝[X] {x ⁻} refl , ⋆
f [] (y ∷ v) x = inl (to-＝[X] {x ⁻} refl , to-＝[X] {y} refl , to-＝[FA] {v} refl)
f (y ∷ u) v x = inr (to-＝[X] {y} refl , f u v x)
\end{code}
The usual way to define the transitive closure of a relation (cf. the
file SRTclosure) applied to the relation _▶_ would increase
universe levels back to those of the relation _∾_.
In order to overcome this obstacle, we consider a type of redexes.
\begin{code}
redex : FA → 𝓤 ̇
redex [] = 𝟘
redex (x ∷ []) = 𝟘
redex (x ∷ y ∷ s) = (y ＝[X] (x ⁻)) + redex (y ∷ s)
reduct : (s : FA) → redex s → FA
reduct (x ∷ y ∷ s) (inl p) = s
reduct (x ∷ y ∷ s) (inr r) = x ∷ reduct (y ∷ s) r
\end{code}
The idea behind the above definitions is that we want that the
relation s ▶ t holds if and only the word t is the reduct of s at some
redex r, which is what we prove next:
\begin{code}
lemma-reduct→ : (s : FA) (r : redex s) → s ▶ reduct s r
lemma-reduct→ (x ∷ y ∷ s) (inl p) = ▶-lemma x y s (from-＝[X] p)
lemma-reduct→ (x ∷ y ∷ s) (inr r) = inr (to-＝[X] {x} refl ,
lemma-reduct→ (y ∷ s) r)
lemma-reduct← : (s t : FA) → s ▶ t → Σ r ꞉ redex s , reduct s r ＝ t
lemma-reduct← (x ∷ []) (z ∷ t) (inl ())
lemma-reduct← (x ∷ []) (z ∷ t) (inr ())
lemma-reduct← (x ∷ y ∷ s) [] (p , q) = inl p , from-＝[FA] q
lemma-reduct← (x ∷ y ∷ s) (z ∷ t) (inl (p , q)) = inl p , from-＝[FA] q
lemma-reduct← (x ∷ y ∷ s) (z ∷ t) (inr (p , r)) = inr (pr₁ IH) ,
ap₂ _∷_ (from-＝[X] p) (pr₂ IH)
where
IH : Σ r ꞉ redex (y ∷ s) , reduct (y ∷ s) r ＝ t
IH = lemma-reduct← (y ∷ s) t r
\end{code}
Next we define a type of chains of redexes of length n and a
corresponding notion of reduct for such chains:
\begin{code}
redex-chain : ℕ → FA → 𝓤 ̇
redex-chain 0 s = 𝟙
redex-chain (succ n) s = Σ r ꞉ redex s , redex-chain n (reduct s r)
chain-reduct : (s : FA) (n : ℕ) → redex-chain n s → FA
chain-reduct s 0 ρ = s
chain-reduct s (succ n) (r , ρ) = chain-reduct (reduct s r) n ρ
chain-lemma→ : (s : FA) (n : ℕ) (ρ : redex-chain n s) → s ▷[ n ] chain-reduct s n ρ
chain-lemma→ s 0 ρ = refl
chain-lemma→ s (succ n) (r , ρ) = reduct s r ,
▶-gives-▷ (lemma-reduct→ s r) ,
chain-lemma→ (reduct s r) n ρ
chain-lemma← : (s t : FA) (n : ℕ)
→ s ▷[ n ] t
→ Σ ρ ꞉ redex-chain n s , chain-reduct s n ρ ＝ t
chain-lemma← s t 0 r = ⋆ , r
chain-lemma← s t (succ n) (u , b , c) = γ IH l
where
IH : Σ ρ ꞉ redex-chain n u , chain-reduct u n ρ ＝ t
IH = chain-lemma← u t n c
l : Σ r ꞉ redex s , reduct s r ＝ u
l = lemma-reduct← s u (▷-gives-▶ b)
γ : type-of IH
→ type-of l
→ Σ ρ' ꞉ redex-chain (succ n) s , chain-reduct s (succ n) ρ' ＝ t
γ (ρ , refl) (r , refl) = (r , ρ) , refl
\end{code}
And with this we obtain a relation _≏_ whose propositional truncation
will be logically equivalent to the equivalence relation _∾_ used to
quotient FA to get the group freely generated by A. The relation _∾_
itself is the propositional truncation of a suitable relation _∿_,
which we now use for that purpose.
\begin{code}
_≏_ : FA → FA → 𝓤 ̇
s ≏ t = Σ m ꞉ ℕ ,
Σ n ꞉ ℕ ,
Σ ρ ꞉ redex-chain m s ,
Σ σ ꞉ redex-chain n t , chain-reduct s m ρ ＝[FA] chain-reduct t n σ
≏-gives-∿ : (s t : FA) → s ≏ t → s ∿ t
≏-gives-∿ s t (m , n , ρ , σ , p) = γ
where
a : s ▷⋆ chain-reduct s m ρ
a = m , chain-lemma→ s m ρ
b : t ▷⋆ chain-reduct t n σ
b = n , chain-lemma→ t n σ
c : Σ u ꞉ FA , (s ▷⋆ u) × (t ▷⋆ u)
c = chain-reduct t n σ , transport (s ▷⋆_) (from-＝[FA] p) a , b
γ : s ∿ t
γ = to-∿ s t c
∿-gives-≏ : (s t : FA) → s ∿ t → s ≏ t
∿-gives-≏ s t e = γ a
where
a : Σ u ꞉ FA , (s ▷⋆ u) × (t ▷⋆ u)
a = from-∿ Church-Rosser s t e
γ : type-of a → s ≏ t
γ (u , (m , ρ) , (n , σ)) = δ b c
where
b : Σ ρ ꞉ redex-chain m s , chain-reduct s m ρ ＝ u
b = chain-lemma← s u m ρ
c : Σ σ ꞉ redex-chain n t , chain-reduct t n σ ＝ u
c = chain-lemma← t u n σ
δ : type-of b → type-of c → s ≏ t
δ (ρ , p) (σ , q) = m , n , ρ , σ , to-＝[FA] (p ∙ q ⁻¹)
open free-group-construction-step₁ pt
_∥≏∥_ : FA → FA → 𝓤 ̇
s ∥≏∥ t = ∥ s ≏ t ∥
∾-is-logically-equivalent-to-∥≏∥ : (s t : FA) → s ∾ t ⇔ s ∥≏∥ t
∾-is-logically-equivalent-to-∥≏∥ s t = ∥∥-functor (∿-gives-≏ s t) ,
∥∥-functor (≏-gives-∿ s t)
\end{code}
And so we also get a type equivalence, because logically equivalent
propositions are equivalent types:
\begin{code}
∿-is-equivalent-to-∥≏∥ : (s t : FA) → (s ∾ t) ≃ (s ∥≏∥ t)
∿-is-equivalent-to-∥≏∥ s t = logically-equivalent-props-are-equivalent
∥∥-is-prop
∥∥-is-prop
(lr-implication (∾-is-logically-equivalent-to-∥≏∥ s t))
(rl-implication (∾-is-logically-equivalent-to-∥≏∥ s t))
\end{code}
Being logically equivalent to an equivalence relation, the relation
∥≏∥ is itself an equivalence relation (this is proved in the module
SRT).
\begin{code}
open free-group-construction-step₂ fe pe
-∥≏∥- : EqRel {𝓤⁺} {𝓤} FA
-∥≏∥- = _∥≏∥_ , is-equiv-rel-transport _∾_ _∥≏∥_ (λ s t → ∥∥-is-prop)
∾-is-logically-equivalent-to-∥≏∥ ∾-is-equiv-rel
\end{code}
By a general construction in the module UF.LargeQuotient, we conclude
that FA/∾ ≃ FA/∥≏∥. What is crucial for our purposes is that FA/∥≏∥
lives in the lower universe 𝓤⁺, as opposed to the original quotient
FA/∾, which lives in the higher universe 𝓤⁺⁺.
\begin{code}
FA/∥≏∥ : 𝓤⁺ ̇
FA/∥≏∥ = FA / -∥≏∥-
FA/∾-is-equivalent-to-FA/∥≏∥ : FA/∾ ≃ FA/∥≏∥
FA/∾-is-equivalent-to-FA/∥≏∥ = quotients-equivalent FA -∾- -∥≏∥-
(λ {s} {t} → ∾-is-logically-equivalent-to-∥≏∥ s t)
native-universe-of-free-group : universe-of ⟨ free-group A ⟩ ＝ 𝓤 ⁺⁺
native-universe-of-free-group = refl
resized-free-group-carrier : ⟨ free-group A ⟩ is 𝓤⁺ small
resized-free-group-carrier = γ
where
γ : Σ F ꞉ 𝓤⁺ ̇ , F ≃ ⟨ free-group A ⟩
γ = FA/∥≏∥ , ≃-sym FA/∾-is-equivalent-to-FA/∥≏∥
\end{code}
With this we get the proof of the first lemma needed for the main
theorem in this module. This relies on transporting group structures
along equivalences, which is implemented in the module Group.Type
(unfortunately, one cannot apply univalence for that purpose, because
the types live in different universes and hence one can't form their
identity type, and so this transport has to be done manually).
\begin{code}
small-free-group : Σ F ꞉ Group 𝓤⁺ , F ≅ free-group A
small-free-group = resized-group (free-group A) resized-free-group-carrier
\end{code}
NB. If we assume cumulativity in our type theory, the above can be
done with univalence directly. TODO. Write down the proof here in
English (and perhaps also in Agda using --cumulativity).
We say that a type has size 𝓥 if it is equivalent to some type in the
universe 𝓥, and that a map has size 𝓥 if its fibers all have size 𝓥.
See the module UF.Size. This notion of size for maps is
introduced and developed in the paper https://arxiv.org/abs/2102.08812
by Tom de Jong and Martin Escardo.
The native size of the universal map ηᴳʳᵖ : A → FA/∾ into the free
group is rather large - it jumps up two universe levels:
\begin{code}
ηᴳʳᵖ-native-size : ηᴳʳᵖ is 𝓤⁺⁺ small-map
ηᴳʳᵖ-native-size y = fiber ηᴳʳᵖ y , ≃-refl _
\end{code}
Using the above development, we can make it smaller.
In the following, the function η/∾ : FA → FA/∾ is the universal map
into the quotient (constructed in the module Groups.FreeGroup), and, by
definition, the universal map ηᴳʳᵖ : A → FA/∾ into the free group is
the composite η/∾ ∘ η where η : A → FA is the insertion of generators
before quotienting.
The following result is proved by quotient induction, which says that
in order to prove a property of all elements of the quotient, it
suffices to prove it for elements of the form η/∾ s with s : FA.
\begin{code}
ηᴳʳᵖ-is-medium : ηᴳʳᵖ is 𝓤⁺ small-map
ηᴳʳᵖ-is-medium = /-induction -∾- (λ y → fiber ηᴳʳᵖ y is 𝓤⁺ small)
(λ y → being-small-is-prop ua (fiber ηᴳʳᵖ y) 𝓤⁺) γ
where
e : (a : A) (s : FA) → (η/∾ (η a) ＝ η/∾ s) ≃ (η a ∥≏∥ s)
e a s = (η/∾ (η a) ＝ η/∾ s) ≃⟨ I ⟩
(η a ∾ s) ≃⟨ II ⟩
(η a ∥≏∥ s) ■
where
I = logically-equivalent-props-are-equivalent
(quotient-is-set -∾-)
∥∥-is-prop
η/∾-relates-identified-points
η/∾-identifies-related-points
II = ∿-is-equivalent-to-∥≏∥ (η a) s
d : (s : FA) → fiber ηᴳʳᵖ (η/∾ s) ≃ (Σ a ꞉ A , η a ∥≏∥ s)
d s = (Σ a ꞉ A , η/∾ (η a) ＝ η/∾ s) ≃⟨ Σ-cong (λ a → e a s) ⟩
(Σ a ꞉ A , η a ∥≏∥ s) ■
γ : (s : FA) → fiber ηᴳʳᵖ (η/∾ s) is 𝓤⁺ small
γ s = (Σ a ꞉ A , η a ∥≏∥ s) , ≃-sym (d s)
where
notice : universe-of (fiber ηᴳʳᵖ (η/∾ s)) ＝ 𝓤⁺⁺
notice = refl
\end{code}
But the above resizing of the map ηᴳʳᵖ is not small enough for our
purposes.
The fiber type Σ a ꞉ A , η a ＝ s lives in the universe 𝓤⁺. In the next
step we construct a copy of this fiber type in the first universe 𝓤₀.
The following construction also shows that the map η : A → FA has
decidable fibers, which is used implicitly in our definitions by
pattern matching.
\begin{code}
native-universe-fiber-η : (s : FA) → universe-of (Σ a ꞉ A , η a ＝ s) ＝ 𝓤⁺
native-universe-fiber-η s = refl
fiber₀-η : FA → 𝓤₀ ̇
fiber₀-η [] = 𝟘
fiber₀-η (x ∷ y ∷ s) = 𝟘
fiber₀-η ((₀ , a) ∷ []) = 𝟙
fiber₀-η ((₁ , a) ∷ []) = 𝟘
NB-fiber₀-η-is-decidable : (s : FA) → fiber₀-η s + ¬ (fiber₀-η s)
NB-fiber₀-η-is-decidable [] = inr id
NB-fiber₀-η-is-decidable (x ∷ y ∷ s) = inr id
NB-fiber₀-η-is-decidable ((₀ , a) ∷ []) = inl ⋆
NB-fiber₀-η-is-decidable ((₁ , a) ∷ []) = inr id
fiber-η→ : (s : FA) → fiber₀-η s → (Σ a ꞉ A , η a ＝ s)
fiber-η→ [] ()
fiber-η→ (x ∷ y ∷ s) ()
fiber-η→ (₀ , a ∷ []) ⋆ = a , refl
fiber-η→ (₁ , a ∷ []) ()
fiber-η← : (s : FA) → (Σ a ꞉ A , η a ＝ s) → fiber₀-η s
fiber-η← .(η a) (a , refl) = ⋆
η-fiber₀-η : (a : A) → fiber₀-η (η a)
η-fiber₀-η a = ⋆
\end{code}
Using this, next we want to reduce the size of the type
Σ a ꞉ A , η a ∾ s, which we informally refer to
as "the ∾-fiber of s over η".
\begin{code}
generator : FA → 𝓤 ̇
generator s = Σ n ꞉ ℕ , Σ ρ ꞉ redex-chain n s , fiber₀-η (chain-reduct s n ρ)
is-generator : FA → 𝓤 ̇
is-generator s = ∥ generator s ∥
the-∾-fibers-of-η-are-props : (s : FA) → is-prop (Σ a ꞉ A , η a ∾ s)
the-∾-fibers-of-η-are-props s (a , e) (a' , e') = γ
where
α : η a ∾ η a'
α = psrt-transitive (η a) s (η a') e (psrt-symmetric (η a') s e')
β : a ＝ a'
β = η-identifies-∾-related-points A-is-set α
γ : (a , e) ＝ (a' , e')
γ = to-subtype-＝ (λ x → ∥∥-is-prop) β
∾-fiber-η-lemma→ : (s : FA) → (Σ a ꞉ A , η a ∾ s) → is-generator s
∾-fiber-η-lemma→ s (a , e) = ∥∥-functor γ e
where
γ : η a ∿ s → Σ n ꞉ ℕ , Σ ρ ꞉ redex-chain n s , fiber₀-η (chain-reduct s n ρ)
γ e = δ (d c)
where
c : Σ u ꞉ FA , (η a ▷⋆ u) × (s ▷⋆ u)
c = from-∿ Church-Rosser (η a) s e
d : type-of c → Σ n ꞉ ℕ , Σ ρ ꞉ redex-chain n s , chain-reduct s n ρ ＝ η a
d (u , r , r₁) = δ r₂
where
p : η a ＝ u
p = η-irreducible⋆ r
r₂ : s ▷⋆ η a
r₂ = transport (s ▷⋆_) (p ⁻¹) r₁
δ : s ▷⋆ η a → Σ n ꞉ ℕ , Σ ρ ꞉ redex-chain n s , chain-reduct s n ρ ＝ η a
δ (n , r₃) = (n , chain-lemma← s (η a) n r₃)
δ : type-of (d c) → codomain γ
δ (n , ρ , p) = n , ρ , transport fiber₀-η (p ⁻¹) (η-fiber₀-η a)
∾-fiber-η-lemma← : (s : FA) → is-generator s → (Σ a ꞉ A , η a ∾ s)
∾-fiber-η-lemma← s = ∥∥-rec (the-∾-fibers-of-η-are-props s) γ
where
γ : generator s → (Σ a ꞉ A , η a ∾ s)
γ (n , ρ , i) = δ σ
where
r : s ▷[ n ] chain-reduct s n ρ
r = chain-lemma→ s n ρ
e : chain-reduct s n ρ ∾ s
e = ∣ to-∿ (chain-reduct s n ρ) s (chain-reduct s n ρ , (0 , refl) , (n , r)) ∣
σ : Σ a ꞉ A , η a ＝ chain-reduct s n ρ
σ = fiber-η→ (chain-reduct s n ρ) i
δ : type-of σ → Σ a ꞉ A , η a ∾ s
δ (a , p) = a , transport (_∾ s) (p ⁻¹) e
\end{code}
And this is the desired size reduction:
\begin{code}
∾-fiber-η-lemma : (s : FA) → (Σ a ꞉ A , η a ∾ s) ≃ is-generator s
∾-fiber-η-lemma s = logically-equivalent-props-are-equivalent
(the-∾-fibers-of-η-are-props s)
∥∥-is-prop
(∾-fiber-η-lemma→ s)
(∾-fiber-η-lemma← s)
\end{code}
With this we can further reduce the size of the universal map ηᴳʳᵖ:
\begin{code}
ηᴳʳᵖ-is-small : ηᴳʳᵖ is 𝓤 small-map
ηᴳʳᵖ-is-small = /-induction -∾- (λ y → fiber ηᴳʳᵖ y is 𝓤 small)
(λ y → being-small-is-prop ua (fiber ηᴳʳᵖ y) 𝓤) γ
where
e : (a : A) (s : FA) → (η/∾ (η a) ＝ η/∾ s) ≃ (η a ∾ s)
e a s = logically-equivalent-props-are-equivalent
(quotient-is-set -∾-)
∥∥-is-prop
η/∾-relates-identified-points
η/∾-identifies-related-points
d : (s : FA) → fiber ηᴳʳᵖ (η/∾ s) ≃ is-generator s
d s = (Σ a ꞉ A , η/∾ (η a) ＝ η/∾ s) ≃⟨ Σ-cong (λ a → e a s) ⟩
(Σ a ꞉ A , η a ∾ s) ≃⟨ ∾-fiber-η-lemma s ⟩
is-generator s ■
γ : (s : FA) → fiber ηᴳʳᵖ (η/∾ s) is 𝓤 small
γ s = is-generator s , ≃-sym (d s)
\end{code}
A result by Tom de Jong and Martin Escardo (https://arxiv.org/abs/2102.08812),
recorded in the module UF.Size and recently submitted for
publication in a paper about size, says that if a map has size 𝓥, and
if also its codomain has size 𝓥, then so does its domain.
\begin{code}
free-group-small-gives-generating-set-small : ⟨ free-group A ⟩ is 𝓤 small
→ A is 𝓤 small
free-group-small-gives-generating-set-small h = size-contravariance ηᴳʳᵖ ηᴳʳᵖ-is-small h
\end{code}
It follows that if there is a large, locally small set, then there is
a large group:
\begin{code}
large-group-with-no-small-copy : (Σ A ꞉ 𝓤 ⁺ ̇ , is-set A
× is-large A
× is-locally-small A)
→ Σ F ꞉ Group (𝓤 ⁺) , ((G : Group 𝓤) → ¬ (G ≅ F))
large-group-with-no-small-copy {𝓤} (A , A-is-set , A-is-large , A-ls) = δ
where
open resize-free-group A A-is-set Id⟦ A-ls ⟧ (λ _ → ⟦ A-ls ⟧-refl) (λ _ _ p → ＝⟦ A-ls ⟧-gives-＝ p)
γ : (Σ F ꞉ Group (𝓤 ⁺) , F ≅ free-group A)
→ (Σ F ꞉ Group (𝓤 ⁺) , ((G : Group 𝓤) → ¬ (G ≅ F)))
γ (F , f , f-is-equiv , f-is-hom) = F , β
where
β : (G : Group 𝓤) → G ≅ F → 𝟘
β G (g , g-is-equiv , g-is-hom) = α
where
h : ⟨ free-group A ⟩ is 𝓤 small
h = ⟨ G ⟩ , f ∘ g , ∘-is-equiv g-is-equiv f-is-equiv
α : 𝟘
α = A-is-large (free-group-small-gives-generating-set-small h)
δ : codomain γ
δ = γ small-free-group
\end{code}
In the module BuraliForti we instantiate A to the type of
ordinals, which is large and locally small, to construct a large group
with no small copy.