diff --git a/src/Monad/Instance/K/Commutative.lagda.md b/src/Monad/Instance/K/Commutative.lagda.md
index e25940e..8160325 100644
--- a/src/Monad/Instance/K/Commutative.lagda.md
+++ b/src/Monad/Instance/K/Commutative.lagda.md
@@ -22,7 +22,7 @@ open import Category.Construction.UniformIterationAlgebras ambient
 open import Algebra.UniformIterationAlgebra ambient
 open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
 open import Algebra.ElgotAlgebra ambient
-open import Monad.Instance.K.Elgot ambient MK
+open import Monad.Instance.K.ElgotAlgebra ambient MK
 
 open Equiv
 open HomReasoning
diff --git a/src/Monad/Instance/K/Elgot.lagda.md b/src/Monad/Instance/K/ElgotAlgebra.lagda.md
similarity index 93%
rename from src/Monad/Instance/K/Elgot.lagda.md
rename to src/Monad/Instance/K/ElgotAlgebra.lagda.md
index 51688a1..2d4c4fc 100644
--- a/src/Monad/Instance/K/Elgot.lagda.md
+++ b/src/Monad/Instance/K/ElgotAlgebra.lagda.md
@@ -9,7 +9,7 @@ import Monad.Instance.K as MIK
 # Every KX is a free Elgot algebra
 
 ```agda
-module Monad.Instance.K.Elgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
+module Monad.Instance.K.ElgotAlgebra {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
   open Ambient ambient
   open MIK ambient
   open MonadK MK
diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md
index dcb3eac..7b603e2 100644
--- a/src/Monad/Instance/K/PreElgot.lagda.md
+++ b/src/Monad/Instance/K/PreElgot.lagda.md
@@ -22,7 +22,7 @@ open import Algebra.ElgotAlgebra ambient
 open import Algebra.UniformIterationAlgebra ambient
 open import Monad.PreElgot ambient
 open import Monad.Instance.K ambient
-open import Monad.Instance.K.Elgot ambient MK
+open import Monad.Instance.K.ElgotAlgebra ambient MK
 open import Monad.Instance.K.Commutative ambient MK
 open import Monad.Instance.K.Strong ambient MK
 open import Category.Construction.PreElgotMonads ambient
@@ -34,7 +34,7 @@ open MR C
 open M C
 ```
 
-# K is a pre-Elgot monad
+# K is the initial (strong) pre-Elgot monad
 
 ```agda
 isPreElgot : IsPreElgot monadK
diff --git a/src/index.lagda.md b/src/index.lagda.md
index 641df6e..aa53dbd 100644
--- a/src/index.lagda.md
+++ b/src/index.lagda.md
@@ -70,7 +70,7 @@ open import Monad.Instance.K.Strong
 The next step is to show that every *KX* satisfies compositionality, meaning that each *KX* is an Elgot algebra.
 
 ```agda
-open import Monad.Instance.K.Compositionality
+open import Monad.Instance.K.ElgotAlgebra
 ```
 
 and with this we can show that K is and equational lifting monad, i.e. a commutative monad satisfying the equational lifting law:
@@ -80,9 +80,9 @@ open import Monad.Instance.K.Commutative
 open import Monad.Instance.K.EquationalLifting
 ```
 
-and lastly we formalize the notion of *pre-Elgot monad* and show that **K** is pre-Elgot.
+and lastly we formalize the notion of *pre-Elgot monad* and show that **K** is the initial pre-Elgot monad.
 
 ```agda
-open import Monad.ElgotMonad
--- open import Monad.Instance.K.PreElgot TODO
+open import Monad.PreElgot
+open import Monad.Instance.K.PreElgot
 ```
\ No newline at end of file