diff --git a/.gitignore b/.gitignore
index d313a11..4d47fdc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,7 +1,7 @@
 *.agdai
 *.pdf
 *.log
-src/Everything.agda
+Everything.agda
 public/
 .direnv
 .DS_Store
diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md
new file mode 100644
index 0000000..45a4f74
--- /dev/null
+++ b/src/Monad/Instance/K/PreElgot.lagda.md
@@ -0,0 +1,32 @@
+<!--
+```agda
+open import Level
+open import Category.Instance.AmbientCategory
+import Monad.Instance.K as MIK
+```
+-->
+
+```agda
+module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
+open Ambient ambient
+open MIK ambient
+open MonadK MK
+open import Monad.ElgotMonad ambient
+open import Monad.Instance.K ambient
+open import Monad.Instance.K.Compositionality ambient MK
+
+open Equiv
+open HomReasoning
+open MR C
+open M C
+```
+
+# K is a pre-Elgot monad
+
+```agda
+preElgot : IsPreElgot monadK
+preElgot = record
+  { elgotalgebras = λ {X} → elgot X
+  ; assoc = {!!}
+  }
+```