diff --git a/.i18n/Game.pot b/.i18n/Game.pot
index 65ffdb8..3a10516 100644
--- a/.i18n/Game.pot
+++ b/.i18n/Game.pot
@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.6.1\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: Sun Mar 31 15:57:31 2024\n"
+"POT-Creation-Date: Sun Mar 31 16:07:10 2024\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: de\n"
diff --git a/Game/Levels/Quotient/Bijection.lean b/Game/Levels/Quotient/Bijection.lean
index 69506d5..b2b9323 100644
--- a/Game/Levels/Quotient/Bijection.lean
+++ b/Game/Levels/Quotient/Bijection.lean
@@ -4,12 +4,20 @@ import Game.Metadata.StructInstWithHoles
 import Game.Levels.Quotient.Respect
 
 World "Quotient"
-Level 4
+Level 5
 
 Title "Quotient"
 
 Introduction
 "
+The crucial universal property of `Quotient r` is the following statement:
+If `f : A → B` is any function that respects the congruence `r` in the sense that
+for every `x y : A`, `r x y` implies `f x = f y`, then `f` uniquely lifts to a function `Quotient.lift f : Quotient r → B`
+defined on a typical element `⟦a⟧` by
+```
+Quotient.lift f ⟦a⟧ = f a
+```
+
 In this level you prove that the quotient lift of `rangeFactorization f` with respect to the
 congruence relation `ker f` is a bijection.
 
diff --git a/Game/Levels/Quotient/Equifibred.lean b/Game/Levels/Quotient/Equifibred.lean
new file mode 100644
index 0000000..8efae51
--- /dev/null
+++ b/Game/Levels/Quotient/Equifibred.lean
@@ -0,0 +1,36 @@
+import Game.Metadata
+import Game.Metadata.StructInstWithHoles
+
+World "Quotient"
+Level 2
+
+Title "Quotient"
+
+Introduction
+"
+Given a setoid structure `s` on `A` and an element `a : A` the equivalence class of `a`
+is the set of all elements of `A` that are congruent to `a`, namely `{x : A | s.Rel x a}`.
+
+We say a function `f : A → B` is equifibred if for any two elements `x` and `y` of `B` the preimages of `x` and `y` are equivlanet.
+
+In this level you show that the equivalence classes of an equifibred function are all equivalent.
+
+"
+
+open Function Set Setoid
+
+section
+-- The following lemma is useful: it says that the elements related to x ∈ α by the kernel of f are those in the preimage of f(x) under f.
+#check ker_iff_mem_preimage
+end
+
+
+Statement equiv_classes_of_equifibred (f : A → B)
+    (e : ∀ b b'  : B, (f ⁻¹' {b}) ≃ (f ⁻¹' {b'})) :
+    ∀ u v, u ∈ (ker f).classes → v ∈ (ker f).classes → u ≃ v := by
+  intro u v hu hv
+  refine {?..!}
+  · sorry
+  · sorry
+  · sorry
+  · sorry
diff --git a/Game/Levels/Quotient/Factorization.lean b/Game/Levels/Quotient/Factorization.lean
index cafd4db..ef838a2 100644
--- a/Game/Levels/Quotient/Factorization.lean
+++ b/Game/Levels/Quotient/Factorization.lean
@@ -6,7 +6,7 @@ import Game.Levels.Quotient.Respect
 import Game.Levels.Quotient.Bijection
 
 World "Quotient"
-Level 5
+Level 6
 
 Title "Quotient"
 
diff --git a/Game/Levels/Quotient/Kernel.lean b/Game/Levels/Quotient/Kernel.lean
index 654b161..7910985 100644
--- a/Game/Levels/Quotient/Kernel.lean
+++ b/Game/Levels/Quotient/Kernel.lean
@@ -12,13 +12,16 @@ Introduction
 A setoid structure on a type `A` provides a relation `r : A → A → Prop` which is congruence (aka equivalence relation). The congruence `r` tell us which elements of `A` are congruent to other elements of `A`.
 
 
-We show that every function `f : A → B` induces a congruence on `A`: We say elements `x` and `y` of `A` are in the same fibre of `f` if `f x = f y`.
+We show that every function `f : A → B` induces a congruence on `A`. We say elements `x`
+and `y` of `A` are kernel-congruent if `f x = f y`.
+This is the equivalence relation `ker f` on `A` denoted by `ker f`.
 ```
-x ~ y ↔ f x = f y
+x ≈ y ↔ f x = f y
 ```
-This is a congruence on `A` denoted by `ker f`.
 
-You might be familiar with the kernel of a group homomorphism. The kernel of a group homomorphism is the set of elements that are sent to the identity element of the codomain. The kernel of a group homomorphism is a subgroup of the domain.
+You might be familiar with the kernel of a group homomorphism which the set of elements
+that are sent to the identity element of the codomain. The kernel of a group
+homomorphism is a subgroup of the domain.
 
 In this level you show that these two notions of kernel coincide: Two elements `x` and `y` of `A` are kernel congruent if and only if their difference is in the kernel of `f`.
 
@@ -44,10 +47,10 @@ Statement {A B : Type*} [AddGroup A]  [AddGroup B] {f : A →+ B} {x y : A} :
     exact h
 
 
--- alternate proof using more from mathlib
-example {A B : Type*} [AddGroup A]  [AddGroup B] {f : A →+ B} {x y : A} :
-    (ker f).Rel x y ↔ (x - y) ∈ f.ker := by
-  simp_rw [AddMonoidHom.mem_ker f]
-  simp only [map_sub]
-  simp [ker_def]
-  simp [sub_eq_zero]
+-- alternate proof using `AddMonoidHom.mem_ker` from mathlib
+-- example {A B : Type*} [AddGroup A]  [AddGroup B] {f : A →+ B} {x y : A} :
+--     (ker f).Rel x y ↔ (x - y) ∈ f.ker := by
+--   simp_rw [AddMonoidHom.mem_ker f]
+--   simp only [map_sub]
+--   simp [ker_def]
+--   simp [sub_eq_zero]
diff --git a/Game/Levels/Quotient/Respect.lean b/Game/Levels/Quotient/Respect.lean
index e142366..b409408 100644
--- a/Game/Levels/Quotient/Respect.lean
+++ b/Game/Levels/Quotient/Respect.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.Metadata.StructInstWithHoles
 
 World "Quotient"
-Level 3
+Level 4
 
 Title "Quotient"
 
diff --git a/Game/Levels/Quotient/Surjection.lean b/Game/Levels/Quotient/Surjection.lean
index 73c1d9e..a0c5172 100644
--- a/Game/Levels/Quotient/Surjection.lean
+++ b/Game/Levels/Quotient/Surjection.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.Metadata.StructInstWithHoles
 
 World "Quotient"
-Level 2
+Level 3
 
 Title "Quotient"
 
@@ -10,18 +10,13 @@ Introduction
 "
 For a congruence `r` on a type `A`, the quotient type `Quotient r` is the type of
 elements of `A` modulo `r`.  A mathematically common notation for `Quotient r` is `A / r`.
-We can think of `Quotient r` as the collection of equivalence classes `⟦a⟧` of elements `a : A` modulo `r`.
-The function `Quotient.mk : A → Quotient r` maps an element `a : A` to its equivalence class `⟦a⟧`.
+
+There is a function `Quotient.mk : A → Quotient r` which maps an element `a : A` to  `⟦a⟧`, a typical element of `Quotient r`.
+
 If elements `a b : A` are congruent, then `⟦a⟧ = ⟦b⟧`. This fact is witnessed
 by `Quotient.sound`.
 
-The simplest induction principle `Quotient.ind` for the quotient type states that a property of elements of `Quotient r` can be proved by showing that it holds for all congruence classes `⟦a⟧`. In other words, if a property `P` holds for all congruence classes `⟦a⟧`, then `P` holds for all elements of `Quotient r`.
-
-The crucial universal property of `Quotient r` is the following statement:
-If `f : A → B` is any function that
-respects the congruence `r` in the sense that for every `x y : A`,
-`r x y` implies `f x = f y`, then `f` uniquely lifts to a function `Quotient.lift f : Quotient r → B`
-defined on each equivalence class `⟦a⟧` by `Quotient.lift f ⟦a⟧ = f a`.
+The simplest induction principle `Quotient.ind` for the quotient type states that we can prove a property of elements of `Quotient r` if we can prove that it holds for all typical elements `⟦a⟧`.
 
 In this level you show that the function `Quotient.mk : A → Quotient fiber_setoid` is surjective.