diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md
index 45a4f74..44b20e4 100644
--- a/src/Monad/Instance/K/PreElgot.lagda.md
+++ b/src/Monad/Instance/K/PreElgot.lagda.md
@@ -11,9 +11,12 @@ module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK
 open Ambient ambient
 open MIK ambient
 open MonadK MK
+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.Commutative ambient MK
 
 open Equiv
 open HomReasoning
@@ -24,9 +27,14 @@ open M C
 # K is a pre-Elgot monad
 
 ```agda
+open kleisliK using (extend)
+-- TODO fix global declarations on Commutative.lagda.md
+-- open Elgot-Algebra-on using (#-Compositionality)
+_# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
+
 preElgot : IsPreElgot monadK
 preElgot = record
   { elgotalgebras = λ {X} → elgot X
-  ; assoc = {!!}
+  ; assoc = λ f h → sym (extend-preserve h f)
   }
 ```