Add reverse function composition to category

This commit is contained in:
Frederik Hanghøj Iversen 2018-02-26 19:59:11 +01:00
parent 47882b1110
commit 67993be27b
2 changed files with 4 additions and 7 deletions

View file

@ -86,6 +86,9 @@ record RawCategory (a b : Level) : Set (lsuc (a ⊔ b)) where
codomain : { a b : Object } Arrow a b Object codomain : { a b : Object } Arrow a b Object
codomain {b = b} _ = b 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 -- | Laws about the data
-- TODO: It seems counter-intuitive that the normal-form is on the -- TODO: It seems counter-intuitive that the normal-form is on the

View file

@ -69,7 +69,7 @@ module Kleisli {a b : Level} ( : Category a b) where
private private
= a b = a b
open Category using (Arrow ; 𝟙 ; Object ; _∘_) open Category using (Arrow ; 𝟙 ; Object ; _∘_ ; _>>>_)
record RawMonad : Set where record RawMonad : Set where
field field
RR : Object Object RR : Object Object
@ -80,12 +80,6 @@ module Kleisli {a b : Level} ( : Category a b) where
fmap f = bind (pure f) fmap f = bind (pure f)
-- Why is (>>=) not implementable? - Because in e.g. the category of sets is -- 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 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 ] _>=>_ : {A B C : Object} [ A , RR B ] [ B , RR C ] [ A , RR C ]
f >=> g = f >>> (bind g) f >=> g = f >>> (bind g)
-- _>>=_ : {A B C : Object} {m : RR A} → [ A , RR B ] → RR C -- _>>=_ : {A B C : Object} {m : RR A} → [ A , RR B ] → RR C