From 67993be27bdb083b06796bf54369f8333e6a9773 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 26 Feb 2018 19:59:11 +0100 Subject: [PATCH] Add reverse function composition to category --- src/Cat/Category.agda | 3 +++ src/Cat/Category/Monad.agda | 8 +------- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index d70fc65..3a275c8 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -86,6 +86,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where codomain : { a b : Object } → Arrow a b → Object codomain {b = b} _ = b + _>>>_ : {A B C : Object} → (Arrow A B) → (Arrow B C) → Arrow A C + f >>> g = g ∘ f + -- | Laws about the data -- TODO: It seems counter-intuitive that the normal-form is on the diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index e59865a..d7d2dc9 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -69,7 +69,7 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where private ℓ = ℓa ⊔ ℓb - open Category ℂ using (Arrow ; 𝟙 ; Object ; _∘_) + open Category ℂ using (Arrow ; 𝟙 ; Object ; _∘_ ; _>>>_) record RawMonad : Set ℓ where field RR : Object → Object @@ -80,12 +80,6 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where fmap f = bind (pure ∘ f) -- Why is (>>=) not implementable? - Because in e.g. the category of sets is -- `m a` a set. This is not necessarily the case. - -- - -- (>>=) : m a -> (a -> m b) -> m b - -- (>=>) : (a -> m b) -> (b -> m c) -> a -> m c - -- Is really like a lifting operation from ∘ (the low level of functions) to >=> (the level of monads) - _>>>_ : {A B C : Object} → (Arrow A B) → (Arrow B C) → Arrow A C - f >>> g = g ∘ f _>=>_ : {A B C : Object} → ℂ [ A , RR B ] → ℂ [ B , RR C ] → ℂ [ A , RR C ] f >=> g = f >>> (bind g) -- _>>=_ : {A B C : Object} {m : RR A} → ℂ [ A , RR B ] → RR C