PreElgotMonads

src/Category/Construction/PreElgotMonads.lagda.md

@@ -0,0 +1,96 @@
+<!--
+```agda
+open import Level
+open import Category.Instance.AmbientCategory
+open import Categories.NaturalTransformation
+open import Categories.NaturalTransformation.Equivalence
+open import Categories.Monad
+open import Categories.Monad.Relative renaming (Monad to RMonad)
+open import Categories.Functor
+open import Categories.Monad.Construction.Kleisli
+open import Categories.Category.Core
+```
+-->
+
+# The (functor) category of pre-Elgot monads.
+
+```agda
+module Category.Construction.PreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where
+open Ambient ambient
+open import Monad.ElgotMonad ambient
+open HomReasoning
+open Equiv
+open M C
+open MR C
+
+module _ (P S : PreElgotMonad) where
+  private
+    open PreElgotMonad P using () renaming (T to TP)
+    open PreElgotMonad S using () renaming (T to TS)
+    module TP = Monad TP
+    module TS = Monad TS
+    open RMonad (Monad⇒Kleisli C TP) using () renaming (extend to extendP)
+    open RMonad (Monad⇒Kleisli C TS) using () renaming (extend to extendS)
+  record PreElgotMonad-Morphism : Set (o ⊔ ℓ ⊔ e) where
+    field
+      α : NaturalTransformation TP.F TS.F
+    module α = NaturalTransformation α
+    field
+      α-η : ∀ {X}
+        → α.η X ∘ TP.η.η X ≈ TS.η.η X
+      α-μ : ∀ {X}
+        → α.η X ∘ TP.μ.η X ≈ TS.μ.η X ∘ TS.F.₁ (α.η X) ∘ α.η (TP.F.₀ X)
+
+PreElgotMonads : Category {!!} {!!} {!!}
+PreElgotMonads = record
+                   { Obj = PreElgotMonad
+                   ; _⇒_ = PreElgotMonad-Morphism
+                   ; _≈_ = λ f g → (PreElgotMonad-Morphism.α f) ≃ (PreElgotMonad-Morphism.α g)
+                   ; id = id'
+                   ; _∘_ = {!!}
+                   ; assoc = {!!}
+                   ; sym-assoc = {!!}
+                   ; identityˡ = {!!}
+                   ; identityʳ = {!!}
+                   ; identity² = {!!}
+                   ; equiv = {!!}
+                   ; ∘-resp-≈ = {!!}
+                   }
+                   where
+                     id' : ∀ {A : PreElgotMonad} → PreElgotMonad-Morphism A A
+                     id' {A} = record
+                       { α = ntHelper (record
+                         { η = λ _ → idC
+                         ; commute = λ _ → id-comm-sym
+                         })
+                       ; α-η = identityˡ
+                       ; α-μ = sym (begin
+                         T.μ.η _ ∘ T.F.₁ idC ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
+                         T.μ.η _ ∘ T.F.₁ idC ≈⟨ elimʳ T.F.identity ⟩
+                         T.μ.η _ ≈⟨ sym identityˡ ⟩
+                         idC ∘ T.μ.η _ ∎) }
+                       where
+                         open PreElgotMonad A using (T)
+                         module T = Monad T
+                     _∘'_ : ∀ {X Y Z : PreElgotMonad} → PreElgotMonad-Morphism Y Z → PreElgotMonad-Morphism X Y → PreElgotMonad-Morphism X Z
+                     _∘'_ {X} {Y} {Z} f g = record
+                        { α = αf ∘ᵥ αg
+                        ; α-η = λ {A} → begin
+                          (αf.η A ∘ αg.η A) ∘ TX.η.η A ≈⟨ {!!} ⟩
+                          {!!} ≈⟨ {!!} ⟩
+                          {!!} ≈⟨ {!!} ⟩
+                          {!!} ≈⟨ {!!} ⟩
+                          {!!} ≈⟨ {!!} ⟩
+                          {!!} ≈⟨ {!!} ⟩
+                          TZ.η.η A ∎
+                        ; α-μ = {!!}
+                        }
+                        where
+                          module TX = Monad (PreElgotMonad.T X)
+                          module TY = Monad (PreElgotMonad.T Y)
+                          module TZ = Monad (PreElgotMonad.T Z)
+
+                          open PreElgotMonad-Morphism f using () renaming (α to αf)
+                          open PreElgotMonad-Morphism g using () renaming (α to αg)
+
+```