DiagonalFunctor.DiagonalFunctor

Let J and C be two categories, we consider the functor category C^J. The diagonal functor D : C -> C^J maps each object x of C to the constant diagram D_x from J to C. It maps each morphism to the natural transformation between the two constant diagrams associated to the source and the target of the morphism.

Documentation

mkDiagonalFunctor

Arguments

:: (FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq o2)

=> c1

J

-> c2

C

-> Diagram c2 m2 o2 (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)

D : C -> C^J

Given two categories J and C, returns the diagonal functor C -> C^J.