diff --git a/Decidable/Sets.agda b/Decidable/Sets.agda
index 97948cc..a1fe0b0 100644
--- a/Decidable/Sets.agda
+++ b/Decidable/Sets.agda
@@ -4,6 +4,5 @@ open import LogicalFormulae
 
 module Decidable.Sets where
 
-record DecidableSet {a : _} (A : Set a) : Set a where
-  field
-    eq : (a b : A) → ((a ≡ b) || ((a ≡ b) → False))
+DecidableSet : {a : _} (A : Set a) → Set a
+DecidableSet A = (a b : A) → ((a ≡ b) || ((a ≡ b) → False))
diff --git a/Everything/Safe.agda b/Everything/Safe.agda
index 13e7bb9..96da870 100644
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -95,6 +95,8 @@ open import Setoids.Functions.Extension
 open import Setoids.Algebra.Lemmas
 open import Setoids.Intersection.Lemmas
 open import Setoids.Union.Lemmas
+open import Setoids.Cardinality.Infinite.Lemmas
+open import Setoids.Cardinality.Finite.Definition
 
 open import Sets.Cardinality.Infinite.Examples
 open import Sets.Cardinality.Infinite.Lemmas
diff --git a/Everything/WithK.agda b/Everything/WithK.agda
index 772735f..f69f006 100644
--- a/Everything/WithK.agda
+++ b/Everything/WithK.agda
@@ -19,6 +19,7 @@ open import Sets.FinSetWithK
 open import Rings.Examples.Examples
 open import Rings.Examples.Proofs
 
+open import Groups.FreeGroup.Lemmas
 open import Groups.FreeGroup.UniversalProperty
 open import Groups.FreeGroup.Parity
 open import Groups.FreeProduct.UniversalProperty
diff --git a/Groups/Cyclic/Lemmas.agda b/Groups/Cyclic/Lemmas.agda
index 50d9a81..e3e6af6 100644
--- a/Groups/Cyclic/Lemmas.agda
+++ b/Groups/Cyclic/Lemmas.agda
@@ -8,7 +8,7 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import Numbers.Naturals.Definition
 open import Numbers.Integers.Integers
 open import Numbers.Integers.Addition
-open import Sets.FinSet
+open import Sets.FinSet.Definition
 open import Groups.Homomorphisms.Definition
 open import Groups.Groups
 open import Groups.Subgroups.Definition
diff --git a/Groups/FreeGroup/Definition.agda b/Groups/FreeGroup/Definition.agda
index b3932b3..a48ef1d 100644
--- a/Groups/FreeGroup/Definition.agda
+++ b/Groups/FreeGroup/Definition.agda
@@ -17,6 +17,10 @@ data FreeCompletion {a : _} (A : Set a) : Set a where
   ofLetter : A → FreeCompletion A
   ofInv : A → FreeCompletion A
 
+freeCompletionMap : {a b : _} {A : Set a} {B : Set b} (f : A → B) (w : FreeCompletion A) → FreeCompletion B
+freeCompletionMap f (ofLetter x) = ofLetter (f x)
+freeCompletionMap f (ofInv x) = ofInv (f x)
+
 freeInverse : {a : _} {A : Set a} (l : FreeCompletion A) → FreeCompletion A
 freeInverse (ofLetter x) = ofInv x
 freeInverse (ofInv x) = ofLetter x
@@ -27,8 +31,11 @@ ofLetterInjective refl = refl
 ofInvInjective : {a : _} {A : Set a} {x y : A} → (ofInv x ≡ ofInv y) → x ≡ y
 ofInvInjective refl = refl
 
+ofLetterOfInv : {a : _} {A : Set a} {x y : A} → ofLetter x ≡ ofInv y → False
+ofLetterOfInv ()
+
 decidableFreeCompletion : {a : _} {A : Set a} → DecidableSet A → DecidableSet (FreeCompletion A)
-decidableFreeCompletion {A = A} record { eq = dec } = record { eq = pr }
+decidableFreeCompletion {A = A} dec = pr
   where
     pr : (a b : FreeCompletion A) → (a ≡ b) || (a ≡ b → False)
     pr (ofLetter x) (ofLetter y) with dec x y
@@ -41,17 +48,17 @@ decidableFreeCompletion {A = A} record { eq = dec } = record { eq = pr }
     ... | inr x!=y = inr λ p → x!=y (ofInvInjective p)
 
 freeCompletionEqual : {a : _} {A : Set a} (dec : DecidableSet A) (x y : FreeCompletion A) → Bool
-freeCompletionEqual dec x y with DecidableSet.eq (decidableFreeCompletion dec) x y
+freeCompletionEqual dec x y with decidableFreeCompletion dec x y
 freeCompletionEqual dec x y | inl x₁ = BoolTrue
 freeCompletionEqual dec x y | inr x₁ = BoolFalse
 
 freeCompletionEqualFalse : {a : _} {A : Set a} (dec : DecidableSet A) {x y : FreeCompletion A} → ((x ≡ y) → False) → (freeCompletionEqual dec x y) ≡ BoolFalse
-freeCompletionEqualFalse dec {x = x} {y} x!=y with DecidableSet.eq (decidableFreeCompletion dec) x y
+freeCompletionEqualFalse dec {x = x} {y} x!=y with decidableFreeCompletion dec x y
 freeCompletionEqualFalse dec {x} {y} x!=y | inl x=y = exFalso (x!=y x=y)
 freeCompletionEqualFalse dec {x} {y} x!=y | inr _ = refl
 
 freeCompletionEqualFalse' : {a : _} {A : Set a} (dec : DecidableSet A) {x y : FreeCompletion A} → .((freeCompletionEqual dec x y) ≡ BoolFalse) → (x ≡ y) → False
-freeCompletionEqualFalse' dec {x} {y} pr with DecidableSet.eq (decidableFreeCompletion dec) x y
+freeCompletionEqualFalse' dec {x} {y} pr with decidableFreeCompletion dec x y
 freeCompletionEqualFalse' dec {x} {y} () | inl x₁
 freeCompletionEqualFalse' dec {x} {y} pr | inr ans = ans
 
diff --git a/Groups/FreeGroup/Group.agda b/Groups/FreeGroup/Group.agda
index 6c0fc48..4bf45c1 100644
--- a/Groups/FreeGroup/Group.agda
+++ b/Groups/FreeGroup/Group.agda
@@ -15,10 +15,10 @@ open import Groups.FreeGroup.Word decA
 prepend : ReducedWord → FreeCompletion A → ReducedWord
 prepend empty x = prependLetter x empty (wordEmpty refl)
 prepend (prependLetter (ofLetter y) w pr) (ofLetter x) = prependLetter (ofLetter x) (prependLetter (ofLetter y) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA {ofLetter x} {ofInv x} λ ()))
-prepend (prependLetter (ofInv y) w pr) (ofLetter x) with DecidableSet.eq decA x y
+prepend (prependLetter (ofInv y) w pr) (ofLetter x) with decA x y
 ... | inl x=y = w
 ... | inr x!=y = prependLetter (ofLetter x) (prependLetter (ofInv y) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA {ofLetter x} {ofLetter y} λ pr → x!=y (ofLetterInjective pr)))
-prepend (prependLetter (ofLetter y) w pr) (ofInv x) with DecidableSet.eq decA x y
+prepend (prependLetter (ofLetter y) w pr) (ofInv x) with decA x y
 ... | inl x=y = w
 ... | inr x!=y = prependLetter (ofInv x) (prependLetter (ofLetter y) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA λ pr → x!=y (ofInvInjective pr)))
 prepend (prependLetter (ofInv y) w pr) (ofInv x) = prependLetter (ofInv x) (prependLetter (ofInv y) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA {ofInv x} {ofLetter x} (λ ())))
@@ -30,50 +30,50 @@ prependLetter letter a x +W b = prepend (a +W b) letter
 prependValid : (w : ReducedWord) (l : A) → (x : PrependIsValid w (ofLetter l)) → prepend w (ofLetter l) ≡ prependLetter (ofLetter l) w x
 prependValid empty l (wordEmpty refl) = refl
 prependValid (prependLetter (ofLetter l2) w x) l pr = prependLetterRefl
-prependValid (prependLetter (ofInv l2) w x) l pr with DecidableSet.eq decA l l2
+prependValid (prependLetter (ofInv l2) w x) l pr with decA l l2
 prependValid (prependLetter (ofInv l2) w x) .l2 (wordEnding _ x1) | inl refl = exFalso (freeCompletionEqualFalse' decA x1 refl)
 ... | inr l!=l2 = prependLetterRefl
 
 prependValid' : (w : ReducedWord) (l : A) → (x : PrependIsValid w (ofInv l)) → prepend w (ofInv l) ≡ prependLetter (ofInv l) w x
 prependValid' empty l (wordEmpty refl) = refl
-prependValid' (prependLetter (ofLetter l2) w x) l pr with DecidableSet.eq decA l l2
+prependValid' (prependLetter (ofLetter l2) w x) l pr with decA l l2
 prependValid' (prependLetter (ofLetter l2) w x) .l2 (wordEnding _ x1) | inl refl = exFalso (freeCompletionEqualFalse' decA x1 refl)
 ... | inr l!=l2 = prependLetterRefl
 prependValid' (prependLetter (ofInv l2) w x) l pr = prependLetterRefl
 
 prependInv : (w : ReducedWord) (l : A) → prepend (prepend w (ofLetter l)) (ofInv l) ≡ w
-prependInv empty l with DecidableSet.eq decA l l
+prependInv empty l with decA l l
 ... | inl l=l = refl
 ... | inr l!=l = exFalso (l!=l refl)
-prependInv (prependLetter (ofLetter l2) w x) l with DecidableSet.eq decA l l
+prependInv (prependLetter (ofLetter l2) w x) l with decA l l
 ... | inl l=l = refl
 ... | inr l!=l = exFalso (l!=l refl)
-prependInv (prependLetter (ofInv l2) w x) l with DecidableSet.eq decA l l2
+prependInv (prependLetter (ofInv l2) w x) l with decA l l2
 prependInv (prependLetter (ofInv l2) w x) .l2 | inl refl = prependValid' w l2 x
-... | inr l!=l2 with DecidableSet.eq decA l l
+... | inr l!=l2 with decA l l
 prependInv (prependLetter (ofInv l2) w x) l | inr l!=l2 | inl refl = refl
 prependInv (prependLetter (ofInv l2) w x) l | inr l!=l2 | inr bad = exFalso (bad refl)
 
 prependInv' : (w : ReducedWord) (l : A) → prepend (prepend w (ofInv l)) (ofLetter l) ≡ w
-prependInv' empty l with DecidableSet.eq decA l l
+prependInv' empty l with decA l l
 ... | inl l=l = refl
 ... | inr l!=l = exFalso (l!=l refl)
-prependInv' (prependLetter (ofLetter l2) w x) l with DecidableSet.eq decA l l2
+prependInv' (prependLetter (ofLetter l2) w x) l with decA l l2
 prependInv' (prependLetter (ofLetter l2) w x) .l2 | inl refl = prependValid w l2 x
-... | inr l!=l2 with DecidableSet.eq decA l l
+... | inr l!=l2 with decA l l
 ... | inl refl = refl
 ... | inr l!=l = exFalso (l!=l refl)
-prependInv' (prependLetter (ofInv l2) w x) l with DecidableSet.eq decA l l
+prependInv' (prependLetter (ofInv l2) w x) l with decA l l
 prependInv' (prependLetter (ofInv l2) w x) l | inl refl = refl
 prependInv' (prependLetter (ofInv l2) w x) l | inr l!=l = exFalso (l!=l refl)
 
 prependAndAdd : (a b : ReducedWord) (l : FreeCompletion A) → prepend (a +W b) l ≡ (prepend a l) +W b
 prependAndAdd empty b l = refl
 prependAndAdd (prependLetter (ofLetter x) w pr) b (ofLetter y) = refl
-prependAndAdd (prependLetter (ofLetter x) w pr) b (ofInv y) with DecidableSet.eq decA y x
+prependAndAdd (prependLetter (ofLetter x) w pr) b (ofInv y) with decA y x
 prependAndAdd (prependLetter (ofLetter x) w pr) b (ofInv .x) | inl refl = prependInv _ _
 ... | inr y!=x = refl
-prependAndAdd (prependLetter (ofInv x) w pr) b (ofLetter y) with DecidableSet.eq decA y x
+prependAndAdd (prependLetter (ofInv x) w pr) b (ofLetter y) with decA y x
 prependAndAdd (prependLetter (ofInv x) w pr) b (ofLetter .x) | inl refl = prependInv' _ _
 ... | inr y!=x = refl
 prependAndAdd (prependLetter (ofInv x) w pr) b (ofInv y) = refl
@@ -96,13 +96,13 @@ invLeftW empty = refl
 invLeftW (prependLetter (ofLetter l) a x) rewrite equalityCommutative (+WAssoc (inverseW a) (prependLetter (ofInv l) empty (wordEmpty refl)) (prependLetter (ofLetter l) a x)) = t
   where
     t : (inverseW a +W (prepend (prependLetter (ofLetter l) a x) (ofInv l))) ≡ empty
-    t with DecidableSet.eq decA l l
+    t with decA l l
     ... | inl refl = invLeftW a
     ... | inr l!=l = exFalso (l!=l refl)
 invLeftW (prependLetter (ofInv l) a x) rewrite equalityCommutative (+WAssoc (inverseW a) (prependLetter (ofLetter l) empty (wordEmpty refl)) (prependLetter (ofInv l) a x)) = t
   where
     t : (inverseW a +W (prepend (prependLetter (ofInv l) a x) (ofLetter l))) ≡ empty
-    t with DecidableSet.eq decA l l
+    t with decA l l
     ... | inl refl = invLeftW a
     ... | inr l!=l = exFalso (l!=l refl)
 
@@ -111,13 +111,13 @@ invRightW empty = refl
 invRightW (prependLetter (ofLetter l) a x) rewrite +WAssoc a (inverseW a) (prependLetter (ofInv l) empty (wordEmpty refl)) | invRightW a = t
   where
     t : prepend (prependLetter (ofInv l) empty (wordEmpty refl)) (ofLetter l) ≡ empty
-    t with DecidableSet.eq decA l l
+    t with decA l l
     ... | inl refl = refl
     ... | inr l!=l = exFalso (l!=l refl)
 invRightW (prependLetter (ofInv l) a x) rewrite +WAssoc a (inverseW a) (prependLetter (ofLetter l) empty (wordEmpty refl)) | invRightW a = t
   where
     t : prepend (prependLetter (ofLetter l) empty (wordEmpty refl)) (ofInv l) ≡ empty
-    t with DecidableSet.eq decA l l
+    t with decA l l
     ... | inl refl = refl
     ... | inr l!=l = exFalso (l!=l refl)
 
diff --git a/Groups/FreeGroup/Lemmas.agda b/Groups/FreeGroup/Lemmas.agda
index 79e5d45..bcbd432 100644
--- a/Groups/FreeGroup/Lemmas.agda
+++ b/Groups/FreeGroup/Lemmas.agda
@@ -1,11 +1,13 @@
 {-# OPTIONS --safe --warning=error #-}
 
+open import Sets.Cardinality.Infinite.Definition
 open import Sets.EquivalenceRelations
 open import Setoids.Setoids
 open import Groups.FreeGroup.Definition
 open import Groups.Homomorphisms.Definition
 open import Groups.Definition
 open import Decidable.Sets
+open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 open import LogicalFormulae
 open import Semirings.Definition
@@ -14,18 +16,116 @@ open import Groups.Isomorphisms.Definition
 open import Groups.FreeGroup.Word
 open import Groups.FreeGroup.Group
 open import Groups.FreeGroup.UniversalProperty
+open import Groups.Abelian.Definition
+open import Groups.QuotientGroup.Definition
+open import Groups.Lemmas
+open import Groups.Homomorphisms.Lemmas
 
 module Groups.FreeGroup.Lemmas {a : _} {A : Set a} (decA : DecidableSet A) where
 
-freeGroupFunctorWellDefined : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → Bijection f → GroupsIsomorphic (freeGroup decA) (freeGroup decB)
-GroupsIsomorphic.isomorphism (freeGroupFunctorWellDefined decB {f} bij) = universalPropertyFunction decA (freeGroup decB) λ a → freeEmbedding decB (f a)
-GroupIso.groupHom (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)) = universalPropertyHom decA (freeGroup decB) λ a → freeEmbedding decB (f a)
-GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)) = {!!}
+freeGroupNonAbelian : AbelianGroup (freeGroup decA) → (a : A) → Sg (A → True) Bijection
+freeGroupNonAbelian record { commutative = commutative } a = (λ _ → record {}) , b
+  where
+    b : Bijection (λ _ → record {})
+    Bijection.inj b {x} {y} _ with decA x y
+    ... | inl pr = pr
+    ... | inr neq = exFalso (neq (ofLetterInjective (prependLetterInjective' decA t)))
+      where
+        t : prependLetter {decA = decA} (ofLetter x) (prependLetter (ofLetter y) empty (wordEmpty refl)) (wordEnding (succIsPositive 0) refl) ≡ prependLetter (ofLetter y) (prependLetter (ofLetter x) empty (wordEmpty refl)) (wordEnding (succIsPositive 0) refl)
+        t = commutative {prependLetter (ofLetter x) empty (wordEmpty refl)} {prependLetter (ofLetter y) empty (wordEmpty refl)}
+    Bijection.surj b record {} = a , refl
 
 private
-  subgroupGeneratedBySquares : {c d : _} {C : Set c} {S : Setoid {c} {d} C} {_+_ : C → C → C} (G : Group S _+_) → Set
-  sub
+  iso : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → Bijection f → ReducedWord decA → ReducedWord decB
+  iso decB {f} bij = universalPropertyFunction decA (freeGroup decB) λ a → freeEmbedding decB (f a)
 
+  isoHom : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → GroupHom (freeGroup decA) (freeGroup decB) (iso decB bij)
+  isoHom decB {f} bij = universalPropertyHom decA (freeGroup decB) λ a → iso decB bij (freeEmbedding decA a)
 
+  iso2 : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → Bijection f → ReducedWord decB → ReducedWord decA
+  iso2 decB {f} bij = universalPropertyFunction decB (freeGroup decA) λ b → freeEmbedding decA (Invertible.inverse (bijectionImpliesInvertible bij) b)
+
+  iso2Hom : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → GroupHom (freeGroup decB) (freeGroup decA) (iso2 decB bij)
+  iso2Hom decB {f} bij = universalPropertyHom decB (freeGroup decA) λ b → iso2 decB bij (freeEmbedding decB b)
+
+  fixesF : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : A) → iso2 decB bij (iso decB bij (freeEmbedding decA x)) ≡ freeEmbedding decA x
+  fixesF decB {f} bij x with Bijection.surj bij (f x)
+  ... | _ , pr rewrite Bijection.inj bij pr = refl
+
+  fixesF' : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : B) → iso decB bij (iso2 decB bij (freeEmbedding decB x)) ≡ freeEmbedding decB x
+  fixesF' decB {f} bij x with Bijection.surj bij x
+  ... | _ , pr rewrite pr = refl
+
+  uniq : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decA) → x ≡ universalPropertyFunction decA (freeGroup decA) (λ x → iso2 decB bij (iso decB bij (freeEmbedding decA x))) x
+  uniq decB {f} bij x = universalPropertyUniqueness decA (freeGroup decA) (λ x → iso2 decB bij (iso decB bij (freeEmbedding decA x))) {id} (record { wellDefined = id ; groupHom = refl }) (fixesF decB bij) x
+  uniqLemm : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decA) → iso2 decB bij (iso decB bij x) ≡ universalPropertyFunction decA (freeGroup decA) (λ x → iso2 decB bij (iso decB bij (freeEmbedding decA x))) x
+  uniqLemm decB {f} bij x = universalPropertyUniqueness decA (freeGroup decA) (λ i → freeEmbedding decA (underlying (Bijection.surj bij (f i)))) {λ i → iso2 decB bij (iso decB bij i)} (groupHomsCompose (isoHom decB bij) (iso2Hom decB bij)) (λ _ → refl) x
+  uniq! : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decA) → iso2 decB bij (iso decB bij x) ≡ x
+  uniq! decB bij x = transitivity (uniqLemm decB bij x) (equalityCommutative (uniq decB bij x))
+
+  uniq' : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decB) → x ≡ universalPropertyFunction decB (freeGroup decB) (λ x → iso decB bij (iso2 decB bij (freeEmbedding decB x))) x
+  uniq' decB {f} bij x = universalPropertyUniqueness decB (freeGroup decB) (λ x → iso decB bij (iso2 decB bij (freeEmbedding decB x))) {id} (record { wellDefined = id ; groupHom = refl }) (fixesF' decB bij) x
+  uniq'Lemm : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decB) → iso decB bij (iso2 decB bij x) ≡ universalPropertyFunction decB (freeGroup decB) (λ x → iso decB bij (iso2 decB bij (freeEmbedding decB x))) x
+  uniq'Lemm decB {f} bij x = universalPropertyUniqueness decB (freeGroup decB) (λ i → freeEmbedding decB (f (Invertible.inverse (bijectionImpliesInvertible bij) i))) {λ i → iso decB bij (iso2 decB bij i)} (groupHomsCompose (iso2Hom decB bij) (isoHom decB bij)) (λ _ → refl) x
+  uniq'! : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decB) → iso decB bij (iso2 decB bij x) ≡ x
+  uniq'! decB bij x = transitivity (uniq'Lemm decB bij x) (equalityCommutative (uniq' decB bij x))
+
+  inBijection : {b : _} {B : Set b} (decB : DecidableSet B) {f : A → B} (bij : Bijection f) → Bijection (iso decB bij)
+  inBijection decB bij = invertibleImpliesBijection (record { inverse = iso2 decB bij ; isLeft = uniq'! decB bij ; isRight = uniq! decB bij })
+
+freeGroupFunctorWellDefined : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → Bijection f → GroupsIsomorphic (freeGroup decA) (freeGroup decB)
+GroupsIsomorphic.isomorphism (freeGroupFunctorWellDefined decB {f} bij) = iso decB bij
+GroupIso.groupHom (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)) = universalPropertyHom decA (freeGroup decB) λ a → freeEmbedding decB (f a)
+SetoidInjection.wellDefined (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)))) refl = refl
+SetoidInjection.injective (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)))) {x} {y} pr = Bijection.inj (inBijection decB bij) pr
+SetoidSurjection.wellDefined (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)))) refl = refl
+SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)))) {x} = Bijection.surj (inBijection decB bij) x
+
+{-
 freeGroupFunctorInjective : {b : _} {B : Set b} (decB : DecidableSet B) → GroupsIsomorphic (freeGroup decA) (freeGroup decB) → Sg (A → B) (λ f → Bijection f)
 freeGroupFunctorInjective decB iso = {!!}
+
+everyGroupQuotientOfFreeGroup : {b : _} → (S : Setoid {a} {b} A) → {_+_ : A → A → A} → (G : Group S _+_) → GroupsIsomorphic G (quotientGroupByHom (freeGroup decA) (universalPropertyHom decA {!!} {!!}))
+everyGroupQuotientOfFreeGroup = {!!}
+
+everyFGGroupQuotientOfFGFreeGroup : {!!}
+everyFGGroupQuotientOfFGFreeGroup = {!!}
+
+freeGroupTorsionFree : {!!}
+freeGroupTorsionFree = {!!}
+-}
+
+private
+  mapNToGrp : (a : A) → (n : ℕ) → ReducedWord decA
+  mapNToGrpLen : (a : A) → (n : ℕ) → wordLength decA (mapNToGrp a n) ≡ n
+  mapNToGrpFirstLetter : (a : A) → (n : ℕ) → .(pr : 0 <N wordLength decA (mapNToGrp a (succ n))) → firstLetter decA (mapNToGrp a (succ n)) pr ≡ (ofLetter a)
+  lemma : (a : A) → (n : ℕ) → .(pr : 0 <N wordLength decA (mapNToGrp a (succ n))) → ofLetter a ≡ freeInverse (firstLetter decA (mapNToGrp a (succ n)) pr) → False
+
+  lemma a zero _ ()
+  lemma a (succ n) _ ()
+
+  mapNToGrp a zero = empty
+  mapNToGrp a 1 = prependLetter (ofLetter a) empty (wordEmpty refl)
+  mapNToGrp a (succ (succ n)) = prependLetter (ofLetter a) (mapNToGrp a (succ n)) (wordEnding (identityOfIndiscernablesRight _<N_ (succIsPositive n) (equalityCommutative (mapNToGrpLen a (succ n)))) (freeCompletionEqualFalse decA λ p → lemma a n ((identityOfIndiscernablesRight _<N_ (succIsPositive n) (equalityCommutative (mapNToGrpLen a (succ n))))) p))
+
+  mapNToGrpFirstLetter a zero pr = refl
+  mapNToGrpFirstLetter a (succ n) pr = refl
+
+  mapNToGrpLen a zero = refl
+  mapNToGrpLen a (succ zero) = refl
+  mapNToGrpLen a (succ (succ n)) = applyEquality succ (mapNToGrpLen a (succ n))
+
+  mapNToGrpInj : (a : A) → (x y : ℕ) → mapNToGrp a x ≡ mapNToGrp a y → x ≡ y
+  mapNToGrpInj a zero zero pr = refl
+  mapNToGrpInj a zero (succ zero) ()
+  mapNToGrpInj a zero (succ (succ y)) ()
+  mapNToGrpInj a (succ zero) zero ()
+  mapNToGrpInj a (succ (succ x)) zero ()
+  mapNToGrpInj a (succ zero) (succ zero) pr = refl
+  mapNToGrpInj a (succ zero) (succ (succ y)) pr = exFalso (naughtE (transitivity (applyEquality (wordLength decA) (prependLetterInjective decA pr)) (mapNToGrpLen a (succ y))))
+  mapNToGrpInj a (succ (succ x)) (succ 0) pr = exFalso (naughtE (transitivity (equalityCommutative (applyEquality (wordLength decA) (prependLetterInjective decA pr))) (mapNToGrpLen a (succ x))))
+  mapNToGrpInj a (succ (succ x)) (succ (succ y)) pr = applyEquality succ (mapNToGrpInj a (succ x) (succ y) (prependLetterInjective decA pr))
+
+freeGroupInfinite : (nonempty : A) → DedekindInfiniteSet (ReducedWord decA)
+DedekindInfiniteSet.inj (freeGroupInfinite nonempty) = mapNToGrp nonempty
+DedekindInfiniteSet.isInjection (freeGroupInfinite nonempty) {x} {y} = mapNToGrpInj nonempty x y
diff --git a/Groups/FreeGroup/Parity.agda b/Groups/FreeGroup/Parity.agda
index 9ede50d..8964c1e 100644
--- a/Groups/FreeGroup/Parity.agda
+++ b/Groups/FreeGroup/Parity.agda
@@ -48,97 +48,97 @@ notWellDefined {BoolFalse} {BoolFalse} x=y = refl
 
 parity : (x : A) → ReducedWord → Bool
 parity x empty = BoolFalse
-parity x (prependLetter (ofLetter y) w _) with DecidableSet.eq decA x y
+parity x (prependLetter (ofLetter y) w _) with decA x y
 parity x (prependLetter (ofLetter y) w _) | inl _ = not (parity x w)
 parity x (prependLetter (ofLetter y) w _) | inr _ = parity x w
-parity x (prependLetter (ofInv y) w _) with DecidableSet.eq decA x y
+parity x (prependLetter (ofInv y) w _) with decA x y
 parity x (prependLetter (ofInv y) w _) | inl _ = not (parity x w)
 parity x (prependLetter (ofInv y) w _) | inr _ = parity x w
 
 parityPrepend : (a : A) (w : ReducedWord) (l : A) → ((a ≡ l) → False) → parity a (prepend w (ofLetter l)) ≡ parity a w
-parityPrepend a empty l notEq with DecidableSet.eq decA a l
+parityPrepend a empty l notEq with decA a l
 parityPrepend a empty l notEq | inl x = exFalso (notEq x)
 parityPrepend a empty l notEq | inr x = refl
-parityPrepend a (prependLetter (ofLetter r) w x) l notEq with DecidableSet.eq decA a l
+parityPrepend a (prependLetter (ofLetter r) w x) l notEq with decA a l
 parityPrepend a (prependLetter (ofLetter r) w x) l notEq | inl m = exFalso (notEq m)
 parityPrepend a (prependLetter (ofLetter r) w x) l notEq | inr _ = refl
-parityPrepend a (prependLetter (ofInv r) w x) l notEq with DecidableSet.eq decA a r
-parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r with DecidableSet.eq decA l r
+parityPrepend a (prependLetter (ofInv r) w x) l notEq with decA a r
+parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r with decA l r
 parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inl l=r = exFalso (notEq (transitivity a=r (equalityCommutative l=r)))
-parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r with DecidableSet.eq decA a l
+parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r with decA a l
 parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inl a=l = exFalso (notEq a=l)
-parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l with DecidableSet.eq decA a r
+parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l with decA a r
 parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l | inl x₁ = refl
 parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l | inr bad = exFalso (bad a=r)
-parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r with DecidableSet.eq decA l r
+parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r with decA l r
 parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl x₁ = refl
-parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r with DecidableSet.eq decA a l
+parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r with decA a l
 parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inl a=l = exFalso (notEq a=l)
-parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l with DecidableSet.eq decA a r
+parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l with decA a r
 parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l | inl a=r = exFalso (a!=r a=r)
 parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l | inr x₁ = refl
 
 parityPrepend' : (a : A) (w : ReducedWord) (l : A) → ((a ≡ l) → False) → parity a (prepend w (ofInv l)) ≡ parity a w
-parityPrepend' a empty l notEq with DecidableSet.eq decA a l
+parityPrepend' a empty l notEq with decA a l
 parityPrepend' a empty l notEq | inl x = exFalso (notEq x)
 parityPrepend' a empty l notEq | inr x = refl
-parityPrepend' a (prependLetter (ofLetter r) w x) l notEq with DecidableSet.eq decA l r
-parityPrepend' a (prependLetter (ofLetter r) w x) l notEq | inl m with DecidableSet.eq decA a r
+parityPrepend' a (prependLetter (ofLetter r) w x) l notEq with decA l r
+parityPrepend' a (prependLetter (ofLetter r) w x) l notEq | inl m with decA a r
 ... | inl a=r = exFalso (notEq (transitivity a=r (equalityCommutative m)))
 ... | inr a!=r = refl
-parityPrepend' a (prependLetter (ofLetter r) w x) l notEq | inr l!=r with DecidableSet.eq decA a l
+parityPrepend' a (prependLetter (ofLetter r) w x) l notEq | inr l!=r with decA a l
 ... | inl a=l = exFalso (notEq a=l)
 ... | inr a!=l = refl
-parityPrepend' a (prependLetter (ofInv r) w x) l notEq with DecidableSet.eq decA a r
-parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r with DecidableSet.eq decA l r
+parityPrepend' a (prependLetter (ofInv r) w x) l notEq with decA a r
+parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r with decA l r
 parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inl l=r = exFalso (notEq (transitivity a=r (equalityCommutative l=r)))
-parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r with DecidableSet.eq decA a l
+parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r with decA a l
 parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inl a=l = exFalso (notEq a=l)
-parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l with DecidableSet.eq decA a r
+parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l with decA a r
 parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l | inl x₁ = refl
 parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l | inr bad = exFalso (bad a=r)
-parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r with DecidableSet.eq decA l r
-parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl l=r with DecidableSet.eq decA a l
+parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r with decA l r
+parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl l=r with decA a l
 parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl l=r | inl a=l = exFalso (notEq a=l)
-parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl l=r | inr a!=l with DecidableSet.eq decA a r
+parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl l=r | inr a!=l with decA a r
 ... | inl a=r = exFalso (a!=r a=r)
 ... | inr _ = refl
-parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r with DecidableSet.eq decA a l
+parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r with decA a l
 parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inl a=l = exFalso (notEq a=l)
-parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l with DecidableSet.eq decA a r
+parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l with decA a r
 parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l | inl a=r = exFalso (a!=r a=r)
 parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l | inr x₁ = refl
 
 parityPrepend'' : (a : A) (w : ReducedWord) → parity a (prepend w (ofLetter a)) ≡ not (parity a w)
-parityPrepend'' a empty with DecidableSet.eq decA a a
+parityPrepend'' a empty with decA a a
 ... | inl _ = refl
 ... | inr bad = exFalso (bad refl)
-parityPrepend'' a (prependLetter (ofLetter l) w x) with DecidableSet.eq decA a a
-parityPrepend'' a (prependLetter (ofLetter l) w x) | inl _ with DecidableSet.eq decA a l
+parityPrepend'' a (prependLetter (ofLetter l) w x) with decA a a
+parityPrepend'' a (prependLetter (ofLetter l) w x) | inl _ with decA a l
 parityPrepend'' a (prependLetter (ofLetter l) w x) | inl _ | inl a=l = refl
 parityPrepend'' a (prependLetter (ofLetter l) w x) | inl _ | inr a!=l = refl
 parityPrepend'' a (prependLetter (ofLetter l) w x) | inr bad = exFalso (bad refl)
-parityPrepend'' a (prependLetter (ofInv l) w x) with DecidableSet.eq decA a l
+parityPrepend'' a (prependLetter (ofInv l) w x) with decA a l
 ... | inl a=l = equalityCommutative (notNot (parity a w))
-parityPrepend'' a (prependLetter (ofInv l) w x) | inr a!=l with DecidableSet.eq decA a a
-parityPrepend'' a (prependLetter (ofInv l) w x) | inr a!=l | inl _ with DecidableSet.eq decA a l
+parityPrepend'' a (prependLetter (ofInv l) w x) | inr a!=l with decA a a
+parityPrepend'' a (prependLetter (ofInv l) w x) | inr a!=l | inl _ with decA a l
 ... | inl a=l = exFalso (a!=l a=l)
 ... | inr _ = refl
 parityPrepend'' a (prependLetter (ofInv l) w x) | inr a!=l | inr bad = exFalso (bad refl)
 
 parityPrepend''' : (a : A) (w : ReducedWord) → parity a (prepend w (ofInv a)) ≡ not (parity a w)
-parityPrepend''' a empty with DecidableSet.eq decA a a
+parityPrepend''' a empty with decA a a
 ... | inl _ = refl
 ... | inr bad = exFalso (bad refl)
-parityPrepend''' a (prependLetter (ofLetter l) w x) with DecidableSet.eq decA a l
+parityPrepend''' a (prependLetter (ofLetter l) w x) with decA a l
 ... | inl a=l = equalityCommutative (notNot _)
-parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l with DecidableSet.eq decA a a
-... | inl _ with DecidableSet.eq decA a l
+parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l with decA a a
+... | inl _ with decA a l
 parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l | inl _ | inl a=l = exFalso (a!=l a=l)
 parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l | inl _ | inr _ = refl
 parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l | inr bad = exFalso (bad refl)
-parityPrepend''' a (prependLetter (ofInv l) w x) with DecidableSet.eq decA a a
-parityPrepend''' a (prependLetter (ofInv l) w x) | inl _ with DecidableSet.eq decA a l
+parityPrepend''' a (prependLetter (ofInv l) w x) with decA a a
+parityPrepend''' a (prependLetter (ofInv l) w x) | inl _ with decA a l
 ... | inl a=l = refl
 ... | inr a!=l = refl
 parityPrepend''' a (prependLetter (ofInv l) w x) | inr bad = exFalso (bad refl)
@@ -151,10 +151,10 @@ notXor BoolFalse BoolFalse = refl
 
 parityHomIsHom : (a : A) → (x y : ReducedWord) → parity a (_+W_ x y) ≡ xor (parity a x) (parity a y)
 parityHomIsHom a empty y = refl
-parityHomIsHom a (prependLetter (ofLetter l) x _) y with DecidableSet.eq decA a l
+parityHomIsHom a (prependLetter (ofLetter l) x _) y with decA a l
 parityHomIsHom a (prependLetter (ofLetter .a) x _) y | inl refl = transitivity (parityPrepend'' a (x +W y)) (transitivity (notWellDefined (parityHomIsHom a x y)) (notXor (parity a x) (parity a y)))
 parityHomIsHom a (prependLetter (ofLetter l) x _) y | inr a!=l = transitivity (parityPrepend a (_+W_ x y) l a!=l) (parityHomIsHom a x y)
-parityHomIsHom a (prependLetter (ofInv l) x _) y with DecidableSet.eq decA a l
+parityHomIsHom a (prependLetter (ofInv l) x _) y with decA a l
 parityHomIsHom a (prependLetter (ofInv .a) x _) y | inl refl = transitivity (parityPrepend''' a (x +W y)) (transitivity (notWellDefined (parityHomIsHom a x y)) (notXor (parity a x) (parity a y)))
 parityHomIsHom a (prependLetter (ofInv l) x _) y | inr a!=l = transitivity (parityPrepend' a (x +W y) l a!=l) (parityHomIsHom a x y)
 
diff --git a/Groups/FreeGroup/UniversalProperty.agda b/Groups/FreeGroup/UniversalProperty.agda
index a6c7661..85dd12f 100644
--- a/Groups/FreeGroup/UniversalProperty.agda
+++ b/Groups/FreeGroup/UniversalProperty.agda
@@ -32,7 +32,7 @@ private
     where
       open Setoid S
       open Equivalence eq
-  prepLemma {S = S} G f (prependLetter (ofInv x) w pr) l with DecidableSet.eq decA l x
+  prepLemma {S = S} G f (prependLetter (ofInv x) w pr) l with decA l x
   ... | inl refl = transitive (symmetric identLeft) (transitive (+WellDefined (symmetric invRight) reflexive) (symmetric +Associative))
     where
       open Group G
@@ -48,7 +48,7 @@ private
     where
       open Setoid S
       open Equivalence eq
-  prepLemma' {S = S} G f (prependLetter (ofLetter x) w pr) l with DecidableSet.eq decA l x
+  prepLemma' {S = S} G f (prependLetter (ofLetter x) w pr) l with decA l x
   ... | inl refl = symmetric (transitive +Associative (transitive (+WellDefined invLeft reflexive) identLeft))
     where
       open Group G
diff --git a/Groups/FreeGroup/Word.agda b/Groups/FreeGroup/Word.agda
index 65c853f..6209028 100644
--- a/Groups/FreeGroup/Word.agda
+++ b/Groups/FreeGroup/Word.agda
@@ -45,125 +45,12 @@ prependLetterInjective' refl = refl
 
 badPrepend : {x : A} {w : ReducedWord} {pr : PrependIsValid w (ofInv x)} → (PrependIsValid (prependLetter (ofInv x) w pr) (ofLetter x)) → False
 badPrepend (wordEmpty ())
-badPrepend {x = x} (wordEnding pr bad) with DecidableSet.eq (decidableFreeCompletion decA) (ofLetter x) (ofLetter x)
+badPrepend {x = x} (wordEnding pr bad) with decidableFreeCompletion decA (ofLetter x) (ofLetter x)
 badPrepend {x} (wordEnding pr ()) | inl x₁
 badPrepend {x} (wordEnding pr bad) | inr pr2 = pr2 refl
 
 badPrepend' : {x : A} {w : ReducedWord} {pr : PrependIsValid w (ofLetter x)} → (PrependIsValid (prependLetter (ofLetter x) w pr) (ofInv x)) → False
 badPrepend' (wordEmpty ())
-badPrepend' {x = x} (wordEnding pr x₁) with DecidableSet.eq (decidableFreeCompletion decA) (ofInv x) (ofInv x)
+badPrepend' {x = x} (wordEnding pr x₁) with decidableFreeCompletion decA (ofInv x) (ofInv x)
 badPrepend' {x} (wordEnding pr ()) | inl x₂
 badPrepend' {x} (wordEnding pr x₁) | inr pr2 = pr2 refl
-
-data FreeGroupGenerators : Set a where
-  χ : A → FreeGroupGenerators
-
-freeGroupGenerators : (w : FreeGroupGenerators) → SymmetryGroupElements (reflSetoid (ReducedWord))
-freeGroupGenerators (χ x) = sym {f = f} bij
-  where
-    open DecidableSet decA
-    f : ReducedWord → ReducedWord
-    f empty = prependLetter (ofLetter x) empty (wordEmpty refl)
-    f (prependLetter (ofLetter startLetter) w pr) = prependLetter (ofLetter x) (prependLetter (ofLetter startLetter) w pr) (wordEnding (succIsPositive _) ans)
-      where
-        ans : freeCompletionEqual decA (ofLetter x) (ofInv startLetter) ≡ BoolFalse
-        ans with DecidableSet.eq (decidableFreeCompletion decA) (ofLetter x) (ofInv startLetter)
-        ... | bl = refl
-    f (prependLetter (ofInv startLetter) w pr) with DecidableSet.eq decA startLetter x
-    f (prependLetter (ofInv startLetter) w pr) | inl startLetter=x = w
-    f (prependLetter (ofInv startLetter) w pr) | inr startLetter!=x = prependLetter (ofLetter x) (prependLetter (ofInv startLetter) w pr) (wordEnding (succIsPositive _) ans)
-      where
-        ans : freeCompletionEqual decA (ofLetter x) (ofLetter startLetter) ≡ BoolFalse
-        ans with DecidableSet.eq (decidableFreeCompletion decA) (ofLetter x) (ofInv startLetter)
-        ans | bl with DecidableSet.eq decA x startLetter
-        ans | bl | inl x=sl = exFalso (startLetter!=x (equalityCommutative x=sl))
-        ans | bl | inr x!=sl = refl
-    bij : SetoidBijection (reflSetoid ReducedWord) (reflSetoid ReducedWord) f
-    SetoidInjection.wellDefined (SetoidBijection.inj bij) x=y rewrite x=y = refl
-    SetoidInjection.injective (SetoidBijection.inj bij) {empty} {empty} fx=fy = refl
-    SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofLetter x₁) y pr1} ()
-    SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) y pr1} fx=fy with DecidableSet.eq decA l x
-    SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) empty (wordEmpty x₁)} () | inl l=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) empty (wordEnding () x₁)} fx=fy | inl l=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) (prependLetter (ofLetter x₂) y x₁) (wordEmpty ())} fx=fy | inl l=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) (prependLetter (ofLetter x₂) y x₁) (wordEnding pr bad)} fx=fy | inl refl with ofLetterInjective (prependLetterInjective' fx=fy)
-    ... | l=x2 = exFalso ((freeCompletionEqualFalse' decA bad) (applyEquality ofInv l=x2))
-    SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) (prependLetter (ofInv x₂) y x₁) pr1} () | inl l=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) y pr1} fx=fy | inr l!=x with prependLetterInjective fx=fy
-    SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) y pr1} fx=fy | inr l!=x | ()
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter x) w1 prX} {empty} fx=fy with prependLetterInjective fx=fy
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter x) w1 prX} {empty} fx=fy | ()
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter x) w1 prX} {prependLetter (ofLetter y) w2 prY} fx=fy = prependLetterInjective fx=fy
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) w2 prY} fx=fy with DecidableSet.eq decA y x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) empty prY} () | inl y=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofLetter b) w2 x₁) prY} fx=fy | inl y=x with ofLetterInjective (prependLetterInjective' fx=fy)
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofLetter b) w2 x₁) (wordEmpty ())} fx=fy | inl y=x | x=b
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofLetter b) w2 x₁) (wordEnding pr bad)} fx=fy | inl y=x | x=b rewrite x=b | y=x = exFalso (freeCompletionEqualFalse' decA bad refl)
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofInv b) w2 x₁) prY} fx=fy | inl y=x with prependLetterInjective' fx=fy
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofInv b) w2 x₁) prY} fx=fy | inl y=x | ()
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) w2 prY} fx=fy | inr y!=x with prependLetterInjective fx=fy
-    ... | bl = bl
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {empty} fx=fy with DecidableSet.eq decA a x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) empty prX} {empty} () | inl a=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₂) w1 x₁) prX} {empty} fx=fy | inl a=x with ofLetterInjective (prependLetterInjective' fx=fy)
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₂) w1 x₁) (wordEmpty ())} {empty} fx=fy | inl a=x | x2=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₂) w1 x₁) (wordEnding pr x3)} {empty} fx=fy | inl a=x | x2=x with freeCompletionEqualFalse' decA x3
-    ... | bl = exFalso (bl (applyEquality ofInv (transitivity a=x (equalityCommutative x2=x))))
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofInv x₂) w1 x₁) prX} {empty} () | inl a=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {empty} () | inr a!=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofLetter x₁) y x₂} fx=fy with DecidableSet.eq decA a x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) empty prX} {prependLetter (ofLetter b) y x₂} () | inl a=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₃) w1 x₁) prX} {prependLetter (ofLetter b) y x₂} fx=fy | inl a=x with ofLetterInjective (prependLetterInjective' fx=fy)
-    ... | x3=x rewrite a=x | x3=x = exFalso (badPrepend' prX)
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofInv x₃) w1 x₁) prX} {prependLetter (ofLetter b) y x₂} fx=fy | inl a=x with prependLetterInjective' fx=fy
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofInv x₃) w1 x₁) prX} {prependLetter (ofLetter b) y x₂} fx=fy | inl a=x | ()
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofLetter x₁) y x₂} () | inr a!=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv x₁) y x₂} fx=fy with DecidableSet.eq decA a x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) y x₂} fx=fy | inl a=x with DecidableSet.eq decA b x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) y x₂} fx=fy | inl a=x | inl b=x rewrite fx=fy | a=x | b=x = prependLetterRefl
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) empty prX} {prependLetter (ofInv b) y x₂} () | inl a=x | inr b!=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₃) w1 x₁) prX} {prependLetter (ofInv b) y x₂} fx=fy | inl a=x | inr b!=x with ofLetterInjective (prependLetterInjective' fx=fy)
-    ... | x3=x rewrite a=x | x3=x = exFalso (badPrepend' prX)
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofInv x₃) w1 x₁) prX} {prependLetter (ofInv b) y x₂} () | inl a=x | inr b!=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) y x₂} fx=fy | inr a!=x with DecidableSet.eq decA b x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) empty x₂} () | inr a!=x | inl b=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) (prependLetter (ofLetter x₃) y x₁) x2} fx=fy | inr a!=x | inl b=x with ofLetterInjective (prependLetterInjective' fx=fy)
-    ... | x3=x rewrite (equalityCommutative x3=x) | b=x = exFalso (badPrepend' x2)
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) (prependLetter (ofInv x₃) y x₁) x₂} () | inr a!=x | inl b=x
-    SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) y x₂} fx=fy | inr a!=x | inr b!=x = prependLetterInjective fx=fy
-    SetoidSurjection.wellDefined (SetoidBijection.surj bij) x=y rewrite x=y = refl
-    SetoidSurjection.surjective (SetoidBijection.surj bij) {empty} = prependLetter (ofInv x) empty (wordEmpty refl) , needed
-      where
-        needed : f (prependLetter (ofInv x) empty (wordEmpty refl)) ≡ empty
-        needed with DecidableSet.eq decA x x
-        needed | inl x₁ = refl
-        needed | inr x!=x = exFalso (x!=x refl)
-    SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) empty pr} with DecidableSet.eq decA x l
-    SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter x) empty (wordEmpty refl)} | inl refl = empty , refl
-    SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter x) empty (wordEnding () x₁)} | inl refl
-    SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) empty pr} | inr x!=l = prependLetter (ofInv x) (prependLetter (ofLetter l) empty pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA (λ p → x!=l (ofInvInjective p)))) , needed
-      where
-        needed : f (prependLetter (ofInv x) (prependLetter (ofLetter l) empty pr) (wordEnding (succIsPositive 0) (freeCompletionEqualFalse decA {ofInv x} {ofInv l} λ p → x!=l (ofInvInjective p)))) ≡ prependLetter (ofLetter l) empty pr
-        needed with DecidableSet.eq decA x x
-        ... | inl _ = refl
-        ... | inr bad = exFalso (bad refl)
-    SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) (prependLetter letter w pr2) pr} with DecidableSet.eq decA l x
-    SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) (prependLetter (ofLetter y) w pr2) pr} | inl l=x rewrite l=x = prependLetter (ofLetter y) w pr2 , prependLetterRefl
-    SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) (prependLetter (ofInv y) w pr2) pr} | inl l=x = prependLetter (ofInv y) w pr2 , needed
-      where
-        needed : f (prependLetter (ofInv y) w pr2) ≡ prependLetter (ofLetter l) (prependLetter (ofInv y) w pr2) pr
-        needed with DecidableSet.eq decA y x
-        needed | inl y=x rewrite l=x | y=x = exFalso (badPrepend pr)
-        needed | inr y!=x rewrite l=x = prependLetterRefl
-    SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) (prependLetter letter w pr2) pr} | inr l!=x = prependLetter (ofInv x) (prependLetter (ofLetter l) (prependLetter letter w pr2) pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA λ p → l!=x (ofInvInjective (equalityCommutative p)))) , needed
-      where
-        needed : f (prependLetter (ofInv x) (prependLetter (ofLetter l) (prependLetter letter w pr2) pr) (wordEnding (succIsPositive (succ (wordLength w))) (freeCompletionEqualFalse decA (λ p → l!=x (ofInvInjective (equalityCommutative p)))))) ≡ prependLetter (ofLetter l) (prependLetter letter w pr2) pr
-        needed with DecidableSet.eq decA x x
-        needed | inl x₁ = refl
-        needed | inr x!=x = exFalso (x!=x refl)
-    SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofInv l) w pr} = prependLetter (ofInv x) (prependLetter (ofInv l) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA {ofInv x} {ofLetter l} λ ())) , needed
-      where
-        needed : f (prependLetter (ofInv x) (prependLetter (ofInv l) w pr) (wordEnding (succIsPositive (wordLength w)) (freeCompletionEqualFalse decA {ofInv x} {ofLetter l} λ ()))) ≡ (prependLetter (ofInv l) w pr)
-        needed with DecidableSet.eq decA x x
-        needed | inl x₁ = refl
-        needed | inr x!=x = exFalso (x!=x refl)
diff --git a/Groups/FreeProduct/Lemmas.agda b/Groups/FreeProduct/Lemmas.agda
new file mode 100644
index 0000000..0dcee7e
--- /dev/null
+++ b/Groups/FreeProduct/Lemmas.agda
@@ -0,0 +1,47 @@
+{-# OPTIONS --safe --warning=error #-}
+
+open import Numbers.Naturals.Semiring
+open import Groups.FreeProduct.Definition
+open import Groups.FreeProduct.Setoid
+open import Groups.FreeProduct.Group
+open import Groups.Definition
+open import Groups.Homomorphisms.Definition
+open import Groups.Isomorphisms.Definition
+open import LogicalFormulae
+open import Numbers.Integers.Addition
+open import Numbers.Integers.Definition
+open import Groups.FreeGroup.Definition
+open import Groups.FreeGroup.Word
+open import Groups.FreeGroup.Group
+open import Groups.FreeGroup.UniversalProperty
+open import Setoids.Setoids
+
+module Groups.FreeProduct.Lemmas {i : _} {I : Set i} (decidableIndex : (x y : I) → ((x ≡ y) || ((x ≡ y) → False))) where
+
+private
+  f : ReducedWord decidableIndex → ReducedSequence decidableIndex (λ _ → ℤDecideEquality) (λ _ → ℤGroup)
+  f = universalPropertyFunction decidableIndex (FreeProductGroup decidableIndex (λ _ → ℤDecideEquality) (λ _ → ℤGroup)) λ i → nonempty i (ofEmpty i (nonneg 1) λ ())
+
+  freeProductIso : GroupHom (freeGroup decidableIndex) (FreeProductGroup decidableIndex (λ _ → ℤDecideEquality) (λ _ → ℤGroup)) f
+  freeProductIso = universalPropertyHom decidableIndex (FreeProductGroup decidableIndex (λ _ → ℤDecideEquality) (λ _ → ℤGroup)) (λ i → nonempty i (ofEmpty i (nonneg 1) λ ()))
+
+  freeProductInj : (x y : ReducedWord decidableIndex) → (decidableIndex =RP λ _ → ℤDecideEquality) (λ _ → ℤGroup) (f x) (f y) → x ≡ y
+  freeProductInj empty empty pr = refl
+  freeProductInj empty (prependLetter (ofLetter x₁) y x) pr = exFalso {!!}
+  freeProductInj empty (prependLetter (ofInv x₁) y x) pr = {!!}
+  freeProductInj (prependLetter letter x x₁) y pr = {!!}
+
+freeProductZ : GroupsIsomorphic (freeGroup decidableIndex) (FreeProductGroup decidableIndex (λ _ → ℤDecideEquality) (λ _ → ℤGroup))
+GroupsIsomorphic.isomorphism (freeProductZ) = universalPropertyFunction decidableIndex (FreeProductGroup decidableIndex (λ _ → ℤDecideEquality) (λ _ → ℤGroup)) λ i → nonempty i (ofEmpty i (nonneg 1) λ ())
+GroupIso.groupHom (GroupsIsomorphic.proof (freeProductZ)) = freeProductIso
+SetoidInjection.wellDefined (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) = GroupHom.wellDefined (freeProductIso)
+SetoidInjection.injective (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) {x} {y} = freeProductInj x y
+SetoidSurjection.wellDefined (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) = GroupHom.wellDefined freeProductIso
+SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) {empty} = empty , record {}
+SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) {nonempty i (ofEmpty .i (nonneg zero) nonZero)} = exFalso (nonZero refl)
+SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) {nonempty i (ofEmpty .i (nonneg (succ x)) nonZero)} = prependLetter (ofLetter i) empty (wordEmpty refl) , {!!}
+SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) {nonempty i (ofEmpty .i (negSucc x) nonZero)} = {!!}
+SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) {nonempty i (prependLetter .i g nonZero x x₁)} = {!!}
+
+freeProductNonAbelian : {!!}
+freeProductNonAbelian = {!!}
diff --git a/Setoids/Cardinality/Finite/Definition.agda b/Setoids/Cardinality/Finite/Definition.agda
new file mode 100644
index 0000000..754573e
--- /dev/null
+++ b/Setoids/Cardinality/Finite/Definition.agda
@@ -0,0 +1,16 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Functions
+open import Numbers.Naturals.Definition
+open import Sets.FinSet.Definition
+open import Setoids.Setoids
+
+module Setoids.Cardinality.Finite.Definition where
+
+record FiniteSetoid {a b : _} {A : Set a} (S : Setoid {a} {b} A) : Set (a ⊔ b) where
+  field
+    size : ℕ
+    mapping : FinSet size → A
+    bij : SetoidBijection (reflSetoid (FinSet size)) S mapping
+
diff --git a/Setoids/Cardinality/Infinite/Definition.agda b/Setoids/Cardinality/Infinite/Definition.agda
new file mode 100644
index 0000000..862e8bb
--- /dev/null
+++ b/Setoids/Cardinality/Infinite/Definition.agda
@@ -0,0 +1,18 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import LogicalFormulae
+open import Functions
+open import Numbers.Naturals.Definition
+open import Sets.FinSet.Definition
+open import Setoids.Setoids
+
+module Setoids.Cardinality.Infinite.Definition where
+
+InfiniteSetoid : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Set (a ⊔ b)
+InfiniteSetoid {A = A} S = (n : ℕ) → (f : FinSet n → A) → (SetoidBijection (reflSetoid (FinSet n)) S f) → False
+
+record DedekindInfiniteSetoid {a b : _} {A : Set a} (S : Setoid {a} {b} A) : Set (a ⊔ b) where
+  field
+    inj : ℕ → A
+    isInjection : SetoidInjection (reflSetoid ℕ) S inj
diff --git a/Setoids/Cardinality/Infinite/Lemmas.agda b/Setoids/Cardinality/Infinite/Lemmas.agda
new file mode 100644
index 0000000..1a53202
--- /dev/null
+++ b/Setoids/Cardinality/Infinite/Lemmas.agda
@@ -0,0 +1,29 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import LogicalFormulae
+open import Functions
+open import Numbers.Naturals.Definition
+open import Numbers.Naturals.Order
+open import Sets.FinSet.Definition
+open import Sets.FinSet.Lemmas
+open import Setoids.Setoids
+open import Setoids.Cardinality.Infinite.Definition
+open import Sets.Cardinality.Infinite.Lemmas
+open import Setoids.Subset
+open import Sets.EquivalenceRelations
+
+module Setoids.Cardinality.Infinite.Lemmas where
+
+finsetNotInfiniteSetoid : {n : ℕ} → InfiniteSetoid (reflSetoid (FinSet n)) → False
+finsetNotInfiniteSetoid {n} isInfinite = isInfinite n id (record { inj = record { wellDefined = id ; injective = id } ; surj = record { wellDefined = id ; surjective = λ {x} → x , refl } })
+
+dedekindInfiniteImpliesInfiniteSetoid : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → DedekindInfiniteSetoid S → InfiniteSetoid S
+dedekindInfiniteImpliesInfiniteSetoid S record { inj = inj ; isInjection = isInj } zero f isBij with SetoidInvertible.inverse (setoidBijectiveImpliesInvertible isBij) (inj 0)
+... | ()
+dedekindInfiniteImpliesInfiniteSetoid {A = A} S record { inj = inj ; isInjection = isInj } (succ n) f isBij = noInjectionNToFinite {f = t} tInjective
+  where
+    t : ℕ → FinSet (succ n)
+    t n = SetoidInvertible.inverse (setoidBijectiveImpliesInvertible isBij) (inj n)
+    tInjective : Injection t
+    tInjective pr = SetoidInjection.injective isInj (SetoidInjection.injective (SetoidBijection.inj (setoidInvertibleImpliesBijective (inverseInvertible (setoidBijectiveImpliesInvertible isBij)))) pr)
diff --git a/Setoids/Setoids.agda b/Setoids/Setoids.agda
index 33a35bc..b9c9706 100644
--- a/Setoids/Setoids.agda
+++ b/Setoids/Setoids.agda
@@ -49,6 +49,9 @@ record SetoidInjection {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c}
     wellDefined : {x y : A} → x ∼A y → (f x) ∼B (f y)
     injective : {x y : A} → (f x) ∼B (f y) → x ∼A y
 
+reflSetoidWellDefined : {a b c : _} {A : Set a} (S : Setoid {a} {b} A) (C : Set c) (f : C → A) → {x y : C} → x ≡ y → Setoid._∼_ S (f x) (f y)
+reflSetoidWellDefined S C f refl = Equivalence.reflexive (Setoid.eq S)
+
 record SetoidSurjection {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) : Set (a ⊔ b ⊔ c ⊔ d) where
   open Setoid S renaming (_∼_ to _∼A_)
   open Setoid T renaming (_∼_ to _∼B_)
@@ -119,3 +122,10 @@ SetoidInjection.injective (SetoidBijection.inj (setoidInvertibleImpliesBijective
     open Setoid S
 SetoidSurjection.wellDefined (SetoidBijection.surj (setoidInvertibleImpliesBijective inv)) x~y = SetoidInvertible.fWellDefined inv x~y
 SetoidSurjection.surjective (SetoidBijection.surj (setoidInvertibleImpliesBijective inv)) {x} = SetoidInvertible.inverse inv x , SetoidInvertible.isLeft inv x
+
+inverseInvertible : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {f : A → B} (inv1 : SetoidInvertible S T f) → SetoidInvertible T S (SetoidInvertible.inverse inv1)
+SetoidInvertible.fWellDefined (inverseInvertible record { fWellDefined = fWellDefined ; inverse = inverse ; inverseWellDefined = inverseWellDefined ; isLeft = isLeft ; isRight = isRight }) x=y = inverseWellDefined x=y
+SetoidInvertible.inverse (inverseInvertible {f = f} record { fWellDefined = fWellDefined ; inverse = inverse ; inverseWellDefined = inverseWellDefined ; isLeft = isLeft ; isRight = isRight }) = f
+SetoidInvertible.inverseWellDefined (inverseInvertible record { fWellDefined = fWellDefined ; inverse = inverse ; inverseWellDefined = inverseWellDefined ; isLeft = isLeft ; isRight = isRight }) = fWellDefined
+SetoidInvertible.isLeft (inverseInvertible record { fWellDefined = fWellDefined ; inverse = inverse ; inverseWellDefined = inverseWellDefined ; isLeft = isLeft ; isRight = isRight }) = isRight
+SetoidInvertible.isRight (inverseInvertible record { fWellDefined = fWellDefined ; inverse = inverse ; inverseWellDefined = inverseWellDefined ; isLeft = isLeft ; isRight = isRight }) = isLeft
diff --git a/Sets/Cardinality.agda b/Sets/Cardinality.agda
index e146bb4..5c5624e 100644
--- a/Sets/Cardinality.agda
+++ b/Sets/Cardinality.agda
@@ -1,6 +1,5 @@
 {-# OPTIONS --safe --warning=error --without-K #-}
 
-
 open import LogicalFormulae
 open import Functions
 open import Numbers.Naturals.Semiring
diff --git a/Sets/Cardinality/Infinite/Definition.agda b/Sets/Cardinality/Infinite/Definition.agda
index d9a2890..b1dddde 100644
--- a/Sets/Cardinality/Infinite/Definition.agda
+++ b/Sets/Cardinality/Infinite/Definition.agda
@@ -10,3 +10,7 @@ module Sets.Cardinality.Infinite.Definition where
 InfiniteSet : {a : _} (A : Set a) → Set a
 InfiniteSet A = (n : ℕ) → (f : FinSet n → A) → (Bijection f) → False
 
+record DedekindInfiniteSet {a : _} (A : Set a) : Set a where
+  field
+    inj : ℕ → A
+    isInjection : Injection inj
diff --git a/Sets/Cardinality/Infinite/Lemmas.agda b/Sets/Cardinality/Infinite/Lemmas.agda
index fd4e421..12a799b 100644
--- a/Sets/Cardinality/Infinite/Lemmas.agda
+++ b/Sets/Cardinality/Infinite/Lemmas.agda
@@ -3,10 +3,30 @@
 open import Functions
 open import LogicalFormulae
 open import Numbers.Naturals.Definition
+open import Numbers.Naturals.Order
 open import Sets.Cardinality.Infinite.Definition
 open import Sets.FinSet.Definition
+open import Sets.FinSet.Lemmas
 
 module Sets.Cardinality.Infinite.Lemmas where
 
 finsetNotInfinite : {n : ℕ} → InfiniteSet (FinSet n) → False
 finsetNotInfinite {n} isInfinite = isInfinite n id idIsBijective
+
+noInjectionNToFinite : {n : ℕ} → {f : ℕ → FinSet n} → Injection f → False
+noInjectionNToFinite {n} {f} inj = pigeonhole (le 0 refl) tInj
+  where
+    t : FinSet (succ n) → FinSet n
+    t m = f (toNat m)
+    tInj : Injection t
+    tInj {x} {y} fx=fy = toNatInjective x y (inj fx=fy)
+
+dedekindInfiniteImpliesInfinite : {a : _} (A : Set a) → DedekindInfiniteSet A → InfiniteSet A
+dedekindInfiniteImpliesInfinite A record { inj = inj ; isInjection = isInjection } zero f x with Invertible.inverse (bijectionImpliesInvertible x) (inj 0)
+... | ()
+dedekindInfiniteImpliesInfinite A record { inj = inj ; isInjection = isInj } (succ n) f isBij = noInjectionNToFinite {f = t} tInjective
+  where
+    t : ℕ → FinSet (succ n)
+    t n = Invertible.inverse (bijectionImpliesInvertible isBij) (inj n)
+    tInjective : Injection t
+    tInjective pr = isInj ((Bijection.inj (invertibleImpliesBijection (inverseIsInvertible (bijectionImpliesInvertible isBij)))) pr)