From 317702c0f68679ba07f4751ff3132b2d1da17d85 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Sun, 5 Nov 2023 14:09:54 +0100
Subject: [PATCH] Started showing that K is preelgot

---
 src/Monad/Instance/K/PreElgot.lagda.md | 39 ++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 src/Monad/Instance/K/PreElgot.lagda.md

diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md
new file mode 100644
index 0000000..837066e
--- /dev/null
+++ b/src/Monad/Instance/K/PreElgot.lagda.md
@@ -0,0 +1,39 @@
+<!--
+```agda
+open import Level
+open import Category.Instance.AmbientCategory
+open import Categories.Object.Terminal
+open import Categories.Functor.Algebra
+open import Categories.Object.Initial
+open import Categories.Object.NaturalNumbers.Properties.F-Algebras
+```
+-->
+
+
+
+```agda
+module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) where
+  open Ambient ambient
+  open import Monad.Instance.K ambient
+  open import Monad.Instance.K.Strong ambient
+  open import Monad.Instance.K.Commutative ambient
+  open import Monad.Instance.K.EquationalLifting ambient
+
+  open Terminal terminal using (⊤; !)
+  open Initial using () renaming (! to ¡)
+```
+
+
+First let's define bounded iteration via primitive recursion.
+Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X ⇒ A + X)#⟩ : X × ℕ ⇒ A
+
+```agda
+  p-rec : ∀ {X Y : Obj} → X ⇒ Y → Y × X × N ⇒ Y → X × N ⇒ Y
+  p-rec {X} {Y} f g = π₁ ∘ universal {X = Y × X × N} ⟨ f , ⟨ idC , z ∘ ! ⟩ ⟩ ⟨ g , ⟨ π₁ ∘ π₂ , π₂ ∘ π₂ ⟩ ⟩
+  -- TODO induction, see proposition 2.3 https://ncatlab.org/nlab/show/natural+numbers+object
+
+  [_,_]#⟩ : ∀ {X A : Obj} → (⊤ ⇒ A) → X ⇒ A + X → X × N ⇒ A
+  [_,_]#⟩ {X} {A} !! f = p-rec (!! ∘ !) (([ π₂ , π₁ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ f ∘ π₁))
+  -- TODO might be wrong, check it by testing kleene fixpoint
+  
+```