idris-0.9.5.1: lib/Control/Category.idr

module Control.Category

import Prelude.Morphisms

class Category (cat : Set -> Set -> Set) where
  id  : cat a a
  (.) : cat b c -> cat a b -> cat a c

instance Category Morphism where
  id = Homo Builtins.id
  (Homo f) . (Homo g) = Homo $ Builtins.(.) f g

infixr 1 >>>
(>>>) : Category cat => cat a b -> cat b c -> cat a c
f >>> g = g . f