From b7cc991d116c91794bb998844493ab714cfd9669 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Mon, 9 Oct 2023 12:11:21 +0200
Subject: [PATCH] =?UTF-8?q?=F0=9F=9A=A7=20prepare=20for=20meeting?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Algebra/Properties.lagda.md               | 52 +++++++++++-------
 src/Monad/Core.lagda.md                       | 20 +++++++
 src/Monad/Instance/Delay/Quotienting.lagda.md |  3 +-
 src/Monad/Morphism.lagda.md                   | 53 +++++++++++++++++++
 4 files changed, 108 insertions(+), 20 deletions(-)
 create mode 100644 src/Monad/Core.lagda.md
 create mode 100644 src/Monad/Morphism.lagda.md

diff --git a/src/Algebra/Properties.lagda.md b/src/Algebra/Properties.lagda.md
index 74d19a1..e536fa9 100644
--- a/src/Algebra/Properties.lagda.md
+++ b/src/Algebra/Properties.lagda.md
@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Category.Instance.AmbientCategory using (Ambient)
 open import Categories.FreeObjects.Free
@@ -58,6 +59,25 @@ This file contains some typedefs and records concerning different algebras.
   FreeElgotAlgebra X = FreeObject {C = C} {D = Elgot-Algebras} elgotForgetfulF X
 ```
 
+## Stable Free Elgot Algebras
+
+**TODO** This can be defined, KY is the free elgot algebra and η is the morphism of the free object!
+```agda
+  record StableFreeElgotAlgebra : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
+    field
+      Y : Obj
+      freeElgot : FreeElgotAlgebra Y
+      -- _♯ : ∀ {A : Elgot-Algebra} 
+    open FreeObject freeElgot using (η) renaming (FX to FY)
+    open Elgot-Algebra FY using (_#)
+    field
+        -- TODO awkward notation...
+        [_,_]♯ : ∀ {X : Obj} (A : Elgot-Algebra) (f : X × Y ⇒ Elgot-Algebra.A A) → X × Elgot-Algebra.A FY ⇒ Elgot-Algebra.A A
+        ♯-law : ∀ {X : Obj} {A : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A A) → f ≈ [ A , f ]♯ ∘ (idC ⁂ η)
+        ♯-preserving : ∀ {X : Obj} {B : Elgot-Algebra} (f : X × Elgot-Algebra.A FY ⇒ Elgot-Algebra.A B) {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → f ∘ (idC ⁂ h #) ≈ Elgot-Algebra._# B ((f +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))
+        -- TODO ♯ is unique iteration preserving
+```
+
 ## Free Elgot to Free Uniform Iteration
 
 ```agda
@@ -74,26 +94,22 @@ This file contains some typedefs and records concerning different algebras.
     ; homomorphism = refl
     ; F-resp-≈ = λ x → x
     }
+```
 
-{-
-TODO / NOTES:
-- Theorem 35 talks about stable free elgot algebras,
-  but it is supposed to show that Ď and K are equivalent (under assumptions).
-  This would require us being able to get FreeUniformIterationAlgebras from FreeElgotAlgebras, but the free _* doesn't type check!
-  It probably is possible to remedy it somehow, one naive way would be to do the proof of Theorem 35 twice, 
-  once for the theorem and a second time to establish the connection between ĎX and KX.
-- TODO talk to Sergey about this
--}
-  FreeElgot⇒FreeUniformIteration : ∀ {X} → FreeElgotAlgebra X → FreeUniformIterationAlgebra X
-  FreeElgot⇒FreeUniformIteration {X} free-elgot = record 
-    { FX = F₀ elgot 
-    ; η = η' 
-    ; _* = λ {Y} f → F₁ (f *') 
+  FreeElgots⇒FreeUniformIterations : (∀ X → FreeElgotAlgebra X) → (∀ X → FreeUniformIterationAlgebra X)
+  FreeElgots⇒FreeUniformIterations free-elgots X = record 
+    { FX = F₀ (FreeObject.FX (free-elgots X))
+    ; η = FreeObject.η (free-elgots X)
+    ; _* = λ {FY} f → F₁ (FreeObject._* (free-elgots X) {A = record { A = Uniform-Iteration-Algebra.A FY ; algebra = record
+      { _# = FY Uniform-Iteration-Algebra.#
+      ; #-Fixpoint = Uniform-Iteration-Algebra.#-Fixpoint FY
+      ; #-Uniformity = Uniform-Iteration-Algebra.#-Uniformity FY
+      ; #-Folding = {!   !}
+      ; #-resp-≈ = Uniform-Iteration-Algebra.#-resp-≈ FY
+      } }} f) -- FreeObject.FX (free-elgots (Uniform-Iteration-Algebra.A FY))
     ; *-lift = {!   !}
     ; *-uniq = {!   !}
     }
     where
-      open FreeObject free-elgot renaming (FX to elgot; η to η'; _* to _*'; *-lift to *-lift'; *-uniq to *-uniq')
-      open Elgot-Algebra elgot
-      open Functor elgot-to-uniformF using (F₀; F₁)
-```
+      open Functor elgot-to-uniformF
+      open Functor (FO⇒Functor elgotForgetfulF free-elgots) using () renaming (F₀ to FO₀; F₁ to FO₁)
diff --git a/src/Monad/Core.lagda.md b/src/Monad/Core.lagda.md
new file mode 100644
index 0000000..726dd5d
--- /dev/null
+++ b/src/Monad/Core.lagda.md
@@ -0,0 +1,20 @@
+<!--
+```agda
+open import Level
+open import Categories.Category.Core
+open import Categories.Functor using (Endofunctor; Functor; _∘F_) renaming (id to idF)
+open import Categories.Monad
+open import Categories.NaturalTransformation
+```
+-->
+
+# Monads
+In this file we define some predicates like 'F extends to a monad'
+
+```agda
+module Monad.Core {o ℓ e} (C : Category o ℓ e) where
+  record ExtendsToMonad (F : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
+    field
+      η : NaturalTransformation idF F
+      μ : NaturalTransformation (F ∘F F) F
+```
\ No newline at end of file
diff --git a/src/Monad/Instance/Delay/Quotienting.lagda.md b/src/Monad/Instance/Delay/Quotienting.lagda.md
index ff4fb81..7d6f6bd 100644
--- a/src/Monad/Instance/Delay/Quotienting.lagda.md
+++ b/src/Monad/Instance/Delay/Quotienting.lagda.md
@@ -135,7 +135,6 @@ We will now show that the following conditions are equivalent:
             out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ∘ idC ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ) ⟩
             out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ≈⟨ ((refl⟩∘⟨ sym-assoc) ○ assoc²'') ⟩
             ▷ ∘ now ∎
--- ⁂ ○
 
       Ď-Functor : Endofunctor C
       Ď-Functor = record
@@ -197,7 +196,7 @@ We will now show that the following conditions are equivalent:
       cond-2 = ∀ X → Σ[ s-alg-on ∈ Search-Algebra-on D (Ď₀ X) ] is-F-Algebra-Morphism {F = D-Functor} (record { A = D₀ X ; α = μ.η X }) (record { A = Ď₀ X ; α = Search-Algebra-on.α s-alg-on }) (ρ {X})
 
       cond-3 : Set (o ⊔ ℓ ⊔ e)
-      cond-3 = {!   !}
+      cond-3 = {!   !} 
 
       cond-4 : Set (o ⊔ ℓ ⊔ e)
       cond-4 = {!   !}
diff --git a/src/Monad/Morphism.lagda.md b/src/Monad/Morphism.lagda.md
new file mode 100644
index 0000000..a5dc6af
--- /dev/null
+++ b/src/Monad/Morphism.lagda.md
@@ -0,0 +1,53 @@
+<!--
+```agda
+open import Level
+open import Categories.Category.Core
+open import Categories.Category.Monoidal
+open import Categories.Monad
+open import Categories.Monad.Morphism using (Monad⇒-id)
+open import Categories.Monad.Strong
+open import Categories.NaturalTransformation using (NaturalTransformation)
+open import Data.Product using (_,_; Σ; Σ-syntax)
+```
+-->
+
+```agda
+module Monad.Morphism {o ℓ e} (C : Category o ℓ e) where
+  open Category C
+```
+
+# Monad morphisms
+This file contains the definition of morphisms between (strong) monads on the same category
+
+## Morphisms between monads
+A morphism between monads is a natural transformation that preserves η and μ, 
+this notion is already formalized in the categories library, 
+but since we are only interested in monads on the same category we rename their definitions.
+
+```agda
+  Monad⇒ = Monad⇒-id
+```
+
+## Morphisms between strong monads
+A morphism between strong monads is a morphism between the underlying monads that also preverses strength.
+
+```agda
+  record IsStrongMonad⇒ {monoidal : Monoidal C} (M N : StrongMonad monoidal) (α : NaturalTransformation (StrongMonad.M.F M) (StrongMonad.M.F N)) : Set (o ⊔ ℓ ⊔ e) where
+    private
+      module M = StrongMonad M
+      module N = StrongMonad N
+      module α = NaturalTransformation α
+    open Monoidal monoidal
+    
+    field
+      η-comm : ∀ {U} → α.η U ∘ M.M.η.η U ≈ N.M.η.η U
+      μ-comm : ∀ {U} → α.η U ∘ (M.M.μ.η U) ≈ N.M.μ.η U ∘ α.η (N.M.F.₀ U) ∘ M.M.F.₁ (α.η U)
+      τ-comm : ∀ {U V} → α.η (U ⊗₀ V) ∘ M.strengthen.η (U , V) ≈ N.strengthen.η (U , V) ∘ (id ⊗₁ α.η V)
+
+  record StrongMonad⇒ {monoidal : Monoidal C} {M N : StrongMonad monoidal} : Set (o ⊔ ℓ ⊔ e) where
+    field
+      α : NaturalTransformation (StrongMonad.M.F M) (StrongMonad.M.F N)
+      isStrongMonad⇒ : IsStrongMonad⇒ M N α
+
+    open IsStrongMonad⇒ isStrongMonad⇒ public
+```