# Library NaturalTransformation

Require Import Utf8.
Require Import ProofIrrelevance FunctionalExtensionality.
Require Import JMeq.
Require Export Category Functor.
Require Import Common.

Set Implicit Arguments.

Generalizable All Variables.

# NaturalTransformations

Local Open Scope morphism_scope.

Section NaturalTransformation.
Context `(C : @Category objC).
Context `(D : @Category objD).
Variables F G : Functor C D.

Quoting from the lecture notes for 18.705, Commutative Algebra:
A map of functors is known as a natural transformation. Namely, given two functors F : C D, G : C D, a natural transformation T: F G is a collection of maps T A : F A G A, one for each object A of C, such that (T B) (F m) = (G m) (T A) for every map m : A B of C; that is, the following diagram is commutative:
F m F A -------> F B | | | | | T A | T B | | V G m V G A --------> G B
Local Open Scope morphism_scope.

Record NaturalTransformation :=
{
ComponentsOf :> c, D.(Morphism) (F c) (G c);
Commutes : s d (m : C.(Morphism) s d),
(ComponentsOf d) (F.(MorphismOf) m)
= (G.(MorphismOf) m) (ComponentsOf s)
}.
End NaturalTransformation.

Bind Scope natural_transformation_scope with NaturalTransformation.
Delimit Scope natural_transformation_scope with natural_transformation.

Create HintDb natural_transformation discriminated.

Arguments ComponentsOf {objC%type C%category objD%type D%category F%functor G%functor} T%natural_transformation c%object : rename.

Hint Resolve @Commutes : category.
Hint Resolve @Commutes : natural_transformation.

Section NaturalTransformations_Equal.
Lemma NaturalTransformation_Eq objC C objD D F G
: (T U : @NaturalTransformation objC C objD D F G),
( x, T x = U x)
→ T = U.
intros T U H.
assert (ComponentsOf T = ComponentsOf U) by (apply functional_extensionality_dep; assumption).
destruct T, U; simpl in *; repeat subst;
f_equal; apply ProofIrrelevance.proof_irrelevance.
Qed.
End NaturalTransformations_Equal.

Section NaturalTransformationComposition.
Context `(C : @Category objC).
Context `(D : @Category objD).
Context `(E : @Category objE).
Variables F F' F'' : Functor C D.
Variables G G' : Functor D E.

Local Hint Resolve f_equal f_equal2 : natural_transformation.

Definition NTComposeT (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F') :
NaturalTransformation F F''.
(fun c(T' c) (T c));

abstract (
intros;
transitivity ((T' _) ((MorphismOf F' m) (T _)));
try_associativity ltac:(eauto with natural_transformation)
).
Defined.

Local Hint Extern 1 (_ = _) ⇒ apply @FCompositionOf : natural_transformation.

Definition NTComposeF (U : NaturalTransformation G G') (T : NaturalTransformation F F'):
NaturalTransformation (ComposeFunctors G F) (ComposeFunctors G' F').
(fun c(G'.(MorphismOf) (T c)) (U (F c)));
abstract (
simpl; intros; autorewrite with category;
repeat try_associativity ltac:(repeat rewrite <- @Commutes; repeat rewrite <- @FCompositionOf);
reflexivity
).
Defined.
End NaturalTransformationComposition.

Infix "◇" := NTComposeF : natural_transformation_scope.
Infix "○" := NTComposeT : natural_transformation_scope.

Section IdentityNaturalTransformation.
Context `(C : @Category objC).
Context `(D : @Category objD).
Section FullIdentity.
Variable F : Functor C D.

Definition IdentityNaturalTransformation : NaturalTransformation F F.
(fun cIdentity (F c));
abstract (intros; autorewrite with morphism; reflexivity).
Defined.

Lemma LeftIdentityNaturalTransformation (F' : Functor C D) (T : NaturalTransformation F' F) :
NTComposeT IdentityNaturalTransformation T = T.
apply NaturalTransformation_Eq; simpl; auto with morphism.
Qed.

Lemma RightIdentityNaturalTransformation (F' : Functor C D) (T : NaturalTransformation F F') :
NTComposeT T IdentityNaturalTransformation = T.
apply NaturalTransformation_Eq; simpl; auto with morphism.
Qed.
End FullIdentity.

Section ProofFreeIdentity.
Variable FOO : CD.
Variable FMO : s d, Morphism C s dMorphism D (FOO s) (FOO d).

Definition IdentityNaturalTransformation'
FCO FIO FCO' FIO'
(F := Build_Functor C D FOO FMO FCO FIO)
(F' := Build_Functor C D FOO FMO FCO' FIO')
: NaturalTransformation F F'.
refine (Build_NaturalTransformation F F'
(fun cIdentity (FOO c))
_);
subst F F'; simpl in *;
abstract (intros; autorewrite with morphism; reflexivity).
Defined.
End ProofFreeIdentity.
End IdentityNaturalTransformation.

Hint Rewrite @LeftIdentityNaturalTransformation @RightIdentityNaturalTransformation : category.
Hint Rewrite @LeftIdentityNaturalTransformation @RightIdentityNaturalTransformation : natural_transformation.

Section IdentityNaturalTransformationF.
Context `(C : @Category objC).
Context `(D : @Category objD).
Context `(E : @Category objE).
Variable G : Functor D E.
Variable F : Functor C D.

Lemma NTComposeFIdentityNaturalTransformation :
NTComposeF (IdentityNaturalTransformation G) (IdentityNaturalTransformation F) = IdentityNaturalTransformation (ComposeFunctors G F).
Proof.
apply NaturalTransformation_Eq; simpl; intros; repeat rewrite FIdentityOf; auto with morphism.
Qed.
End IdentityNaturalTransformationF.

Hint Rewrite @NTComposeFIdentityNaturalTransformation : category.
Hint Rewrite @NTComposeFIdentityNaturalTransformation : natural_transformation.

Section NTAssociativity.
Context `(B : @Category objB).
Context `(C : @Category objC).
Context `(D : @Category objD).
Context `(E : @Category objE).
Variable F : Functor D E.
Variable G : Functor C D.
Variable H : Functor B C.

Let F0 := ComposeFunctors (ComposeFunctors F G) H.
Let F1 := ComposeFunctors F (ComposeFunctors G H).

Definition ComposeFunctorsAssociator1 : NaturalTransformation F0 F1.
refine (Build_NaturalTransformation F0 F1
(fun _Identity (C := E) _)
_
);
abstract (
simpl; intros;
autorewrite with morphism; reflexivity
).
Defined.

Definition ComposeFunctorsAssociator2 : NaturalTransformation F1 F0.
refine (Build_NaturalTransformation F1 F0
(fun _Identity (C := E) _)
_
);
abstract (
simpl; intros;
autorewrite with morphism; reflexivity
).
Defined.
End NTAssociativity.

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

Local Ltac t :=
repeat match goal with
| [ |- NaturalTransformation ?F ?G ] ⇒
refine (Build_NaturalTransformation F G
(fun _Identity _)
_)
| _abstract (simpl; intros; autorewrite with morphism; reflexivity)
| _split; apply NaturalTransformation_Eq
end.

Section left.
Variable F : Functor D C.

Definition LeftIdentityFunctorNaturalTransformation1 : NaturalTransformation (ComposeFunctors (IdentityFunctor _) F) F. t. Defined.
Definition LeftIdentityFunctorNaturalTransformation2 : NaturalTransformation F (ComposeFunctors (IdentityFunctor _) F). t. Defined.

Theorem LeftIdentityFunctorNT_Isomorphism
: NTComposeT LeftIdentityFunctorNaturalTransformation1 LeftIdentityFunctorNaturalTransformation2 = IdentityNaturalTransformation _
NTComposeT LeftIdentityFunctorNaturalTransformation2 LeftIdentityFunctorNaturalTransformation1 = IdentityNaturalTransformation _.
t.
Qed.
End left.

Section right.
Variable F : Functor C D.

Definition RightIdentityFunctorNaturalTransformation1 : NaturalTransformation (ComposeFunctors F (IdentityFunctor _)) F. t. Defined.
Definition RightIdentityFunctorNaturalTransformation2 : NaturalTransformation F (ComposeFunctors F (IdentityFunctor _)). t. Defined.

Theorem RightIdentityFunctorNT_Isomorphism
: NTComposeT RightIdentityFunctorNaturalTransformation1 RightIdentityFunctorNaturalTransformation2 = IdentityNaturalTransformation _
NTComposeT RightIdentityFunctorNaturalTransformation2 RightIdentityFunctorNaturalTransformation1 = IdentityNaturalTransformation _.
t.
Qed.
End right.
End NTIdentityFunctor.

Section NaturalTransformationExchangeLaw.
Context `(C : @Category objC).
Context `(D : @Category objD).
Context `(E : @Category objE).

Variables F G H : Functor C D.
Variables F' G' H' : Functor D E.

Variable T : NaturalTransformation F G.
Variable U : NaturalTransformation G H.

Variable T' : NaturalTransformation F' G'.
Variable U' : NaturalTransformation G' H'.

Local Ltac t_progress := progress repeat
match goal with
| _apply f_equal
| _apply f_equal2; try reflexivity; []
| _apply Commutes
| _symmetry; apply Commutes
end.

Local Ltac t_exch := repeat
match goal with
| _repeat rewrite FCompositionOf; repeat rewrite Associativity;
t_progress
| _repeat rewrite <- FCompositionOf; repeat rewrite <- Associativity;
t_progress
end.

Theorem NaturalTransformationExchangeLaw :
NTComposeF (NTComposeT U' T') (NTComposeT U T) =
NTComposeT (NTComposeF U' U) (NTComposeF T' T).
Proof.
apply NaturalTransformation_Eq; intro; simpl.
t_exch.
Qed.
End NaturalTransformationExchangeLaw.

Hint Resolve @NaturalTransformationExchangeLaw : category.
Hint Resolve @NaturalTransformationExchangeLaw : natural_transformation.

Ltac nt_solve_associator' :=
repeat match goal with
| _exact (ComposeFunctorsAssociator1 _ _ _)
| _exact (ComposeFunctorsAssociator2 _ _ _)
| [ |- NaturalTransformation (ComposeFunctors ?F _) (ComposeFunctors ?F _) ] ⇒
refine (NTComposeF (IdentityNaturalTransformation F) _)
| [ |- NaturalTransformation (ComposeFunctors _ ?F) (ComposeFunctors _ ?F) ] ⇒
refine (NTComposeF _ (IdentityNaturalTransformation F))
end.
Ltac nt_solve_associator :=
repeat match goal with
| _refine (NTComposeT (ComposeFunctorsAssociator1 _ _ _) _); progress nt_solve_associator'
| _refine (NTComposeT _ (ComposeFunctorsAssociator1 _ _ _)); progress nt_solve_associator'
| _refine (NTComposeT (ComposeFunctorsAssociator2 _ _ _) _); progress nt_solve_associator'
| _refine (NTComposeT _ (ComposeFunctorsAssociator2 _ _ _)); progress nt_solve_associator'
| _progress nt_solve_associator'
end.