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.