
  0 | module Data.CT.Functor.Definition
  1 | 
  2 | import Data.CT.Category.Definition
  3 | 
  4 | public export
  5 | record Functor (c, d : Cat) where
  6 |   constructor MkFunctor
  7 |   0 mapObj : c.Obj -> d.Obj
  8 |   0 mapMor : {x, y : c.Obj} -> c.Hom x y -> d.Hom (mapObj x) (mapObj y)
  9 | 
 10 | public export
 11 | composeFunctors : Functor c d -> Functor d e -> Functor c e
 12 | composeFunctors f g = MkFunctor
 13 |   (g.mapObj . f.mapObj)
 14 |   (g.mapMor . f.mapMor)
 15 | 
 16 |