🚧 Working on stable algebras, currently showing that K is strong

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
@@ -38,9 +39,32 @@ This file contains some typedefs and records concerning different algebras.
   FreeUniformIterationAlgebra X = FreeObject {C = C} {D = Uniform-Iteration-Algebras} uniformForgetfulF X
 ```
 
--- TODO this is an alternate characterization, prove it with lemma 18 and formalize definition 17
 ## Stable Free Uniform-Iteration Algebras
 
+```agda
+  record IsStableFreeUniformIterationAlgebra {Y : Obj} (freeAlgebra : FreeUniformIterationAlgebra Y) : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
+    open FreeObject freeAlgebra using (η) renaming (FX to FY)
+    open Uniform-Iteration-Algebra FY using (_#)
+
+    field
+        -- TODO awkward notation...
+        [_,_]♯ : ∀ {X : Obj} (A : Uniform-Iteration-Algebra) (f : X × Y ⇒ Uniform-Iteration-Algebra.A A) → X × Uniform-Iteration-Algebra.A FY ⇒ Uniform-Iteration-Algebra.A A
+        ♯-law : ∀ {X : Obj} {A : Uniform-Iteration-Algebra} (f : X × Y ⇒ Uniform-Iteration-Algebra.A A) → f ≈ [ A , f ]♯ ∘ (idC ⁂ η)
+        ♯-preserving : ∀ {X : Obj} {B : Uniform-Iteration-Algebra} (f : X × Y ⇒ Uniform-Iteration-Algebra.A B) {Z : Obj} (h : Z ⇒ Uniform-Iteration-Algebra.A FY + Z) → [ B , f ]♯ ∘ (idC ⁂ h #) ≈ Uniform-Iteration-Algebra._# B (([ B , f ]♯ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))
+        ♯-unique : ∀ {X : Obj} {B : Uniform-Iteration-Algebra} (f : X × Y ⇒ Uniform-Iteration-Algebra.A B) (g : X × Uniform-Iteration-Algebra.A FY ⇒ Uniform-Iteration-Algebra.A B)
+          → f ≈ g ∘ (idC ⁂ η)
+          → (∀ {Z : Obj} (h : Z ⇒ Uniform-Iteration-Algebra.A FY + Z) → g ∘ (idC ⁂ h #) ≈ Uniform-Iteration-Algebra._# B ((g +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)))
+          → g ≈ [ B , f ]♯
+
+  record StableFreeUniformIterationAlgebra : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
+    field
+      Y : Obj
+      freeAlgebra : FreeUniformIterationAlgebra Y
+      isStableFreeUniformIterationAlgebra : IsStableFreeUniformIterationAlgebra freeAlgebra
+    
+    open IsStableFreeUniformIterationAlgebra isStableFreeUniformIterationAlgebra public
+```
+
 ## Free Elgot Algebras
 
 ```agda
@@ -58,6 +82,33 @@ 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 is duplicated from uniform iteration and since free elgots coincide with free uniform iterations this can later be removed.
+```agda
+  record IsStableFreeElgotAlgebra {Y : Obj} (freeElgot : FreeElgotAlgebra Y) : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
+    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 × Y ⇒ Elgot-Algebra.A B) {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → [ B , f ]♯ ∘ (idC ⁂ h #) ≈ Elgot-Algebra._# B (([ B , f ]♯ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))
+        ♯-unique : ∀ {X : Obj} {B : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A B) (g : X × Elgot-Algebra.A FY ⇒ Elgot-Algebra.A B)
+          → f ≈ g ∘ (idC ⁂ η)
+          → (∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → g ∘ (idC ⁂ h #) ≈ Elgot-Algebra._# B ((g +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)))
+          → g ≈ [ B , f ]♯
+
+  record StableFreeElgotAlgebra : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
+    field
+      Y : Obj
+      freeElgot : FreeElgotAlgebra Y
+      isStableFreeElgotAlgebra : IsStableFreeElgotAlgebra freeElgot
+    
+    open IsStableFreeElgotAlgebra isStableFreeElgotAlgebra public
+```
+
 ## Free Elgot to Free Uniform Iteration
 
 ```agda
@@ -74,26 +125,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₁)

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
+```

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

src/Monad/Instance/K.lagda.md

@@ -2,11 +2,16 @@
 ```agda
 open import Level
 open import Categories.FreeObjects.Free
+open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)
+open import Categories.Category
 open import Categories.Functor.Core
 open import Categories.Adjoint
 open import Categories.Adjoint.Properties
 open import Categories.Monad
+open import Categories.Monad.Strong
 open import Category.Instance.AmbientCategory using (Ambient)
+open import Categories.NaturalTransformation
+-- open import Data.Product using (_,_; Σ; Σ-syntax)
 ```
 -->
 
@@ -28,7 +33,8 @@ In this file I explore the monad ***K*** and its properties:
 module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
   open Ambient ambient
   open import Category.Construction.UniformIterationAlgebras ambient
-  open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF)
+  open import Algebra.UniformIterationAlgebra
+  open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
 
   open Equiv
 
@@ -53,3 +59,52 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
     -- EilenbergMoore⇒UniformIterationAlgebras : StrongEquivalence (EilenbergMoore K) (Uniform-Iteration-Algebras D)
     -- EilenbergMoore⇒UniformIterationAlgebras = {!   !}
 ```
+
+### *Proposition 19* If the algebras are stable then K is strong
+
+```agda
+  record MonadKStrong : Set (suc o ⊔ suc ℓ ⊔ suc e) where
+    field
+      algebras : ∀ X → FreeUniformIterationAlgebra X
+      stable : ∀ X → IsStableFreeUniformIterationAlgebra (algebras X)
+    
+    K : Monad C
+    K = MonadK.K (record { algebras = algebras })
+
+    open Monad K using (F)
+    open Functor F using () renaming (F₀ to K₀; F₁ to K₁)
+
+    KStrong : StrongMonad {C = C} monoidal
+    KStrong = record 
+      { M = K 
+      ; strength = record
+        { strengthen = ntHelper (record { η = τ ; commute = λ f → {!   !} }) 
+        ; identityˡ = {!   !}
+        ; η-comm = {!   !}
+        ; μ-η-comm = {!   !}
+        ; strength-assoc = {!   !}
+        }
+      }
+      where
+        open import Agda.Builtin.Sigma
+        open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving)
+
+        module _ (P : Category.Obj (CProduct C C)) where
+          η = λ Z → FreeObject.η (algebras Z)
+          [_,_,_]♯ = λ {A} X Y f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} Y f
+
+
+          X = fst P
+          Y = snd P
+          τ : X × K₀ Y ⇒ K₀ (X × Y)
+          τ = [ Y , FreeObject.FX (algebras (X × Y)) , η (X × Y) ]♯
+
+          τ-η : τ ∘ (idC ⁂ η Y) ≈ η (X × Y)
+          τ-η = sym (♯-law (stable Y) (η (X × Y)))
+
+        [_,_]# : ∀ (A : Uniform-Iteration-Algebra ambient) {X} → (X ⇒ ((Uniform-Iteration-Algebra.A A) + X)) → (X ⇒ Uniform-Iteration-Algebra.A A)
+        [ A , f ]# = Uniform-Iteration-Algebra._# A f
+
+        τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ [ FreeObject.FX (algebras Y) , h ]#) ≈ [ FreeObject.FX (algebras (X × Y)) , (τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ]#
+        τ-comm {X} {Y} {Z} h = ♯-preserving (stable Y) (η (X , Y) (X × Y)) h
+```

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
+```