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.