Move proof of equivalence to IsMonad making them lemmas

src/Cat/Category/Monad.agda

@@ -47,10 +47,10 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     IsInverse = {X : Object}
       → μ X ∘ η (R.func* X) ≡ 𝟙
       × μ X ∘ R.func→ (η X) ≡ 𝟙
-    IsNatural' = ∀ {X Y f} → μ Y ∘ R.func→ f ∘ η X ≡ f
+    IsNatural = ∀ {X Y} f → μ Y ∘ R.func→ f ∘ η X ≡ f
-    IsDistributive' = ∀ {X Y Z} {f : Arrow X (R.func* Y)} {g : Arrow Y (R.func* Z)}
+    IsDistributive = ∀ {X Y Z} (g : Arrow Y (R.func* Z)) (f : Arrow X (R.func* Y))
-      → μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f)
+      → μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f)
-      ≡ μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f)
+      ≡ μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f)
 
   record IsMonad (raw : RawMonad) : Set ℓ where
     open RawMonad raw public
@@ -62,8 +62,8 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       module R = Functor R
       module ℂ = Category ℂ
 
-    isNatural' : IsNatural'
+    isNatural : IsNatural
-    isNatural' {X} {Y} {f} = begin
+    isNatural {X} {Y} f = begin
       μ Y ∘ R.func→ f ∘ η X     ≡⟨ sym ℂ.isAssociative ⟩
       μ Y ∘ (R.func→ f ∘ η X)   ≡⟨ cong (λ φ → μ Y ∘ φ) (sym (ηNat f)) ⟩
       μ Y ∘ (η (R.func* Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩
@@ -71,30 +71,31 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       𝟙 ∘ f                     ≡⟨ proj₂ ℂ.isIdentity ⟩
       f                         ∎
 
-    isDistributive' : IsDistributive'
+    isDistributive : IsDistributive
-    isDistributive' {X} {Y} {Z} {f} {g} = begin
+    isDistributive {X} {Y} {Z} g f = sym done
-      μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f)                     ≡⟨ cong (λ φ → μ Z ∘ φ) distrib ⟩
-      μ Z ∘ (R.func→ (μ Z) ∘ R.func→ (R.func→ g) ∘ R.func→ f) ≡⟨⟩
-      μ Z ∘ (R.func→ (μ Z) ∘ R².func→ g ∘ R.func→ f)          ≡⟨ {!!} ⟩ -- ●-solver?
-      (μ Z ∘ R.func→ (μ Z)) ∘ (R².func→ g ∘ R.func→ f)        ≡⟨ cong (λ φ → φ ∘ (R².func→ g ∘ R.func→ f)) lemmm ⟩
-      (μ Z ∘ μ (R.func* Z)) ∘ (R².func→ g ∘ R.func→ f)        ≡⟨ {!!} ⟩ -- ●-solver?
-      μ Z ∘ μ (R.func* Z) ∘ R².func→ g ∘ R.func→ f            ≡⟨ {!!} ⟩ -- ●-solver + lem4
-      μ Z ∘ R.func→ g ∘ μ Y ∘ R.func→ f                       ≡⟨ sym (Category.isAssociative ℂ) ⟩
-      μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ∎
       where
-        module R² = Functor F[ R ∘ R ]
+      module R² = Functor F[ R ∘ R ]
-        distrib : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B}
+      distrib : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B}
-          → R.func→ (a ∘ b ∘ c)
+        → R.func→ (a ∘ b ∘ c)
-          ≡ R.func→ a ∘ R.func→ b ∘ R.func→ c
+        ≡ R.func→ a ∘ R.func→ b ∘ R.func→ c
-        distrib = {!!}
+      distrib = {!!}
-        comm : ∀ {A B C D E}
+      comm : ∀ {A B C D E}
-          → {a : Arrow D E} {b : Arrow C D} {c : Arrow B C} {d : Arrow A B}
+        → {a : Arrow D E} {b : Arrow C D} {c : Arrow B C} {d : Arrow A B}
-          → a ∘ (b ∘ c ∘ d) ≡ a ∘ b ∘ c ∘ d
+        → a ∘ (b ∘ c ∘ d) ≡ a ∘ b ∘ c ∘ d
-        comm = {!!}
+      comm = {!!}
-        lemmm : μ Z ∘ R.func→ (μ Z) ≡ μ Z ∘ μ (R.func* Z)
+      lemmm : μ Z ∘ R.func→ (μ Z) ≡ μ Z ∘ μ (R.func* Z)
-        lemmm = isAssociative
+      lemmm = isAssociative
-        lem4 : μ (R.func* Z) ∘ R².func→ g ≡ R.func→ g ∘ μ Y
+      lem4 : μ (R.func* Z) ∘ R².func→ g ≡ R.func→ g ∘ μ Y
-        lem4 = μNat g
+      lem4 = μNat g
+      done = begin
+        μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f)                     ≡⟨ cong (λ φ → μ Z ∘ φ) distrib ⟩
+        μ Z ∘ (R.func→ (μ Z) ∘ R.func→ (R.func→ g) ∘ R.func→ f) ≡⟨⟩
+        μ Z ∘ (R.func→ (μ Z) ∘ R².func→ g ∘ R.func→ f)          ≡⟨ {!!} ⟩ -- ●-solver?
+        (μ Z ∘ R.func→ (μ Z)) ∘ (R².func→ g ∘ R.func→ f)        ≡⟨ cong (λ φ → φ ∘ (R².func→ g ∘ R.func→ f)) lemmm ⟩
+        (μ Z ∘ μ (R.func* Z)) ∘ (R².func→ g ∘ R.func→ f)        ≡⟨ {!!} ⟩ -- ●-solver?
+        μ Z ∘ μ (R.func* Z) ∘ R².func→ g ∘ R.func→ f            ≡⟨ {!!} ⟩ -- ●-solver + lem4
+        μ Z ∘ R.func→ g ∘ μ Y ∘ R.func→ f                       ≡⟨ sym (Category.isAssociative ℂ) ⟩
+        μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ∎
 
   record Monad : Set ℓ where
     field
@@ -233,42 +234,12 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       Kraw.bind forthRaw = bind
 
     module _ {raw : M.RawMonad} (m : M.IsMonad raw) where
-      private
+      module MI = M.IsMonad m
-        open M.IsMonad m
-        open K.RawMonad (forthRaw raw)
-        module R = Functor R
-
-        isIdentity : IsIdentity
-        isIdentity {X} = begin
-          bind pure                  ≡⟨⟩
-          bind (η X)                ≡⟨⟩
-          μ X ∘ func→ R (η X)       ≡⟨ proj₂ isInverse ⟩
-          𝟙 ∎
-
-        isNatural : IsNatural
-        isNatural {X} {Y} f = begin
-          bind f ∘ pure             ≡⟨⟩
-          bind f ∘ η X              ≡⟨⟩
-          μ Y ∘ R.func→ f ∘ η X     ≡⟨ isNatural' ⟩
-          f ∎
-          where
-            open NaturalTransformation
-            module ℂ = Category ℂ
-            ηN : Natural ℂ ℂ F.identity R η
-            ηN = proj₂ ηNatTrans
-
-        isDistributive : IsDistributive
-        isDistributive {X} {Y} {Z} g f = begin
-          bind g ∘ bind f                     ≡⟨⟩
-          μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ≡⟨ sym isDistributive' ⟩
-          μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f) ≡⟨⟩
-          μ Z ∘ R.func→ (bind g ∘ f) ∎
-
       module KI = K.IsMonad
       forthIsMonad : K.IsMonad (forthRaw raw)
-      KI.isIdentity     forthIsMonad = isIdentity
+      KI.isIdentity     forthIsMonad = proj₂ MI.isInverse
-      KI.isNatural      forthIsMonad = isNatural
+      KI.isNatural      forthIsMonad = MI.isNatural
-      KI.isDistributive forthIsMonad = isDistributive
+      KI.isDistributive forthIsMonad = MI.isDistributive
 
     forth : M.Monad → K.Monad
     Kleisli.Monad.raw     (forth m) = forthRaw     (M.Monad.raw m)