Idris2Doc : Data.CT.Functor.Definition

Data.CT.Functor.Definition

(source)
Definitions
record Functor : Cat -> Cat -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkFunctor : (mapObj : (c .Obj -> d .Obj)) -> (c .Hom x y -> d .Hom (mapObj x) (mapObj y)) -> Functor c d

  Projections:
  
.mapMor : ({rec:0} : Functor c d) -> c .Hom x y -> d .Hom (mapObj {rec:0} x) (mapObj {rec:0} y)
  
.mapObj : Functor c d -> c .Obj -> d .Obj
.mapObj : Functor c d -> c .Obj -> d .Obj
  Totality: total
  Visibility: public export
mapObj : Functor c d -> c .Obj -> d .Obj
  Totality: total
  Visibility: public export
.mapMor : ({rec:0} : Functor c d) -> c .Hom x y -> d .Hom (mapObj {rec:0} x) (mapObj {rec:0} y)
  Totality: total
  Visibility: public export
mapMor : ({rec:0} : Functor c d) -> c .Hom x y -> d .Hom (mapObj {rec:0} x) (mapObj {rec:0} y)
  Totality: total
  Visibility: public export
composeFunctors : Functor c d -> Functor d e -> Functor c e
  Totality: total
  Visibility: public export