Data.CT.Functor.Definition

Definitions

record Functor : Cat -> Cat -> Type

Totality: total
Visibility: public export
Constructor: 

MkFunctor : (0 mapObj : (c .Obj -> d .Obj)) -> (0 _ : (c .Hom x y -> d .Hom (mapObj x) (mapObj y))) -> Functor c d

Projections:

0 .mapMor : ({rec:0} : Functor c d) -> c .Hom x y -> d .Hom (mapObj {rec:0} x) (mapObj {rec:0} y)

0 .mapObj : Functor c d -> c .Obj -> d .Obj

0 .mapObj : Functor c d -> c .Obj -> d .Obj

Visibility: public export

0 mapObj : Functor c d -> c .Obj -> d .Obj

Visibility: public export

0 .mapMor : ({rec:0} : Functor c d) -> c .Hom x y -> d .Hom (mapObj {rec:0} x) (mapObj {rec:0} y)

Visibility: public export

0 mapMor : ({rec:0} : Functor c d) -> c .Hom x y -> d .Hom (mapObj {rec:0} x) (mapObj {rec:0} y)

Visibility: public export

composeFunctors : Functor c d -> Functor d e -> Functor c e

Visibility: public export