Formatting

src/Cat/Category/Monad.agda

@@ -24,14 +24,14 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       -- R ~ m
       R : Functor ℂ ℂ
       -- η ~ pure
-      ηNat : NaturalTransformation F.identity R
+      ηNatTrans : NaturalTransformation F.identity R
       -- μ ~ join
-      μNat : NaturalTransformation F[ R ∘ R ] R
+      μNatTrans : NaturalTransformation F[ R ∘ R ] R
 
     η : Transformation F.identity R
-    η = proj₁ ηNat
+    η = proj₁ ηNatTrans
     μ : Transformation F[ R ∘ R ] R
-    μ = proj₁ μNat
+    μ = proj₁ μNatTrans
 
     private
       module R  = Functor R
@@ -122,17 +122,17 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       isIdentity     : IsIdentity
       isNatural      : IsNatural
       isDistributive : IsDistributive
+
+    -- | Map fusion is admissable.
     fusion : Fusion
     fusion {g = g} {f} = begin
       fmap (g ∘ f)               ≡⟨⟩
-      --     f >=> g = >>= g ∘ f
       bind ((f >>> g) >>> pure)  ≡⟨ cong bind isAssociative ⟩
       bind (f >>> (g >>> pure))  ≡⟨ cong (λ φ → bind (f >>> φ)) (sym (isNatural _)) ⟩
       bind (f >>> (pure >>> (bind (g >>> pure)))) ≡⟨⟩
       bind (f >>> (pure >>> fmap g)) ≡⟨⟩
       bind ((fmap g ∘ pure) ∘ f) ≡⟨ cong bind (sym isAssociative) ⟩
-      bind
-      (fmap g ∘ (pure ∘ f)) ≡⟨ sym lem ⟩
+      bind (fmap g ∘ (pure ∘ f)) ≡⟨ sym lem ⟩
       bind (pure ∘ g) ∘ bind (pure ∘ f)   ≡⟨⟩
       fmap g ∘ fmap f           ∎
       where
@@ -155,7 +155,9 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       res : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
       res = {!!}
 
--- Problem 2.3
+-- | The monoidal- and kleisli presentation of monads are equivalent.
+--
+-- This is problem 2.3 in [voe].
 module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
   private
     open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_)
@@ -187,7 +189,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       private
         open M.IsMonad m
         open K.RawMonad (forthRaw raw)
-        module Kis = K.IsMonad
+        module R = Functor R
 
         isIdentity : IsIdentity
         isIdentity {X} = begin
@@ -196,7 +198,6 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
           μ X ∘ func→ R (η X)       ≡⟨ proj₂ isInverse ⟩
           𝟙 ∎
 
-        module R = Functor R
         isNatural : IsNatural
         isNatural {X} {Y} f = begin
           bind f ∘ pure             ≡⟨⟩
@@ -211,7 +212,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
             open NaturalTransformation
             module ℂ = Category ℂ
             ηN : Natural ℂ ℂ F.identity R η
-            ηN = proj₂ ηNat
+            ηN = proj₂ ηNatTrans
 
         isDistributive : IsDistributive
         isDistributive {X} {Y} {Z} g f = begin
@@ -243,16 +244,17 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
                   → {a : Arrow D E} {b : Arrow C D} {c : Arrow B C} {d : Arrow A B}
                   → a ∘ (b ∘ c ∘ d) ≡ a ∘ b ∘ c ∘ d
                 comm = {!!}
-                μN = proj₂ μNat
+                μN = proj₂ μNatTrans
                 lemmm : μ Z ∘ R.func→ (μ Z) ≡ μ Z ∘ μ (R.func* Z)
                 lemmm = isAssociative
                 lem4 : μ (R.func* Z) ∘ RR.func→ g ≡ R.func→ g ∘ μ Y
                 lem4 = μN g
 
+      module KI = K.IsMonad
       forthIsMonad : K.IsMonad (forthRaw raw)
-      Kis.isIdentity forthIsMonad = isIdentity
-      Kis.isNatural forthIsMonad = isNatural
-      Kis.isDistributive forthIsMonad = isDistributive
+      KI.isIdentity     forthIsMonad = isIdentity
+      KI.isNatural      forthIsMonad = isNatural
+      KI.isDistributive forthIsMonad = isDistributive
 
     forth : M.Monad → K.Monad
     Kleisli.Monad.raw     (forth m) = forthRaw     (M.Monad.raw m)
@@ -262,7 +264,6 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       private
         module ℂ = Category ℂ
         open K.Monad m
-        module Mraw = M.RawMonad
         open NaturalTransformation ℂ ℂ
 
         rawR : RawFunctor ℂ ℂ
@@ -274,6 +275,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
           bind (pure ∘ 𝟙) ≡⟨ cong bind (proj₁ ℂ.isIdentity) ⟩
           bind pure       ≡⟨ isIdentity ⟩
           𝟙               ∎
+
         IsFunctor.isDistributive isFunctorR {f = f} {g} = begin
           bind (pure ∘ (g ∘ f))             ≡⟨⟩
           fmap (g ∘ f)                      ≡⟨ fusion ⟩
@@ -284,19 +286,20 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
         Functor.raw       R = rawR
         Functor.isFunctor R = isFunctorR
 
-        R2 : Functor ℂ ℂ
-        R2 = F[ R ∘ R ]
+        R² : Functor ℂ ℂ
+        R² = F[ R ∘ R ]
 
-        ηNat : NaturalTransformation F.identity R
-        ηNat = {!!}
+        ηNatTrans : NaturalTransformation F.identity R
+        ηNatTrans = {!!}
 
-        μNat : NaturalTransformation R2 R
-        μNat = {!!}
+        μNatTrans : NaturalTransformation R² R
+        μNatTrans = {!!}
 
+      module MR = M.RawMonad
       backRaw : M.RawMonad
-      Mraw.R    backRaw = R
-      Mraw.ηNat backRaw = ηNat
-      Mraw.μNat backRaw = μNat
+      MR.R         backRaw = R
+      MR.ηNatTrans backRaw = ηNatTrans
+      MR.μNatTrans backRaw = μNatTrans
 
     module _ (m : K.Monad) where
       open K.Monad m
@@ -327,8 +330,8 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       backRawEq : backRaw (forth m) ≡ M.Monad.raw m
       -- stuck
       M.RawMonad.R         (backRawEq i) = {!!}
-      M.RawMonad.ηNat (backRawEq i) = {!!}
-      M.RawMonad.μNat (backRawEq i) = {!!}
+      M.RawMonad.ηNatTrans (backRawEq i) = {!!}
+      M.RawMonad.μNatTrans (backRawEq i) = {!!}
 
     backeq : (m : M.Monad) → back (forth m) ≡ m
     backeq m = M.Monad≡ (backRawEq m)