diff --git a/src/Monad/Instance/K/Commutative.lagda.md b/src/Monad/Instance/K/Commutative.lagda.md
index 751334f..e25940e 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.Compositionality ambient MK
+open import Monad.Instance.K.Elgot ambient MK
 
 open Equiv
 open HomReasoning
diff --git a/src/Monad/Instance/K/Compositionality.lagda.md b/src/Monad/Instance/K/Elgot.lagda.md
similarity index 90%
rename from src/Monad/Instance/K/Compositionality.lagda.md
rename to src/Monad/Instance/K/Elgot.lagda.md
index 3789165..51688a1 100644
--- a/src/Monad/Instance/K/Compositionality.lagda.md
+++ b/src/Monad/Instance/K/Elgot.lagda.md
@@ -1,5 +1,3 @@
-# TODO: every KX satisfies compositionality
-
 ```agda
 {-# OPTIONS --allow-unsolved-metas #-}
 open import Level
@@ -8,8 +6,10 @@ open import Category.Instance.AmbientCategory
 import Monad.Instance.K as MIK
 ```
 
+# Every KX is a free Elgot algebra
+
 ```agda
-module Monad.Instance.K.Compositionality {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
+module Monad.Instance.K.Elgot {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 080f353..4d41509 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.ElgotMonad ambient
 open import Monad.Instance.K ambient
-open import Monad.Instance.K.Compositionality ambient MK
+open import Monad.Instance.K.Elgot ambient MK
 open import Monad.Instance.K.Commutative ambient MK
 open import Monad.Instance.K.Strong ambient MK
 open import Category.Construction.PreElgotMonads ambient
@@ -37,11 +37,6 @@ open M C
 # K is a pre-Elgot monad
 
 ```agda
--- TODO fix global declarations on Commutative.lagda.md
--- open Elgot-Algebra-on using (#-Compositionality)
--- TODO fix this import mess!!!
--- _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
-
 isPreElgot : IsPreElgot monadK
 isPreElgot = record
   { elgotalgebras = λ {X} → elgot X
@@ -52,7 +47,6 @@ isPreElgot = record
 preElgot : PreElgotMonad
 preElgot = record { T = monadK ; isPreElgot = isPreElgot }
 
--- initialPreElgot :
 initialPreElgot : IsInitial PreElgotMonads preElgot
 initialPreElgot = record
   { ! = !′