From 0e89d524609da90195678640380c917fd3c0aad8 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Wed, 15 Nov 2023 14:37:28 +0100
Subject: [PATCH] minor

---
 src/Monad/Instance/K/PreElgot.lagda.md | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md
index 44b20e4..0aee30b 100644
--- a/src/Monad/Instance/K/PreElgot.lagda.md
+++ b/src/Monad/Instance/K/PreElgot.lagda.md
@@ -17,6 +17,7 @@ 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 import Categories.FreeObjects.Free
 
 open Equiv
 open HomReasoning
@@ -32,9 +33,14 @@ open kleisliK using (extend)
 -- open Elgot-Algebra-on using (#-Compositionality)
 _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
 
-preElgot : IsPreElgot monadK
-preElgot = record
+isPreElgot : IsPreElgot monadK
+isPreElgot = record
   { elgotalgebras = λ {X} → elgot X
   ; assoc = λ f h → sym (extend-preserve h f)
   }
+
+preElgot : PreElgotMonad
+preElgot = record { T = monadK ; isPreElgot = isPreElgot }
+
+-- initialPreElgot :
 ```