# Library Exercise_4_3_1_10

Require Import Utf8.
Require Import Graph GraphCategory SetCategory NaturalTransformation.
Require Import Common.

Set Implicit Arguments.

Generalizable All Variables.

# Exercise 4.3.1.10

## Problem

Let X and Y be sets, and let f : X Y. There is a functor C_X : Grph Set that sends every graph to the set X and sends every morphism of graphs to the identity morphism id_X : X X. This functor is called the constant functor at X. Similarly there is a constant functor C_Y : Grph Set. Use f to construct a natural transformation C_X C_Y. What are its components?

Section DiagonalFunctor_parts.
Context `(C : @Category objC).
Context `(D : @Category objD).

Definition diagonal_functor_object_of (c : C) : Functor D C.
refine {| ObjectOf := (fun _ c);
MorphismOf := (fun _ _ _ Identity c) |};
abstract (intros; repeat rewrite LeftIdentity; reflexivity).
Defined.

Definition diagonal_functor_morphism_of X Y
(f : C.(Morphism) X Y)
: NaturalTransformation (diagonal_functor_object_of X)
(diagonal_functor_object_of Y).
refine (Build_NaturalTransformation (diagonal_functor_object_of X)
(diagonal_functor_object_of Y)
(fun _f)
_);
abstract (
intros;
simpl;
repeat rewrite LeftIdentity, RightIdentity;
reflexivity
).
Defined.
End DiagonalFunctor_parts.

Variables X Y : CategoryOfTypes.
Variable f : Morphism CategoryOfTypes X Y.
Definition C := diagonal_functor_object_of CategoryOfTypes CategoryOfGraphs.
Definition Exercise_4_3_1_10_NT : NaturalTransformation (C X) (C Y)
:= diagonal_functor_morphism_of CategoryOfTypes
CategoryOfGraphs
X
Y
f.
End Exercise_4_3_1_10.