From 9173468b03739037c158832e3655fd923a5f66dd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 6 Mar 2018 09:56:44 +0100 Subject: [PATCH] Use omap/fmap --- src/Cat/Category/Monad.agda | 21 ++++++++------------- 1 file changed, 8 insertions(+), 13 deletions(-) diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index c47a851..7ad49e8 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -22,9 +22,7 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where open NaturalTransformation ℂ ℂ record RawMonad : Set ℓ where field - -- TODO rename fields here - -- R ~ m - R : EndoFunctor ℂ + R : EndoFunctor ℂ pureNT : NaturalTransformation F.identity R joinNT : NaturalTransformation F[ R ∘ R ] R @@ -40,9 +38,6 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where joinN : Natural F[ R ∘ R ] R joinT joinN = proj₂ joinNT - private - module R = Functor R - Romap = Functor.func* R Rfmap = Functor.func→ R @@ -51,15 +46,15 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where IsAssociative : Set _ IsAssociative = {X : Object} - → joinT X ∘ R.func→ (joinT X) ≡ joinT X ∘ joinT (R.func* X) + → joinT X ∘ Rfmap (joinT X) ≡ joinT X ∘ joinT (Romap X) IsInverse : Set _ IsInverse = {X : Object} - → joinT X ∘ pureT (R.func* X) ≡ 𝟙 - × joinT X ∘ R.func→ (pureT X) ≡ 𝟙 - IsNatural = ∀ {X Y} f → joinT Y ∘ R.func→ f ∘ pureT X ≡ f - IsDistributive = ∀ {X Y Z} (g : Arrow Y (R.func* Z)) (f : Arrow X (R.func* Y)) - → joinT Z ∘ R.func→ g ∘ (joinT Y ∘ R.func→ f) - ≡ joinT Z ∘ R.func→ (joinT Z ∘ R.func→ g ∘ f) + → joinT X ∘ pureT (Romap X) ≡ 𝟙 + × joinT X ∘ Rfmap (pureT X) ≡ 𝟙 + IsNatural = ∀ {X Y} f → joinT Y ∘ Rfmap f ∘ pureT X ≡ f + IsDistributive = ∀ {X Y Z} (g : Arrow Y (Romap Z)) (f : Arrow X (Romap Y)) + → joinT Z ∘ Rfmap g ∘ (joinT Y ∘ Rfmap f) + ≡ joinT Z ∘ Rfmap (joinT Z ∘ Rfmap g ∘ f) record IsMonad (raw : RawMonad) : Set ℓ where open RawMonad raw public