From 70221377d3898778dfe6ad9f43852b5f75ea08b5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 28 Feb 2018 18:55:32 +0100 Subject: [PATCH] Move proof of equivalence to `IsMonad` making them lemmas --- src/Cat/Category/Monad.agda | 97 +++++++++++++------------------------ 1 file changed, 34 insertions(+), 63 deletions(-) diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index aed92c1..a1f9d3b 100644 --- a/src/Cat/Category/Monad.agda +++ b/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 - IsDistributive' = ∀ {X Y Z} {f : Arrow X (R.func* Y)} {g : Arrow Y (R.func* Z)} - → μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f) - ≡ μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) + IsNatural = ∀ {X Y} f → μ Y ∘ R.func→ f ∘ η X ≡ f + IsDistributive = ∀ {X Y Z} (g : Arrow Y (R.func* Z)) (f : Arrow X (R.func* Y)) + → μ 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' {X} {Y} {f} = begin + isNatural : IsNatural + 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' {X} {Y} {Z} {f} {g} = 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) ∎ + isDistributive : IsDistributive + isDistributive {X} {Y} {Z} g f = sym done where - module R² = Functor F[ R ∘ R ] - 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 ∘ R.func→ b ∘ R.func→ c - distrib = {!!} - comm : ∀ {A B C D E} - → {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 = {!!} - lemmm : μ Z ∘ R.func→ (μ Z) ≡ μ Z ∘ μ (R.func* Z) - lemmm = isAssociative - lem4 : μ (R.func* Z) ∘ R².func→ g ≡ R.func→ g ∘ μ Y - lem4 = μNat g + module R² = Functor F[ R ∘ R ] + 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 ∘ R.func→ b ∘ R.func→ c + distrib = {!!} + comm : ∀ {A B C D E} + → {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 = {!!} + lemmm : μ Z ∘ R.func→ (μ Z) ≡ μ Z ∘ μ (R.func* Z) + lemmm = isAssociative + lem4 : μ (R.func* Z) ∘ R².func→ g ≡ R.func→ g ∘ μ Y + 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 - 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 MI = M.IsMonad m module KI = K.IsMonad forthIsMonad : K.IsMonad (forthRaw raw) - KI.isIdentity forthIsMonad = isIdentity - KI.isNatural forthIsMonad = isNatural - KI.isDistributive forthIsMonad = isDistributive + KI.isIdentity forthIsMonad = proj₂ MI.isInverse + KI.isNatural forthIsMonad = MI.isNatural + KI.isDistributive forthIsMonad = MI.isDistributive forth : M.Monad → K.Monad Kleisli.Monad.raw (forth m) = forthRaw (M.Monad.raw m)