Library CT.Instance.Category.FunctorCategory
Require Import CT.Category.
Require Import CT.Functor.
Require Import CT.NaturalTransformation.
Require Import CT.Instance.Functor.
Require Import CT.Instance.NaturalTransformation.Composition.
Require Import CT.Instance.NaturalTransformation.IdentityNaturalTransformation.
Program Definition FunctorCategory (C D : Category) : Category :=
{| ob := Functor C D;
mor := NaturalTransformation;
id := IdentityNaturalTransformation;
comp := @VCNaturalTransformation C D
|}.
Next Obligation.
Proof.
rewrite VCNaturalTransformation_assoc.
reflexivity.
Qed.
Next Obligation.
Proof. symmetry. apply FunctorCategory_obligation_1. Qed.
Next Obligation.
Proof. apply VCNaturalTransformation_id_left. Qed.
Next Obligation.
Proof. apply VCNaturalTransformation_id_right. Qed.
Definition EndofunctorCategory (C : Category) := FunctorCategory C C.
Require Import CT.Functor.
Require Import CT.NaturalTransformation.
Require Import CT.Instance.Functor.
Require Import CT.Instance.NaturalTransformation.Composition.
Require Import CT.Instance.NaturalTransformation.IdentityNaturalTransformation.
Program Definition FunctorCategory (C D : Category) : Category :=
{| ob := Functor C D;
mor := NaturalTransformation;
id := IdentityNaturalTransformation;
comp := @VCNaturalTransformation C D
|}.
Next Obligation.
Proof.
rewrite VCNaturalTransformation_assoc.
reflexivity.
Qed.
Next Obligation.
Proof. symmetry. apply FunctorCategory_obligation_1. Qed.
Next Obligation.
Proof. apply VCNaturalTransformation_id_left. Qed.
Next Obligation.
Proof. apply VCNaturalTransformation_id_right. Qed.
Definition EndofunctorCategory (C : Category) := FunctorCategory C C.