minor

.gitignore

@@ -1,7 +1,7 @@
 *.agdai
 *.pdf
 *.log
-src/Everything.agda
+Everything.agda
 public/
 .direnv
 .DS_Store

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 = {!!}
+  }
+```