0 | module Control.Category
 1 |
 2 | import Data.Morphisms
 3 |
 4 |
 5 | public export
 6 | interface Category (0 cat : obj -> obj -> Type) | cat where
 7 |   constructor MkCategory
 8 |   id  : cat a a
 9 |   (.) : cat b c -> cat a b -> cat a c
10 |
11 | public export
12 | Category Morphism where
13 |   id                = Mor id
14 |   -- disambiguation needed below, because unification can now get further
15 |   -- here with Category.(.) and it's only interface resolution that fails!
16 |   (Mor f) . (Mor g) = Mor $ Basics.(.) f g
17 |
18 | public export
19 | Monad m => Category (Kleislimorphism m) where
20 |   id                        = Kleisli (pure . id)
21 |   (Kleisli f) . (Kleisli g) = Kleisli $ \a => g a >>= f
22 |
23 | export infixr 1 >>>
24 |
25 | public export
26 | (>>>) : Category cat => cat a b -> cat b c -> cat a c
27 | f >>> g = g . f
28 |