Library FunctorCategory

Require Import Utf8.
Require Import Category Functor NaturalTransformation.

Set Implicit Arguments.

Generalizable All Variables.

Functor Category

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

There is a category Fun(C, D) of functors from C to D.
  Definition FunctorCategory : @Category (Functor C D).
    refine (@Build_Category _
                            (NaturalTransformation (C := C) (D := D))
                            (IdentityNaturalTransformation (C := C) (D := D))
                            (NTComposeT (C := C) (D := D))
    abstract (intros; apply NaturalTransformation_Eq; simpl; auto with morphism).
End FunctorCategory.

Notation "C ^ D" := (FunctorCategory D C) : category_scope.