Martin Escardo
January - February 2021, with a modularization of the presentation September 2023.
In collaboration with Marc Bezem, Thierry Coquand and Peter Dybjer.
We construct free groups in HoTT/UF in Agda notation without HIT's
other than propositional truncation, and optionally quotient types,
but quotients are not really necessary, although they make the proofs
marginally shorter.
This is based on the book [1]. It is noteworthy and surprising that
the set of generators is not required to have decidable equality.
One application of free groups in this development is to show,
constructively, that "there are more groups in the next universe", in
the sense that for any universe 𝓤 there is a group in the next
universe 𝓤⁺ which is not isomorphic to any group in 𝓤. See the modules
Groups.Large and Ordinals.BuraliForti.
For this particular application, it is important that
1. The insertion of generators, or universal map, into the free group
is injective, and hence an embedding in the sense of HoTT/UF if
the type of generators is a set (its fibers are subsingletons).
2. The universal map is sufficiently small (its fibers are
sufficiently small).
Condition (1) follows automatically from [1]. For condition (2) we
need more work, which is explained below.
[1] Ray Mines, Fred Richman and Wim Ruitenburg. "A course in
constructive algebra", 1988.
https://doi.org/10.1007/978-1-4419-8640-5
\begin{code}
{-# OPTIONS --safe --without-K --no-exact-split --lossy-unification #-}
module Groups.Free where
open import Groups.Type
open import MLTT.List
renaming (_∷_ to _•_ ;
_++_ to _◦_ ;
++-assoc to ◦-assoc)
open import MLTT.Spartan
open import MLTT.Two-Properties
open import Quotient.Effectivity
open import Quotient.FromSetReplacement
open import Quotient.GivesPropTrunc
open import Quotient.GivesSetReplacement
open import Quotient.Large
open import Quotient.Type
open import UF.Base
open import UF.Embeddings
open import UF.Equiv hiding (_≅_)
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.PropTrunc
open import UF.Sets
open import UF.Size
open import UF.SmallnessProperties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UA-FunExt
open import UF.Univalence
\end{code}
In the following definition of existence of free groups, the given
type A of generators lives in the universe 𝓤, the group freely
generated by A is required to live in the universe 𝓥, and the
universal propertly eliminates into any universe 𝓥'.
That the universal map η into the free group is an embedding and small
if A is a set is not part of the definition of freely generated group,
but we need it, in some applications, and we just have it, and so we
find it convenient to include it in our definition of the existence of
a "good" freely generated group.
The universe 𝓦 measures the size of the map η. Recall that a map is
said to be 𝓦-small if its fibers are all 𝓦-small.
We also include the smallness of η in our definition of existence of
good free groups.
\begin{code}
record good-freely-generated-group-exists (A : 𝓤 ̇ ) (𝓥 𝓦 : Universe) : 𝓤ω where
field
𝓕 : Group 𝓥
η : A → ⟨ 𝓕 ⟩
universality : {𝓥' : Universe} (𝓖 : Group 𝓥') (f : A → ⟨ 𝓖 ⟩)
→ ∃! f̅ ꞉ (⟨ 𝓕 ⟩ → ⟨ 𝓖 ⟩)
, is-hom 𝓕 𝓖 f̅
× f̅ ∘ η ∼ f
η-is-embedding : is-set A → is-embedding η
η-is-small : is-set A → η is 𝓦 small-map
\end{code}
We will see that we don't need to assume that the type A of generators
is a set to construct the free group and establish its universal
property. But if A is a set then the universal map η is automatically
a small embedding, although not automatically *sufficiently* small for
the application discussed above, and we add some work to the reference
[1] above to make it "tiny" for the purposes of the application.
We first formulate the main results of this file before proving them.
We start with a technical lemma, which assumes a general notion of
quotient, which in turn allows the quotient of a given type to live in
a universe other than that of the given type. The parameter ℓ controls
this - see the explanations in the module Quotient.Type.
\begin{code}
Lemma[free-groups-from-general-set-quotients]
: propositional-truncations-exist
→ Fun-Ext
→ (ℓ : Universe → Universe)
→ (sq : general-set-quotients-exist ℓ)
→ are-effective sq
→ (A : 𝓤 ̇ ) → good-freely-generated-group-exists A (𝓤 ⊔ ℓ 𝓤) (𝓤 ⊔ ℓ 𝓤)
\end{code}
The proof is postponed. We just mention that it follows the above
reference [1], adapting the reasoning to HoTT/UF rather routinely,
except that we have to pay attention to proof (ir)relevance.
We are interested in ℓ = id and ℓ = (_⁺) and we are interested in the
following corollaries, which don't mention ℓ.
The first one assumes that small set quotients exist and derives their
effectivity from functional and propositional extensionality to get
that small free groups exist, choosing ℓ = id. (Notice that the
HoTT-book also uses propositional extensionality to prove the
effectivity of quotients, although with a rather different proof.)
\begin{code}
Corollary₁[free-groups-from-small-set-quotients]
: Fun-Ext
→ Prop-Ext
→ set-quotients-exist
→ (A : 𝓤 ̇ ) → good-freely-generated-group-exists A 𝓤 𝓤
Corollary₁[free-groups-from-small-set-quotients] fe pe sq =
Lemma[free-groups-from-general-set-quotients]
(propositional-truncations-from-set-quotients sq fe)
fe (λ 𝓤 → 𝓤) sq
(effectivity fe pe sq)
\end{code}
The second one assumes Set Replacement to construct quotients, and
again uses ℓ = id.
\begin{code}
Corollary₂[free-groups-from-pt-fe-pe-sr]
: (pt : propositional-truncations-exist)
→ Fun-Ext
→ Prop-Ext
→ Set-Replacement pt
→ (A : 𝓤 ̇ ) → good-freely-generated-group-exists A 𝓤 𝓤
Corollary₂[free-groups-from-pt-fe-pe-sr] pt fe pe sr =
Lemma[free-groups-from-general-set-quotients] pt fe (λ 𝓤 → 𝓤)
(set-quotients-from-set-replacement pt fe pe sr)
(set-replacement-gives-effective-set-quotients pt fe pe sr)
\end{code}
Set replacement is equivalent to the existence of small quotients in
the presence of propositional truncations and functional and
propositional extensionality.
\begin{code}
private
module _ (pt : propositional-truncations-exist)
(fe : Fun-Ext)
(pe : Prop-Ext)
where
remark→ : Set-Replacement pt → set-quotients-exist
remark→ = set-quotients-from-set-replacement pt fe pe
remark← : set-quotients-exist → Set-Replacement pt
remark← sq = set-replacement-from-set-quotients-and-prop-trunc sq pt
\end{code}
The third corollary drops set replacement, and instead constructs
freely generated groups, with ℓ = (_⁺), at the price of having the
free group living in the next universe (but still with the universal
property eliminating in all universes).
\begin{code}
Corollary₃[large-free-groups-from-pt-fe-pe]
: propositional-truncations-exist
→ Fun-Ext
→ Prop-Ext
→ (A : 𝓤 ̇ ) → good-freely-generated-group-exists A (𝓤 ⁺) (𝓤 ⁺)
Corollary₃[large-free-groups-from-pt-fe-pe] pt fe pe =
Lemma[free-groups-from-general-set-quotients] pt fe (_⁺)
(large-set-quotients pt fe pe)
(large-effective-set-quotients pt fe pe)
\end{code}
The fourth one is the observation that univalence and propositional
truncation suffice to construct large free groups.
\begin{code}
Corollary₄[large-free-groups-from-ua-pt]
: Univalence
→ propositional-truncations-exist
→ (A : 𝓤 ̇ ) → good-freely-generated-group-exists A (𝓤 ⁺) (𝓤 ⁺)
Corollary₄[large-free-groups-from-ua-pt] ua pt =
Corollary₃[large-free-groups-from-pt-fe-pe] pt
(Univalence-gives-Fun-Ext ua)
(Univalence-gives-Prop-Ext ua)
\end{code}
We also prove the following two theorems, which are not corollaries of
the above technical lemma but instead require a careful enhancement of
its proof. They both assume that the type A of generators lives in the
universe 𝓤⁺, and reduce the size of η (compared to the above
corollaries) from 𝓤⁺ to 𝓤, but with different assumptions. For future
reference, we say that η is *tiny*.
For both theorems we assume that A is a large, locally small type.
For the first one we assume the existence of small quotients.
\begin{code}
Theorem₁[large-free-groups-from-set-quotients]
: Fun-Ext
→ Prop-Ext
→ set-quotients-exist
→ (A : 𝓤 ⁺ ̇ )
→ is-locally-small A
→ good-freely-generated-group-exists A (𝓤 ⁺) 𝓤
\end{code}
The proof is posponed. But we mention that it relies on reducing the
size of the equivalence relation on words, in the sense that the
original relation has values on 𝓤⁺, and we get an equivalent
equivalence relation with values on 𝓤, exploiting the local smallness
of A and introducing other technical tools.
This theorem says that if A is large and locally small, we can
construct the group freely generated by A in the same universe as A,
so that additionally η is 𝓤 small, rather than 𝓤⁺ small, which is what
the previous corollaries give. This means that η is tiny, using the
terminology introduced above.
The second theorem doesn't assume the existence of quotients, and
instead constructs them from the assumptions, and resizes it down to
𝓤⁺ using the local smallness of A and the lemmas used to prove the
above theorem.
\begin{code}
Theorem₂[free-groups-of-large-locally-small-types]
: propositional-truncations-exist
→ Fun-Ext
→ Prop-Ext
→ (A : 𝓤 ⁺ ̇)
→ is-locally-small A
→ good-freely-generated-group-exists A (𝓤 ⁺) 𝓤
\end{code}
The proof is postponed. It is more or less routine, given the work
done to prove Theorem₁.
It is any of these two theorems that we need, in the module
Groups.Large, in order to prove that there is a group in 𝓤⁺ with no
isomorphic copy in the universe 𝓤, where it is crucial that η is
tiny. The 𝓤⁺ smallness of η, given by the previous lemma and
corollaries, is not enough.
Remark. Notice that if propositional resizing is available, then η is
automatically tiny, because it is an embedding, and the fibers of
embeddings are propositions, so that the technical lemma is
sufficient. For example, propositional resizing is available if we
assume excluded middle. Additionally, in this case, the construction
of the free group can be considerably simplified, because we can work
with words in normal form, as in classical textbooks.
Organization:
* The proof of the above technical lemma is in the submodule
free-group-construction.
* Its enhancements are in the submodules resize-universal-map
and resize-free-group.
We now proceed to prove the technical lemma. The set-hood requirement
is needed only later, and so we don't include it as an assumption in
the following anonymous module.
Notational conventions. We have a number of universal maps, such as
those into a quotient and into a free group, all denoted by η with
decorations. Moreover, we have a "pre-universal" map of A into the set
of "words with polarity".
* Given a set A of generators, FA is the type of words over elements
of A with polarities (formally 𝟚 × A).
* The function η : A → FA is the "pre-universal map".
* The function η/∾ : FA → FA/∾ is the universal map into the quotient
FA/∾ by a suitable equivalence relation _∾_ on words.
* The function ηᴳʳᵖ : A → FA/∾, the composition of the above two
functions, is the universal map into the (underlying set of the)
free group.
So in the above definition of good free group, η will be
instantiated to ηᴳʳᵖ.
\begin{code}
module free-group-construction
{𝓤 : Universe}
(A : 𝓤 ̇ )
where
X : 𝓤 ̇
X = 𝟚 × A
_⁻ : X → X
(n , a)⁻ = (complement n , a)
_⁻⁻ : X → X
x ⁻⁻ = (x ⁻)⁻
inv-invol : (x : X) → x ⁻⁻ ＝ x
inv-invol (n , a) = ap (_, a) (complement-involutive n)
\end{code}
The idea is that list concatenation _◦_ will be the group operation
after suitable quotienting, with the empty list [] as the neutral
element.
We will quotient the following type FA to get the undelying type of
the free group:
\begin{code}
FA : 𝓤 ̇
FA = List X
η : A → FA
η a = [ (₀ , a) ]
\end{code}
The type 𝟚 has two elements ₀ and ₁, and a prefix ₁ to an element a of
the type A means it is formally inverted. So in the inclusion of
generators η we indicate that the element a is not inverted by
prefixing it with ₀.
We will quotient the type FA, to get the group freely generated by A,
by the equivalence relation generated by the following reduction
relation, where we use _◦_ and _•_ for concatenation of words in FA
and letters in X.
\begin{code}
_▷_ : FA → FA → 𝓤 ̇
s ▷ t = Σ u ꞉ FA , Σ v ꞉ FA , Σ x ꞉ X , (s ＝ u ◦ x • x ⁻ • v)
× (t ＝ u ◦ v)
infix 1 _▷_
•-▷ : {s t : FA} (x : X) → s ▷ t → x • s ▷ x • t
•-▷ x (u , v , y , p , q) = (x • u) , v , y , ap (x •_) p , ap (x •_) q
\end{code}
The following lemma is proved by induction on u₀ and u₁:
\begin{code}
Lemma[Church-Rosser]
: (u₀ v₀ u₁ v₁ : FA) (x₀ x₁ : X)
→ u₀ ◦ x₀ • x₀ ⁻ • v₀ ＝ u₁ ◦ x₁ • x₁ ⁻ • v₁
→ (u₀ ◦ v₀ ＝ u₁ ◦ v₁)
+ (Σ t ꞉ FA , (u₀ ◦ v₀ ▷ t) × (u₁ ◦ v₁ ▷ t))
Lemma[Church-Rosser] u₀ v₀ u₁ v₁ x₀ x₁ = f u₀ u₁
where
f : (u₀ u₁ : FA)
→ u₀ ◦ x₀ • x₀ ⁻ • v₀ ＝ u₁ ◦ x₁ • x₁ ⁻ • v₁
→ (u₀ ◦ v₀ ＝ u₁ ◦ v₁) + (Σ t ꞉ FA , (u₀ ◦ v₀ ▷ t) × (u₁ ◦ v₁ ▷ t))
f [] [] p = inl γ
where
have : x₀ • x₀ ⁻ • v₀
＝ x₁ • x₁ ⁻ • v₁
have = p
γ : v₀ ＝ v₁
γ = equal-tails (equal-tails p)
f [] (y₁ • []) p = inl γ
where
have : x₀ • x₀ ⁻ • v₀
＝ y₁ • x₁ • x₁ ⁻ • v₁
have = p
q = x₁ ⁻ ＝⟨ ap _⁻ ((equal-heads (equal-tails p))⁻¹) ⟩
x₀ ⁻⁻ ＝⟨ inv-invol x₀ ⟩
x₀ ＝⟨ equal-heads p ⟩
y₁ ∎
r : v₀ ＝ x₁ ⁻ • v₁
r = equal-tails (equal-tails p)
γ : v₀ ＝ y₁ • v₁
γ = transport (λ - → v₀ ＝ - • v₁) q r
f [] (y₁ • z₁ • u₁) p = inr γ
where
have : x₀ • x₀ ⁻ • v₀
＝ y₁ • z₁ • u₁ ◦ x₁ • x₁ ⁻ • v₁
have = p
d' : u₁ ◦ x₁ • x₁ ⁻ • v₁ ▷ u₁ ◦ v₁
d' = u₁ , v₁ , x₁ , refl , refl
p' : u₁ ◦ x₁ • x₁ ⁻ • v₁ ＝ v₀
p' = (equal-tails (equal-tails p))⁻¹
d : v₀ ▷ u₁ ◦ v₁
d = transport (_▷ u₁ ◦ v₁) p' d'
q = y₁ ⁻ ＝⟨ (ap (_⁻) (equal-heads p)⁻¹) ⟩
x₀ ⁻ ＝⟨ equal-heads (equal-tails p) ⟩
z₁ ∎
e' : y₁ • y₁ ⁻ • u₁ ◦ v₁ ▷ u₁ ◦ v₁
e' = [] , (u₁ ◦ v₁) , y₁ , refl , refl
e : y₁ • z₁ • u₁ ◦ v₁ ▷ u₁ ◦ v₁
e = transport (λ - → y₁ • - • u₁ ◦ v₁ ▷ u₁ ◦ v₁) q e'
γ : Σ t ꞉ FA , (v₀ ▷ t) × (y₁ • z₁ • u₁ ◦ v₁ ▷ t)
γ = (u₁ ◦ v₁) , d , e
f (y₀ • []) [] p = inl γ
where
have : y₀ • x₀ • x₀ ⁻ • v₀
＝ x₁ • x₁ ⁻ • v₁
have = p
γ = y₀ • v₀ ＝⟨ ap (_• v₀) (equal-heads p) ⟩
x₁ • v₀ ＝⟨ ap (_• v₀) ((inv-invol x₁)⁻¹) ⟩
x₁ ⁻⁻ • v₀ ＝⟨ ap (λ - → - ⁻ • v₀) ((equal-heads (equal-tails p))⁻¹) ⟩
x₀ ⁻ • v₀ ＝⟨ equal-tails (equal-tails p) ⟩
v₁ ∎
f (y₀ • z₀ • u₀) [] p = inr γ
where
have : y₀ • z₀ • u₀ ◦ x₀ • x₀ ⁻ • v₀
＝ x₁ • x₁ ⁻ • v₁
have = p
q = y₀ ⁻ ＝⟨ ap (_⁻) (equal-heads p) ⟩
x₁ ⁻ ＝⟨ (equal-heads (equal-tails p))⁻¹ ⟩
z₀ ∎
d' : y₀ • y₀ ⁻ • u₀ ◦ v₀ ▷ u₀ ◦ v₀
d' = [] , (u₀ ◦ v₀) , y₀ , refl , refl
d : y₀ • z₀ • u₀ ◦ v₀ ▷ u₀ ◦ v₀
d = transport (λ - → y₀ • - • u₀ ◦ v₀ ▷ u₀ ◦ v₀) q d'
e' : u₀ ◦ x₀ • x₀ ⁻ • v₀ ▷ u₀ ◦ v₀
e' = u₀ , v₀ , x₀ , refl , refl
e : v₁ ▷ u₀ ◦ v₀
e = transport (_▷ u₀ ◦ v₀) (equal-tails (equal-tails p)) e'
γ : Σ t ꞉ FA , (y₀ • z₀ • u₀ ◦ v₀ ▷ t) × (v₁ ▷ t)
γ = (u₀ ◦ v₀) , d , e
f (y₀ • u₀) (y₁ • u₁) p = γ
where
have : y₀ • u₀ ◦ x₀ • x₀ ⁻ • v₀
＝ y₁ • u₁ ◦ x₁ • x₁ ⁻ • v₁
have = p
IH : (u₀ ◦ v₀ ＝ u₁ ◦ v₁) + (Σ t ꞉ FA , (u₀ ◦ v₀ ▷ t) × (u₁ ◦ v₁ ▷ t))
IH = f u₀ u₁ (equal-tails p)
Γ : X → X → 𝓤 ̇
Γ y₀ y₁ = (y₀ • u₀ ◦ v₀ ＝ y₁ • u₁ ◦ v₁)
+ (Σ t ꞉ FA , (y₀ • u₀ ◦ v₀ ▷ t) × (y₁ • u₁ ◦ v₁ ▷ t))
δ : type-of IH → ∀ {y₀ y₁} → y₀ ＝ y₁ → Γ y₀ y₁
δ (inl q) {y₀} refl = inl (ap (y₀ •_) q)
δ (inr (t , d , e)) {y₀} refl = inr ((y₀ • t) , •-▷ y₀ d , •-▷ y₀ e)
γ : Γ y₀ y₁
γ = δ IH (equal-heads p)
\end{code}
We are interested in the following consequence of this lemma.
\begin{code}
Theorem[Church-Rosser]
: (s t₀ t₁ : FA)
→ s ▷ t₀
→ s ▷ t₁
→ (t₀ ＝ t₁) + (Σ t ꞉ FA , (t₀ ▷ t) × (t₁ ▷ t))
Theorem[Church-Rosser] s t₀ t₁ (u₀ , v₀ , x₀ , p₀ , q₀)
(u₁ , v₁ , x₁ , p₁ , q₁) = γ δ
where
have-p₀ : s ＝ u₀ ◦ x₀ • x₀ ⁻ • v₀
have-p₀ = p₀
have-p₁ : s ＝ u₁ ◦ x₁ • x₁ ⁻ • v₁
have-p₁ = p₁
have-q₀ : t₀ ＝ u₀ ◦ v₀
have-q₀ = q₀
have-q₁ : t₁ ＝ u₁ ◦ v₁
have-q₁ = q₁
δ : (u₀ ◦ v₀ ＝ u₁ ◦ v₁) + (Σ t ꞉ FA , (u₀ ◦ v₀ ▷ t) × (u₁ ◦ v₁ ▷ t))
δ = Lemma[Church-Rosser] u₀ v₀ u₁ v₁ x₀ x₁
(u₀ ◦ x₀ • x₀ ⁻ • v₀ ＝⟨ p₀ ⁻¹ ⟩
s ＝⟨ p₁ ⟩
u₁ ◦ x₁ • x₁ ⁻ • v₁ ∎)
γ : type-of δ → (t₀ ＝ t₁) + (Σ t ꞉ FA , (t₀ ▷ t) × (t₁ ▷ t))
γ (inl q) = inl (t₀ ＝⟨ q₀ ⟩
u₀ ◦ v₀ ＝⟨ q ⟩
u₁ ◦ v₁ ＝⟨ q₁ ⁻¹ ⟩
t₁ ∎)
γ (inr (t , p₀ , p₁)) = inr (t , I₀ , I₁)
where
I₀ : t₀ ▷ t
I₀ = transport (_▷ t) (q₀ ⁻¹) p₀
I₁ : t₁ ▷ t
I₁ = transport (_▷ t) (q₁ ⁻¹) p₁
\end{code}
It is noteworthy and remarkable that the above doesn't need decidable
equality on A. We repeat that this construction is due to Mines,
Richman and Ruitenburg [1].
The following import defines
_◁▷_ the symmetric closure of _▷_,
_∿_ the symmetric, reflexive, transitive closure of _▷_,
_▷*_ the reflexive, transitive closure of _▷_,
_▷[ n ]_ the n-fold iteration of _▷_.
_◁▷[ n ]_ the n-fold iteration of _◁▷_.
and develops some useful consequences of the Church-Rosser property in
a general setting.
\begin{code}
open import Relations.SRTclosure public
open import Relations.ChurchRosser _▷_ public
\end{code}
The insertion of generators is trivially left cancellable before
quotienting:
\begin{code}
η-lc : {a b : A} → η a ＝ η b → a ＝ b
η-lc refl = refl
\end{code}
The following less trivial result, which relies on the Church-Rosser
property, will give that the insertion of generators is injective
after quotienting:
\begin{code}
η-irreducible : {a : A} {s : FA} → ¬ (η a ▷ s)
η-irreducible ((x • []) , v , y , () , refl)
η-irreducible ((x • y • u) , v , z , () , q)
η-irreducible⋆ : {a : A} {s : FA} → η a ▷⋆ s → η a ＝ s
η-irreducible⋆ {a} {s} (n , r) = f n r
where
f : (n : ℕ) → η a ▷[ n ] s → η a ＝ s
f 0 refl = refl
f (succ n) (t , r , i) = 𝟘-elim (η-irreducible r)
η-identifies-∿-related-points : {a b : A} → η a ∿ η b → a ＝ b
η-identifies-∿-related-points {a} {b} e = η-lc p
where
σ : Σ s ꞉ FA , (η a ▷⋆ s) × (η b ▷⋆ s)
σ = from-∿ Theorem[Church-Rosser] (η a) (η b) e
s = pr₁ σ
p = η a ＝⟨ η-irreducible⋆ (pr₁ (pr₂ σ)) ⟩
s ＝⟨ (η-irreducible⋆ (pr₂ (pr₂ σ)))⁻¹ ⟩
η b ∎
\end{code}
We need to work with the propositional truncation of _∿_ to construct
the free group, but most of the work will be done before truncation.
The following is for reasoning with chains of equivalences _∿_:
\begin{code}
_∿⟨_⟩_ : (s : FA) {t u : FA} → s ∿ t → t ∿ u → s ∿ u
_ ∿⟨ p ⟩ q = srt-transitive _▷_ _ _ _ p q
_∿∎ : (s : FA) → s ∿ s
_∿∎ _ = srt-reflexive _▷_ _
infixr 0 _∿⟨_⟩_
infix 1 _∿∎
\end{code}
We restate the reflexivity of the relation _∿_ as follows for
technical convenience.
\begin{code}
＝-gives-∿ : {s s' : FA} → s ＝ s' → s ∿ s'
＝-gives-∿ {s} refl = srt-reflexive _▷_ s
\end{code}
As discussed above, the group operation before quotienting is simply
concatenation, with the empty list as the neutral element.
Concatenation is a left congruence. We establish this in several
steps:
\begin{code}
◦-▷-left : (s s' t : FA) → s ▷ s' → s ◦ t ▷ s' ◦ t
◦-▷-left s s' t (u , v , x , p , q) = u , (v ◦ t) , x , p' , q'
where
p' = s ◦ t ＝⟨ ap (_◦ t) p ⟩
(u ◦ x • x ⁻ • v) ◦ t ＝⟨ ◦-assoc u _ t ⟩
u ◦ x • x ⁻ • v ◦ t ∎
q' = s' ◦ t ＝⟨ ap (_◦ t) q ⟩
(u ◦ v) ◦ t ＝⟨ ◦-assoc u v t ⟩
u ◦ v ◦ t ∎
◦-◁▷-left : (s s' t : FA) → s ◁▷ s' → s ◦ t ◁▷ s' ◦ t
◦-◁▷-left s s' t (inl a) = inl (◦-▷-left s s' t a)
◦-◁▷-left s s' t (inr a) = inr (◦-▷-left s' s t a)
◦-iteration-left : (s s' t : FA) (n : ℕ)
→ s ◁▷[ n ] s'
→ s ◦ t ◁▷[ n ] s' ◦ t
◦-iteration-left s s t 0 refl = refl
◦-iteration-left s s' t (succ n) (u , b , c) = (u ◦ t) ,
◦-◁▷-left s u t b ,
◦-iteration-left u s' t n c
◦-cong-left : (s s' t : FA) → s ∿ s' → s ◦ t ∿ s' ◦ t
◦-cong-left s s' t (n , a) = n , ◦-iteration-left s s' t n a
\end{code}
It is also a right congruence:
\begin{code}
•-◁▷ : (x : X) {s t : FA} → s ◁▷ t → x • s ◁▷ x • t
•-◁▷ x (inl e) = inl (•-▷ x e)
•-◁▷ x (inr e) = inr (•-▷ x e)
•-iteration : (x : X) {s t : FA} (n : ℕ)
→ s ◁▷[ n ] t
→ x • s ◁▷[ n ] x • t
•-iteration x 0 refl = refl
•-iteration x (succ n) (u , b , c) = (x • u) , •-◁▷ x b , •-iteration x n c
•-cong : (x : X) {s t : FA} → s ∿ t → x • s ∿ x • t
•-cong x (n , a) = n , •-iteration x n a
◦-cong-right : (s {t t'} : FA) → t ∿ t' → s ◦ t ∿ s ◦ t'
◦-cong-right [] e = e
◦-cong-right (x • s) e = •-cong x (◦-cong-right s e)
\end{code}
And therefore it is a two-sided congruence:
\begin{code}
◦-cong-∿ : {s s' t t' : FA} → s ∿ s' → t ∿ t' → s ◦ t ∿ s' ◦ t'
◦-cong-∿ {s} {s'} {t} {t'} d e = s ◦ t ∿⟨ ◦-cong-left s s' t d ⟩
s' ◦ t ∿⟨ ◦-cong-right s' e ⟩
s' ◦ t' ∿∎
\end{code}
We now construct the group inverse before quotienting. We reverse the
given list and formally invert all its elements:
\begin{code}
finv : FA → FA
finv [] = []
finv (x • s) = finv s ◦ x ⁻ • []
\end{code}
It is a congruence, which is proved in several steps:
\begin{code}
finv-◦ : (s t : FA) → finv (s ◦ t) ＝ finv t ◦ finv s
finv-◦ [] t = []-right-neutral (finv t)
finv-◦ (x • s) t = finv (s ◦ t) ◦ x ⁻ • [] ＝⟨ IH ⟩
(finv t ◦ finv s) ◦ x ⁻ • [] ＝⟨ a ⟩
finv t ◦ (finv s ◦ x ⁻ • []) ∎
where
IH = ap (_◦ x ⁻ • []) (finv-◦ s t)
a = ◦-assoc (finv t) (finv s) [ x ⁻ ]
finv-▷ : {s t : FA} → s ▷ t → finv s ▷ finv t
finv-▷ {s} {t} (u , v , y , p , q) = finv v , finv u , y , p' , q'
where
p' = finv s ＝⟨ I ⟩
finv (u ◦ y • y ⁻ • v) ＝⟨ II ⟩
finv (y • y ⁻ • v) ◦ finv u ＝⟨ III ⟩
(finv v ◦ [ y ⁻⁻ ] ◦ [ y ⁻ ]) ◦ finv u ＝⟨ IV ⟩
(finv v ◦ y • y ⁻ • []) ◦ finv u ＝⟨ V ⟩
finv v ◦ y • y ⁻ • finv u ∎
where
I = ap finv p
II = finv-◦ u (y • y ⁻ • v)
III = ap (_◦ finv u) (finv-◦ ([ y ] ◦ [ y ⁻ ]) v)
IV = ap (λ - → (finv v ◦ [ - ] ◦ [ y ⁻ ]) ◦ finv u) (inv-invol y)
V = ◦-assoc (finv v) ([ y ] ◦ [ y ⁻ ]) (finv u)
q' = finv t ＝⟨ ap finv q ⟩
finv (u ◦ v) ＝⟨ finv-◦ u v ⟩
finv v ◦ finv u ∎
finv-◁▷ : {s t : FA} → s ◁▷ t → finv s ◁▷ finv t
finv-◁▷ (inl e) = inl (finv-▷ e)
finv-◁▷ (inr e) = inr (finv-▷ e)
finv-iteration : {s t : FA} (n : ℕ)
→ s ◁▷[ n ] t
→ finv s ◁▷[ n ] finv t
finv-iteration 0 refl = refl
finv-iteration (succ n) (u , b , c) = finv u , finv-◁▷ b , finv-iteration n c
finv-cong-∿ : {s t : FA} → s ∿ t → finv s ∿ finv t
finv-cong-∿ (n , a) = n , finv-iteration n a
\end{code}
The inverse really is an inverse:
\begin{code}
finv-lemma-right : (x : X) → x • x ⁻ • [] ∿ []
finv-lemma-right x = srt-extension _▷_ _ [] ([] , [] , x , refl , refl)
finv-lemma-left : (x : X) → x ⁻ • [] ◦ x • [] ∿ []
finv-lemma-left x = srt-extension _▷_ _ _
([] ,
[] ,
(x ⁻) ,
ap (λ - → x ⁻ • [] ◦ - • []) ((inv-invol x)⁻¹) , refl)
finv-right-∿ : (s : FA) → s ◦ finv s ∿ []
finv-right-∿ [] = srt-reflexive _▷_ []
finv-right-∿ (x • s) = γ
where
IH : s ◦ finv s ∿ []
IH = finv-right-∿ s
γ = x • s ◦ finv s ◦ x ⁻ • [] ∿⟨ I ⟩
x • (s ◦ finv s) ◦ x ⁻ • [] ∿⟨ II ⟩
x • x ⁻ • [] ∿⟨ III ⟩
[] ∿∎
where
I = ＝-gives-∿ (ap (x •_) (◦-assoc s (finv s) [ x ⁻ ])⁻¹)
II = ◦-cong-right [ x ] (◦-cong-left _ _ _ IH)
III = finv-lemma-right x
finv-left-∿ : (s : FA) → finv s ◦ s ∿ []
finv-left-∿ [] = srt-reflexive _▷_ []
finv-left-∿ (x • s) = γ
where
γ = (finv s ◦ x ⁻ • []) ◦ x • s ∿⟨ I ⟩
finv s ◦ (x ⁻ • [] ◦ x • s) ∿⟨ II ⟩
finv s ◦ (x ⁻ • [] ◦ x • []) ◦ s ∿⟨ III ⟩
finv s ◦ s ∿⟨ IV ⟩
[] ∿∎
where
I = ＝-gives-∿ (◦-assoc (finv s) [ x ⁻ ] (x • s))
II = ＝-gives-∿ (ap (finv s ◦_) ((◦-assoc [ x ⁻ ] [ x ] s)⁻¹))
III = ◦-cong-right (finv s) (◦-cong-left _ _ _ (finv-lemma-left x))
IV = finv-left-∿ s
\end{code}
We now work with the propositional, symmetric, reflexive, transitive
closure of _▷_, denoted by _∾_, for which we need to assume the
existence of propositional truncations.
\begin{code}
module free-group-construction-step₁
(pt : propositional-truncations-exist)
where
open PropositionalTruncation pt public
_∾_ : FA → FA → 𝓤 ̇
x ∾ y = ∥ x ∿ y ∥
infix 1 _∾_
η-identifies-∾-related-points : {a b : A} → is-set A → η a ∾ η b → a ＝ b
η-identifies-∾-related-points i = ∥∥-rec i η-identifies-∿-related-points
◦-cong : {s s' t t' : FA} → s ∾ s' → t ∾ t' → s ◦ t ∾ s' ◦ t'
◦-cong = ∥∥-functor₂ ◦-cong-∿
finv-cong : {s t : FA} → s ∾ t → finv s ∾ finv t
finv-cong = ∥∥-functor finv-cong-∿
finv-right : (s : FA) → s ◦ finv s ∾ []
finv-right s = ∣ finv-right-∿ s ∣
finv-left : (s : FA) → finv s ◦ s ∾ []
finv-left s = ∣ finv-left-∿ s ∣
\end{code}
To perform the quotient, we assume functional extensionality and the
existence of general, effective set quotients, in a universe
controlled by ℓ.
\begin{code}
module free-group-construction-step₂
(fe : Fun-Ext)
(ℓ : Universe → Universe)
(sq : general-set-quotients-exist ℓ)
(η/-relates-identified-points : are-effective sq)
where
𝓤̅ : Universe
𝓤̅ = 𝓤 ⊔ ℓ 𝓤
open general-set-quotients-exist sq
open psrt pt _▷_ public
\end{code}
We have that _∾_ is an equivalence relation:
\begin{code}
∾-is-equiv-rel : is-equiv-rel _∾_
∾-is-equiv-rel = psrt-is-equiv-rel
-∾- : EqRel FA
-∾- = _∾_ , ∾-is-equiv-rel
\end{code}
The acronym "psrt" stands for propositional, reflexive, symmetric and
transitive closure of a relation, in this case _▷_.
We now name the quotient set and the universal map into it.
\begin{code}
FA/∾ : 𝓤̅ ̇
FA/∾ = FA / -∾-
η/∾ : FA → FA/∾
η/∾ = η/ -∾-
\end{code}
The insertion of generators of the free group is obtained by composing
the universal map into the quotient with our original map η : A → FA
that inserts the generators into the freely generated "pre-group" of
lists.
\begin{code}
ηᴳʳᵖ : A → FA/∾
ηᴳʳᵖ a = η/∾ (η a)
\end{code}
It is important for our purposes, and what we wanted to know,
constructively, that the inclusion of generators in the free group is
an injection, or a left-cancellable map, which relies on the
effectivity of quotients.
\begin{code}
η/∾-relates-identified-points : {s t : FA} → η/∾ s ＝ η/∾ t → s ∾ t
η/∾-relates-identified-points = η/-relates-identified-points -∾-
ηᴳʳᵖ-lc : is-set A → {a b : A} → ηᴳʳᵖ a ＝ ηᴳʳᵖ b → a ＝ b
ηᴳʳᵖ-lc i p = η-identifies-∾-related-points i
(η/∾-relates-identified-points p)
ηᴳʳᵖ-is-embedding : is-set A → is-embedding ηᴳʳᵖ
ηᴳʳᵖ-is-embedding i = lc-maps-into-sets-are-embeddings ηᴳʳᵖ
(ηᴳʳᵖ-lc i)
(/-is-set -∾-)
η/∾-identifies-related-points : {s t : FA} → s ∾ t → η/∾ s ＝ η/∾ t
η/∾-identifies-related-points = η/-identifies-related-points -∾-
\end{code}
We now need to make FA/∾ into a group. We will use "/" in names to
indicate constructions on the quotient type FA/∾.
\begin{code}
e/ : FA/∾
e/ = η/∾ []
inv/ : FA/∾ → FA/∾
inv/ = extension₁/ -∾- finv finv-cong
_·_ : FA/∾ → FA/∾ → FA/∾
_·_ = extension₂/ -∾- _◦_ ◦-cong
\end{code}
The following two naturality conditions are crucial:
\begin{code}
inv/-natural : (s : FA) → inv/ (η/∾ s) ＝ η/∾ (finv s)
inv/-natural = naturality/ -∾- finv finv-cong
·-natural : (s t : FA) → η/∾ s · η/∾ t ＝ η/∾ (s ◦ t)
·-natural = naturality₂/ -∾- _◦_ ◦-cong
\end{code}
Next, to prove the groups laws, we use quotient induction, denoted by
`/-induction`.
One can think of elements of FA/∾ as equivalence classes, and of η/∾ s
as the equivalence class of s. Then quotient induction says that in
order to prove a property of equivalence classes, it is enough to
prove it for all equivalence classes of given elements (this is proved
in the module Quotient.Type).
The following proofs rely on the above naturality conditions:
\begin{code}
ln/ : left-neutral e/ _·_
ln/ = /-induction -∾- (λ _ → /-is-set -∾-) γ
where
γ : (s : FA) → η/∾ [] · η/∾ s ＝ η/∾ s
γ = ·-natural []
rn/ : right-neutral e/ _·_
rn/ = /-induction -∾- (λ _ → /-is-set -∾-) γ
where
γ : (s : FA) → η/∾ s · η/∾ [] ＝ η/∾ s
γ s = η/∾ s · η/∾ [] ＝⟨ ·-natural s [] ⟩
η/∾ (s ◦ []) ＝⟨ ap η/∾ ([]-right-neutral s ⁻¹) ⟩
η/∾ s ∎
invl/ : (x : FA/∾) → inv/ x · x ＝ e/
invl/ = /-induction -∾- (λ _ → /-is-set -∾-) γ
where
γ : (s : FA) → inv/ (η/∾ s) · η/∾ s ＝ e/
γ s = inv/ (η/∾ s) · η/∾ s ＝⟨ ap (_· η/∾ s) (inv/-natural s) ⟩
η/∾ (finv s) · η/∾ s ＝⟨ ·-natural (finv s) s ⟩
η/∾ (finv s ◦ s) ＝⟨ η/∾-identifies-related-points (finv-left s) ⟩
η/∾ [] ＝⟨ refl ⟩
e/ ∎
invr/ : (x : FA/∾) → x · inv/ x ＝ e/
invr/ = /-induction -∾- (λ _ → /-is-set -∾-) γ
where
γ : (s : FA) → η/∾ s · inv/ (η/∾ s) ＝ e/
γ s = η/∾ s · inv/ (η/∾ s) ＝⟨ ap (η/∾ s ·_) (inv/-natural s) ⟩
η/∾ s · η/∾ (finv s) ＝⟨ ·-natural s (finv s) ⟩
η/∾ (s ◦ finv s) ＝⟨ η/∾-identifies-related-points (finv-right s) ⟩
η/∾ [] ＝⟨ refl ⟩
e/ ∎
assoc/ : associative _·_
assoc/ = /-induction -∾-
(λ x → Π₂-is-prop fe (λ y z → /-is-set -∾-))
(λ s → /-induction -∾-
(λ y → Π-is-prop fe (λ z → /-is-set -∾-))
(λ t → /-induction -∾-
(λ z → /-is-set -∾-)
(γ s t)))
where
γ : (s t u : FA) → (η/∾ s · η/∾ t) · η/∾ u ＝ η/∾ s · (η/∾ t · η/∾ u)
γ s t u = (η/∾ s · η/∾ t) · η/∾ u ＝⟨ ap (_· η/∾ u) (·-natural s t) ⟩
η/∾ (s ◦ t) · η/∾ u ＝⟨ ·-natural (s ◦ t) u ⟩
η/∾ ((s ◦ t) ◦ u) ＝⟨ ap η/∾ (◦-assoc s t u) ⟩
η/∾ (s ◦ (t ◦ u)) ＝⟨ (·-natural s (t ◦ u))⁻¹ ⟩
η/∾ s · η/∾ (t ◦ u) ＝⟨ ap (η/∾ s ·_) ((·-natural t u)⁻¹) ⟩
η/∾ s · (η/∾ t · η/∾ u) ∎
\end{code}
So we have constructed a group with underlying set FA/∾ and a map
ηᴳʳᵖ : A → FA/∾. We now put everyhing together:
\begin{code}
𝓕 : Group 𝓤̅
𝓕 = (FA/∾ , _·_ , /-is-set -∾- , assoc/ , e/ , ln/ , rn/ ,
(λ x → inv/ x , invl/ x , invr/ x))
\end{code}
To prove that ηᴳʳᵖ is the universal map of the set A into a group, we
assume another group 𝓖 with a map f : A → 𝓖:
\begin{code}
module free-group-construction-step₃
{𝓥 : Universe}
(G : 𝓥 ̇ )
(G-is-set : is-set G)
(e : G)
(invG : G → G)
(_*_ : G → G → G)
(G-ln : left-neutral e _*_)
(G-rn : right-neutral e _*_)
(G-invl : (g : G) → invG g * g ＝ e)
(G-invr : (g : G) → g * invG g ＝ e)
(G-assoc : associative _*_)
(f : A → G)
where
𝓖 : Group 𝓥
𝓖 = (G , _*_ ,
G-is-set , G-assoc , e , G-ln , G-rn ,
(λ x → invG x , G-invl x , G-invr x))
\end{code}
Our objective is to construct f̅ from f making the universality
triangle commute. As a first step in the construction of f̅, we
construct a map h by induction on lists.
\begin{code}
h : FA → G
h [] = e
h ((₀ , a) • s) = f a * h s
h ((₁ , a) • s) = invG (f a) * h s
\end{code}
We need the following property of h with respect to formal inverses:
\begin{code}
h⁻ : (x : X) → h (x • x ⁻ • []) ＝ e
h⁻ (₀ , a) = f a * (invG (f a) * e) ＝⟨ ap (f a *_) (G-rn (invG (f a))) ⟩
f a * invG (f a) ＝⟨ G-invr (f a) ⟩
e ∎
h⁻ (₁ , a) = invG (f a) * (f a * e) ＝⟨ ap (invG (f a) *_) (G-rn (f a)) ⟩
invG (f a) * f a ＝⟨ G-invl (f a) ⟩
e ∎
\end{code}
By construction, the function h is a list homomorphism. It is also a
monoid homomorphism:
\begin{code}
h-is-hom : (s t : FA) → h (s ◦ t) ＝ h s * h t
h-is-hom [] t =
h t ＝⟨ (G-ln (h t))⁻¹ ⟩
e * h t ∎
h-is-hom ((₀ , a) • s) t =
f a * h (s ◦ t) ＝⟨ ap (f a *_) (h-is-hom s t) ⟩
f a * (h s * h t) ＝⟨ (G-assoc (f a) (h s) (h t))⁻¹ ⟩
(f a * h s) * h t ＝⟨ refl ⟩
h (₀ , a • s) * h t ∎
h-is-hom (₁ , a • s) t =
invG (f a) * h (s ◦ t) ＝⟨ ap (invG (f a) *_) (h-is-hom s t) ⟩
invG (f a) * (h s * h t) ＝⟨ (G-assoc (invG (f a)) (h s) (h t))⁻¹ ⟩
(invG (f a) * h s) * h t ＝⟨ refl ⟩
h (₁ , a • s) * h t ∎
\end{code}
We also need the following property of the map h in order to construct
our desired group homomorphism f̅:
\begin{code}
h-identifies-▷-related-points : {s t : FA} → s ▷ t → h s ＝ h t
h-identifies-▷-related-points {s} {t} (u , v , y , p , q) =
h s ＝⟨ ap h p ⟩
h (u ◦ y • y ⁻ • v) ＝⟨ h-is-hom u (y • y ⁻ • v) ⟩
h u * h (y • y ⁻ • v) ＝⟨ ap (h u *_) (h-is-hom (y • y ⁻ • []) v) ⟩
h u * (h (y • y ⁻ • []) * h v) ＝⟨ ap (λ - → h u * (- * h v)) (h⁻ y) ⟩
h u * (e * h v) ＝⟨ ap (h u *_) (G-ln (h v)) ⟩
h u * h v ＝⟨ (h-is-hom u v)⁻¹ ⟩
h (u ◦ v) ＝⟨ ap h (q ⁻¹) ⟩
h t ∎
h-identifies-▷⋆-related-points : {s t : FA} → s ▷⋆ t → h s ＝ h t
h-identifies-▷⋆-related-points {s} {t} (n , r) = γ n s t r
where
γ : (n : ℕ) (s t : FA) → s ▷[ n ] t → h s ＝ h t
γ 0 s s refl = refl
γ (succ n) s t (u , r , i) = h s ＝⟨ h-identifies-▷-related-points r ⟩
h u ＝⟨ γ n u t i ⟩
h t ∎
h-identifies-∾-related-points : {s t : FA} → s ∾ t → h s ＝ h t
h-identifies-∾-related-points {s} {t} e = γ
where
δ : (Σ u ꞉ FA , (s ▷⋆ u) × (t ▷⋆ u)) → h s ＝ h t
δ (u , σ , τ) = h s ＝⟨ (h-identifies-▷⋆-related-points σ) ⟩
h u ＝⟨ (h-identifies-▷⋆-related-points τ)⁻¹ ⟩
h t ∎
γ : h s ＝ h t
γ = ∥∥-rec G-is-set δ (∥∥-functor (from-∿ Theorem[Church-Rosser] s t) e)
\end{code}
We can then finally construct the unique homorphism f̅ extending f
applying the universal property of quotients to the above map h:
\begin{code}
f̅ : FA/∾ → G
f̅ = mediating-map/ -∾- G-is-set h h-identifies-∾-related-points
f̅-/triangle : f̅ ∘ η/∾ ∼ h
f̅-/triangle = universality-triangle/ -∾-
G-is-set h h-identifies-∾-related-points
\end{code}
And from this we get the triangle for the universal property of the
free group:
\begin{code}
f̅-triangle : f̅ ∘ ηᴳʳᵖ ∼ f
f̅-triangle a = f̅ (η/∾ (η a)) ＝⟨ f̅-/triangle (η a) ⟩
h (η a) ＝⟨ refl ⟩
f a * e ＝⟨ G-rn (f a) ⟩
f a ∎
\end{code}
Which is a group homomorphism (rather than merely a monoid
homomorphism like h):
\begin{code}
f̅-is-hom : is-hom 𝓕 𝓖 f̅
f̅-is-hom {x} {y} = γ x y
where
δ : (s t : FA) → f̅ (η/∾ s · η/∾ t) ＝ f̅ (η/∾ s) * f̅ (η/∾ t)
δ s t = f̅ (η/∾ s · η/∾ t) ＝⟨ I ⟩
f̅ (η/∾ (s ◦ t)) ＝⟨ II ⟩
h (s ◦ t) ＝⟨ III ⟩
h s * h t ＝⟨ IV ⟩
f̅ (η/∾ s) * f̅ (η/∾ t) ∎
where
I = ap f̅ (·-natural s t)
II = f̅-/triangle (s ◦ t)
III = h-is-hom s t
IV = ap₂ _*_ ((f̅-/triangle s)⁻¹) ((f̅-/triangle t)⁻¹)
γ : (x y : FA / -∾-) → f̅ (x · y) ＝ f̅ x * f̅ y
γ = /-induction -∾-
(λ x → Π-is-prop fe (λ y → G-is-set))
(λ s → /-induction -∾-
(λ a → G-is-set)
(δ s))
\end{code}
Notice that for the following uniqueness property of f̅ we don't need
to assume that f₀ and f₁ are group homomorphisms:
\begin{code}
f̅-uniqueness-∾ : (f₀ f₁ : FA/∾ → G) → f₀ ∘ η/∾ ∼ h → f₁ ∘ η/∾ ∼ h → f₀ ∼ f₁
f̅-uniqueness-∾ f₀ f₁ p q = at-most-one-mediating-map/ -∾-
G-is-set f₀ f₁ (λ s → p s ∙ (q s)⁻¹)
\end{code}
But for this one we do:
\begin{code}
f̅-uniqueness' : (f₀ f₁ : FA/∾ → G)
→ is-hom 𝓕 𝓖 f₀
→ is-hom 𝓕 𝓖 f₁
→ f₀ ∘ ηᴳʳᵖ ∼ f
→ f₁ ∘ ηᴳʳᵖ ∼ f
→ f₀ ∼ f₁
f̅-uniqueness' f₀ f₁ i₀ i₁ f₀-triangle f₁-triangle = γ
where
p : f₀ ∘ ηᴳʳᵖ ∼ f₁ ∘ ηᴳʳᵖ
p x = f₀-triangle x ∙ (f₁-triangle x)⁻¹
δ : (s : FA) → f₀ (η/∾ s) ＝ f₁ (η/∾ s)
δ [] = f₀ (η/∾ []) ＝⟨ homs-preserve-unit 𝓕 𝓖 f₀ i₀ ⟩
e ＝⟨ (homs-preserve-unit 𝓕 𝓖 f₁ i₁)⁻¹ ⟩
f₁ (η/∾ []) ∎
δ ((₀ , a) • s) =
f₀ (η/∾ (η a ◦ s)) ＝⟨ ap f₀ ((·-natural (η a) s)⁻¹) ⟩
f₀ (ηᴳʳᵖ a · η/∾ s) ＝⟨ i₀ ⟩
f₀ (ηᴳʳᵖ a) * f₀ (η/∾ s) ＝⟨ ap₂ _*_ (p a) (δ s) ⟩
f₁ (ηᴳʳᵖ a) * f₁ (η/∾ s) ＝⟨ i₁ ⁻¹ ⟩
f₁ (ηᴳʳᵖ a · η/∾ s) ＝⟨ ap f₁ (·-natural (η a) s) ⟩
f₁ (η/∾ (η a ◦ s)) ∎
δ ((₁ , a) • s) =
f₀ (η/∾ (finv (η a) ◦ s)) ＝⟨ I ⟩
f₀ (η/∾ (finv (η a)) · η/∾ s) ＝⟨ II ⟩
f₀ (η/∾ (finv (η a))) * f₀ (η/∾ s) ＝⟨ III ⟩
f₀ (inv/ (ηᴳʳᵖ a)) * f₀ (η/∾ s) ＝⟨ IV ⟩
invG (f₀ (ηᴳʳᵖ a)) * f₀ (η/∾ s) ＝⟨ IH ⟩
invG (f₁ (ηᴳʳᵖ a)) * f₁ (η/∾ s) ＝⟨ IV' ⟩
f₁ (inv/ (ηᴳʳᵖ a)) * f₁ (η/∾ s) ＝⟨ III' ⟩
f₁ (η/∾ (finv (η a))) * f₁ (η/∾ s) ＝⟨ II' ⟩
f₁ (η/∾ (finv (η a)) · η/∾ s) ＝⟨ I' ⟩
f₁ (η/∾ (finv (η a) ◦ s)) ∎
where
I = ap f₀ ((·-natural (finv (η a)) s)⁻¹)
II = i₀
III = ap (λ - → f₀ - * f₀ (η/∾ s)) ((inv/-natural (η a))⁻¹)
IV = ap (_* f₀ (η/∾ s)) (homs-preserve-invs 𝓕 𝓖 f₀ i₀ (ηᴳʳᵖ a))
IH = ap₂ (λ - -' → invG - * -') (p a) (δ s)
IV' = ap (_* f₁ (η/∾ s)) ((homs-preserve-invs 𝓕 𝓖 f₁ i₁ (ηᴳʳᵖ a))⁻¹)
III' = ap (λ - → f₁ - * f₁ (η/∾ s)) (inv/-natural (η a))
II' = i₁ ⁻¹
I' = ap f₁ (·-natural (finv (η a)) s)
γ : f₀ ∼ f₁
γ = /-induction -∾- (λ x → G-is-set) δ
f̅-uniqueness : ∃! f̅ ꞉ (⟨ 𝓕 ⟩ → ⟨ 𝓖 ⟩)
, is-hom 𝓕 𝓖 f̅
× f̅ ∘ ηᴳʳᵖ ∼ f
f̅-uniqueness = γ
where
c : Σ f̅ ꞉ (⟨ 𝓕 ⟩ → ⟨ 𝓖 ⟩) , is-hom 𝓕 𝓖 f̅ × f̅ ∘ ηᴳʳᵖ ∼ f
c = (f̅ , f̅-is-hom , f̅-triangle)
i : is-central _ c
i (f₀ , f₀-is-hom , f₀-triangle) = to-subtype-＝ a b
where
a : (f̅ : ⟨ 𝓕 ⟩ → ⟨ 𝓖 ⟩) → is-prop (is-hom 𝓕 𝓖 f̅ × f̅ ∘ ηᴳʳᵖ ∼ f)
a f̅ = ×-is-prop
(being-hom-is-prop fe 𝓕 𝓖 f̅)
(Π-is-prop fe (λ a → groups-are-sets 𝓖))
b : f̅ ＝ f₀
b = dfunext fe
(f̅-uniqueness' f̅ f₀ f̅-is-hom f₀-is-hom f̅-triangle f₀-triangle)
γ : ∃! f̅ ꞉ (⟨ 𝓕 ⟩ → ⟨ 𝓖 ⟩) , is-hom 𝓕 𝓖 f̅ × f̅ ∘ ηᴳʳᵖ ∼ f
γ = c , i
\end{code}
This completes the construction of the free group.
We summarize the important parts in the following interface:
\begin{code}
module FreeGroupInterface
(pt : propositional-truncations-exist)
(fe : Fun-Ext)
(ℓ : Universe → Universe)
(sq : general-set-quotients-exist ℓ)
(η/-relates-identified-points : are-effective sq)
{𝓤 : Universe}
(A : 𝓤 ̇ )
where
open free-group-construction A
open free-group-construction-step₁ pt
open free-group-construction-step₂ fe ℓ sq η/-relates-identified-points
free-group : Group 𝓤̅
free-group = 𝓕
η-free-group : A → ⟨ free-group ⟩
η-free-group = ηᴳʳᵖ
η-free-group-is-small : ηᴳʳᵖ is (𝓤 ⊔ ℓ 𝓤) small-map
η-free-group-is-small = native-size-of-map ηᴳʳᵖ
η-free-group-is-embedding : is-set A → is-embedding η-free-group
η-free-group-is-embedding = ηᴳʳᵖ-is-embedding
module _ ((G , _*_ , G-is-set , G-assoc , e , l , r , inversion) : Group 𝓥)
(f : A → G)
where
open free-group-construction-step₃
G G-is-set e (λ x → pr₁ (inversion x)) _*_ l r
(λ x → pr₁ (pr₂ (inversion x))) (λ x → pr₂ (pr₂ (inversion x))) G-assoc f
free-group-extension : ⟨ free-group ⟩ → ⟨ 𝓖 ⟩
free-group-extension = f̅
free-group-is-hom : is-hom free-group 𝓖 free-group-extension
free-group-is-hom = f̅-is-hom
free-group-triangle : free-group-extension ∘ η-free-group ∼ f
free-group-triangle = f̅-triangle
extension-to-free-group-uniqueness :
∃! f̅ ꞉ (⟨ free-group ⟩ → ⟨ 𝓖 ⟩)
, is-hom free-group 𝓖 f̅
× f̅ ∘ η-free-group ∼ f
extension-to-free-group-uniqueness = f̅-uniqueness
\end{code}
With this we have proved the tecnical lemma.
\begin{code}
Lemma[free-groups-from-general-set-quotients] pt fe ℓ sq eff A =
record
{ 𝓕 = free-group
; η = η-free-group
; universality = extension-to-free-group-uniqueness
; η-is-embedding = η-free-group-is-embedding
; η-is-small = λ _ → η-free-group-is-small
}
where
open FreeGroupInterface pt fe ℓ sq eff A
\end{code}
(*) Notice that the assumption that A is a set is not needed for η to
be small in this case, but it is needed for η to be an embedding.
We now proceed to the proof of Theorem₁, which requires an enhancement
of the above proof.
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-universal-map
(fe : Fun-Ext)
(pe : Prop-Ext)
(pt : propositional-truncations-exist)
{𝓤 : Universe}
(A : 𝓤 ⁺ ̇)
(_＝₀_ : A → A → 𝓤 ̇ )
(refl₀ : (a : A) → a ＝₀ a)
(from-＝₀ : (a b : A) → a ＝₀ b → a ＝ b)
(ℓ : Universe → Universe)
(sq : general-set-quotients-exist ℓ)
(η/-relates-identified-points : are-effective sq)
where
open free-group-construction A
𝓤⁺ = 𝓤 ⁺
𝓤⁺⁺ = 𝓤⁺ ⁺
fe' : FunExt
fe' 𝓤 𝓥 = fe {𝓤} {𝓥}
pe' : PropExt
pe' 𝓤 = pe {𝓤}
\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 universal map, we reduce the size of the (propositional) values of
this equivalence relation using the assumed relation _＝₀_ and
functions refl₀ and from-＝₀.
\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)
\end{code}
The crucial idea for the size reduction of the equivalence relation is
to redefine the relation _▷_ as follows.
\begin{code}
_◗_ : 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}
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
level back to that 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}
Now notice that the native size of ηᴳʳᵖ is large.
\begin{code}
open free-group-construction-step₁ pt
open free-group-construction-step₂ fe ℓ sq η/-relates-identified-points
ηᴳʳᵖ-is-large : ηᴳʳᵖ is 𝓤⁺ ⊔ ℓ 𝓤⁺ small-map
ηᴳʳᵖ-is-large = native-size-of-map ηᴳʳᵖ
\end{code}
For the application discussed above, we need ηᴳʳᵖ to be 𝓤 small, or
"tiny", which we achieve applying the above development.
Recall that the function η/∾ : FA → FA/∾ is the universal map into the
quotient, and, by construction, the universal map ηᴳʳᵖ : A → FA/∾ into
the free group is the composite η/∾ ∘ η where η : A → FA is the
insertion of generators before quotienting and η/∾ is the universal
map into the quotient.
We now need to assume that A is a set to be able to proceed.
\begin{code}
module _ (A-is-set : is-set A) where
smallness-of-ηᴳʳᵖ-fibers-is-prop : {𝓦 : Universe} (y : FA/∾)
→ is-prop (fiber ηᴳʳᵖ y is 𝓦 small)
smallness-of-ηᴳʳᵖ-fibers-is-prop y = prop-being-small-is-prop pe' fe'
(fiber ηᴳʳᵖ y)
(ηᴳʳᵖ-is-embedding A-is-set y)
\end{code}
We first discuss the fibers of η, then those of η/∾, and finally those
of ηᴳʳᵖ.
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 𝓤₀.
\begin{code}
NB-native-universe-fiber-η : η is 𝓤⁺ small-map
NB-native-universe-fiber-η = native-size-of-map η
η-is-decidable : each-fiber-of η is-decidable
η-is-decidable = ∘-decidable-embeddings
[]-is-embedding
pair₀-is-decidable
[]-is-decidable
η-is-embedding : is-embedding η
η-is-embedding = ∘-is-embedding pair₀-is-embedding []-is-embedding
η-has-any-size : (𝓦 : Universe) → η is 𝓦 small-map
η-has-any-size 𝓦 = decidable-embeddings-have-any-size 𝓦
η-is-embedding
η-is-decidable
\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 η". First, this type is a proposition:
\begin{code}
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) β
generator : FA → 𝓤⁺ ̇
generator s = Σ n ꞉ ℕ , Σ ρ ꞉ redex-chain n s , fiber η (chain-reduct s n ρ)
is-generator : FA → 𝓤⁺ ̇
is-generator s = ∥ generator s ∥
being-generator-is-small : (s : FA) → is-generator s is 𝓤 small
being-generator-is-small s =
∥∥-is-small pt
(Σ-is-small
(native-size ℕ)
(λ n → Σ-is-small
(native-size (redex-chain n s))
(λ ρ → η-has-any-size 𝓤 (chain-reduct s n ρ))))
∾-fiber-η-lemma→ : (s : FA) → (Σ a ꞉ A , η a ∾ s) → is-generator s
∾-fiber-η-lemma→ s (a , e) = ∥∥-functor γ e
where
γ : η a ∿ s → generator s
γ e = δ (d c)
where
c : Σ u ꞉ FA , (η a ▷⋆ u) × (s ▷⋆ u)
c = from-∿ Theorem[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) → generator s
δ (n , ρ , p) = n , ρ , a , (p ⁻¹)
∾-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) = δ 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)) ∣
δ : fiber η (chain-reduct s n ρ) → Σ a ꞉ A , η a ∾ s
δ (a , p) = a , transport (_∾ s) (p ⁻¹) e
∾-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 reduce the size of the universal map ηᴳʳᵖ down to 𝓤,
as desired:
\begin{code}
open general-set-quotients-exist sq
fiber-η/∾-lemma : (a : A) (s : FA) → (η/∾ (η a) ＝ η/∾ s) ≃ (η a ∾ s)
fiber-η/∾-lemma a s = logically-equivalent-props-are-equivalent
(/-is-set -∾-)
∥∥-is-prop
η/∾-relates-identified-points
η/∾-identifies-related-points
fiber-ηηᴳʳᵖ-lemma : (s : FA) → fiber ηᴳʳᵖ (η/∾ s) ≃ is-generator s
fiber-ηηᴳʳᵖ-lemma s =
(Σ a ꞉ A , η/∾ (η a) ＝ η/∾ s) ≃⟨ Σ-cong (λ a → fiber-η/∾-lemma a s) ⟩
(Σ a ꞉ A , η a ∾ s) ≃⟨ ∾-fiber-η-lemma s ⟩
is-generator s ■
the-ηᴳʳᵖ-fibers-of-equivalence-classes-are-tiny : (s : FA)
→ fiber ηᴳʳᵖ (η/∾ s) is 𝓤 small
the-ηᴳʳᵖ-fibers-of-equivalence-classes-are-tiny s =
smallness-closed-under-≃'
(being-generator-is-small s)
(fiber-ηηᴳʳᵖ-lemma s)
ηᴳʳᵖ-is-tiny : ηᴳʳᵖ is 𝓤 small-map
ηᴳʳᵖ-is-tiny = /-induction -∾-
smallness-of-ηᴳʳᵖ-fibers-is-prop
the-ηᴳʳᵖ-fibers-of-equivalence-classes-are-tiny
\end{code}
This concludes the proof of Theorem₁.
\begin{code}
Theorem₁[large-free-groups-from-set-quotients] {𝓤} fe pe sq A A-ls =
record
{ 𝓕 = 𝓕
; η = ηᴳʳᵖ
; universality = extension-to-free-group-uniqueness
; η-is-embedding = η-free-group-is-embedding
; η-is-small = ηᴳʳᵖ-is-tiny
}
where
pt : propositional-truncations-exist
pt = propositional-truncations-from-set-quotients sq fe
open general-set-quotients-exist sq
open free-group-construction A
open free-group-construction-step₁ pt
open free-group-construction-step₂ fe (λ 𝓤 → 𝓤) sq (effectivity fe pe sq)
open FreeGroupInterface pt fe (λ 𝓤 → 𝓤) sq (effectivity fe pe sq) A
open resize-universal-map fe pe pt
A
Id⟦ A-ls ⟧
(λ _ → ＝⟦ A-ls ⟧-refl)
(λ _ _ → ＝⟦ A-ls ⟧-gives-＝)
(λ 𝓤 → 𝓤)
sq
(effectivity fe pe sq)
\end{code}
We now use the constructions in the module
resize-universal-map to prove Theorem₂.
\begin{code}
module resize-free-group
(fe : Fun-Ext)
(pe : Prop-Ext)
(pt : propositional-truncations-exist)
{𝓤 : Universe}
(A : 𝓤 ⁺ ̇)
(_＝₀_ : A → A → 𝓤 ̇ )
(refl₀ : (a : A) → a ＝₀ a)
(from-＝₀ : (a b : A) → a ＝₀ b → a ＝ b)
where
open FreeGroupInterface pt fe (_⁺)
(large-set-quotients pt fe pe)
(large-effective-set-quotients pt fe pe)
open resize-universal-map fe pe pt A _＝₀_ refl₀ from-＝₀ (_⁺)
(large-set-quotients pt fe pe)
(large-effective-set-quotients pt fe pe)
open free-group-construction A
\end{code}
Using the results of the module resize-universal-map, we
obtain a relation _≏_ whose propositional truncation is 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-∿ Theorem[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))
open free-group-construction-step₂ fe (_⁺)
(large-set-quotients pt fe pe)
(large-effective-set-quotients pt fe pe)
-∥≏∥- : EqRel {𝓤⁺} {𝓤} FA
-∥≏∥- = _∥≏∥_ , is-equiv-rel-transport _∾_ _∥≏∥_ (λ s t → ∥∥-is-prop)
∾-is-logically-equivalent-to-∥≏∥ ∾-is-equiv-rel
\end{code}
Hence 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}
open general-set-quotients-exist (large-set-quotients pt fe pe)
FA/∥≏∥ : 𝓤⁺ ̇
FA/∥≏∥ = FA / -∥≏∥-
FA/∾-to-FA/∥≏∥ : FA/∾ ≃ FA/∥≏∥
FA/∾-to-FA/∥≏∥ = quotients-equivalent FA -∾- -∥≏∥-
(λ {s} {t} → ∾-is-logically-equivalent-to-∥≏∥ s t)
private
native-universe-of-free-group : 𝓤⁺⁺ ̇
native-universe-of-free-group = ⟨ free-group A ⟩
resized-free-group-carrier : ⟨ free-group A ⟩ is 𝓤⁺ small
resized-free-group-carrier = γ
where
γ : Σ F ꞉ 𝓤⁺ ̇ , F ≃ ⟨ free-group A ⟩
γ = FA/∥≏∥ , ≃-sym FA/∾-to-FA/∥≏∥
\end{code}
The following 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).
NB. If we assume cumulativity in our type theory, the above transport
can be done with univalence directly. TODO. Write down the proof here
in mathematical vernacular (and perhaps also in Agda using --cumulativity).
We conclude with a routine applications of the above development.
\begin{code}
small-free-group : Σ 𝓕' ꞉ Group 𝓤⁺ , 𝓕' ≅ 𝓕
small-free-group = group-copy 𝓕 resized-free-group-carrier
𝓕⁻ : Group 𝓤⁺
𝓕⁻ = pr₁ small-free-group
𝕜 : 𝓕⁻ ≅ 𝓕
𝕜 = pr₂ small-free-group
k : ⟨ 𝓕⁻ ⟩ ≃ ⟨ 𝓕 ⟩
k = ≅-to-≃ 𝓕⁻ 𝓕 𝕜
k-is-hom : is-hom 𝓕⁻ 𝓕 ⌜ k ⌝
k-is-hom = ≅-to-≃-is-hom 𝓕⁻ 𝓕 𝕜
η⁻ : A → ⟨ 𝓕⁻ ⟩
η⁻ = ⌜ k ⌝⁻¹ ∘ ηᴳʳᵖ
universality⁻ : {𝓦 : Universe} (𝓖 : Group 𝓦) (f : A → ⟨ 𝓖 ⟩)
→ ∃! f̅ ꞉ (⟨ 𝓕⁻ ⟩ → ⟨ 𝓖 ⟩)
, is-hom 𝓕⁻ 𝓖 f̅
× f̅ ∘ η⁻ ∼ f
universality⁻ 𝓖 f =
equiv-to-singleton I (extension-to-free-group-uniqueness A 𝓖 f)
where
I : (Σ g ꞉ (⟨ 𝓕⁻ ⟩ → ⟨ 𝓖 ⟩) , is-hom 𝓕⁻ 𝓖 g × g ∘ η⁻ ∼ f)
≃ (Σ h ꞉ (⟨ 𝓕 ⟩ → ⟨ 𝓖 ⟩) , is-hom 𝓕 𝓖 h × h ∘ ηᴳʳᵖ ∼ f)
I = qinveq ϕ (ψ , ψϕ , ϕψ)
where
ϕ : (Σ g ꞉ (⟨ 𝓕⁻ ⟩ → ⟨ 𝓖 ⟩) , is-hom 𝓕⁻ 𝓖 g × g ∘ η⁻ ∼ f)
→ (Σ h ꞉ (⟨ 𝓕 ⟩ → ⟨ 𝓖 ⟩) , is-hom 𝓕 𝓖 h × h ∘ ηᴳʳᵖ ∼ f)
ϕ (g , i , e) = g ∘ ⌜ k ⌝⁻¹ ,
∘-is-hom 𝓕 𝓕⁻ 𝓖 ⌜ k ⌝⁻¹ g
(inverses-are-homs' 𝓕⁻ 𝓕 k k-is-hom)
i ,
e
ψ : codomain ϕ → domain ϕ
ψ (h , j , d) = h ∘ ⌜ k ⌝ ,
∘-is-hom 𝓕⁻ 𝓕 𝓖 ⌜ k ⌝ h k-is-hom j ,
d'
where
d' : (a : A) → h (⌜ k ⌝ (η⁻ a)) ＝ f a
d' a = h (⌜ k ⌝ (η⁻ a)) ＝⟨ refl ⟩
h (⌜ k ⌝ (⌜ k ⌝⁻¹ (ηᴳʳᵖ a))) ＝⟨ III ⟩
h (ηᴳʳᵖ a) ＝⟨ d a ⟩
f a ∎
where
III = ap h (inverses-are-sections' k (ηᴳʳᵖ a))
ϕψ : ϕ ∘ ψ ∼ id
ϕψ (h , j , d) = to-subtype-＝
(λ f → ×-is-prop
(being-hom-is-prop fe 𝓕 𝓖 f)
(Π-is-prop fe (λ _ → groups-are-sets 𝓖)))
(dfunext fe (λ x → ap h (inverses-are-sections' k x)))
ψϕ : ψ ∘ ϕ ∼ id
ψϕ (g , i , e) = to-subtype-＝
(λ f → ×-is-prop
(being-hom-is-prop fe 𝓕⁻ 𝓖 f)
(Π-is-prop fe (λ _ → groups-are-sets 𝓖)))
(dfunext fe (λ y → ap g (inverses-are-retractions' k y)))
η⁻-is-embedding : is-set A → is-embedding η⁻
η⁻-is-embedding i = ∘-is-embedding
(η-free-group-is-embedding A i)
(equivs-are-embeddings' (≃-sym k))
η⁻-is-large : ηᴳʳᵖ is 𝓤⁺⁺ small-map
η⁻-is-large = native-size-of-map ηᴳʳᵖ
⌜k⌝⁻¹-is-tiny : ⌜ k ⌝⁻¹ is 𝓤 small-map
⌜k⌝⁻¹-is-tiny = equivs-have-any-size' (≃-sym k)
η⁻-is-tiny : is-set A → η⁻ is 𝓤 small-map
η⁻-is-tiny i = ∘-small-maps (ηᴳʳᵖ-is-tiny i) ⌜k⌝⁻¹-is-tiny
\end{code}
This concludes the proof of Theorem₂.
\begin{code}
Theorem₂[free-groups-of-large-locally-small-types] {𝓤} pt fe pe A A-ls =
record
{ 𝓕 = 𝓕⁻
; η = η⁻
; universality = universality⁻
; η-is-embedding = η⁻-is-embedding
; η-is-small = η⁻-is-tiny
}
where
open resize-free-group fe pe pt
A
Id⟦ A-ls ⟧
(λ _ → ＝⟦ A-ls ⟧-refl)
(λ _ _ → ＝⟦ A-ls ⟧-gives-＝)
\end{code}