(** * Functoriality of the construction of adjunctions from universal morphisms *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Functor.Identity Functor.Composition.Core.
Require Import NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws.
Require Import Functor.Dual NaturalTransformation.Dual.
Require Import Adjoint.Core Adjoint.UnitCounit Adjoint.Dual.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Local Open Scope natural_transformation_scope.
Local Open Scope morphism_scope.

Section left.
  (** ** action on morphisms of the construction of a left adjoint to [G] *)
  (** *** functoriality on [C], [D], and [G] *)
  Section also_categories.
    Variables C C' : PreCategory.
    Variable CF : Functor C C'.
    Variables D D' : PreCategory.
    Variable DF : Functor D D'.

    Variable G : Functor D C.
    Variable F : Functor C D.
    Variable A : F -| G.
    Variable G' : Functor D' C'.
    Variable F' : Functor C' D'.
    Variable A' : F' -| G'.
    Variable T : NaturalTransformation (CF o G) (G' o DF).

    Definition left_morphism_of
    : NaturalTransformation (F' o CF) (DF o F).
C, C': PreCategory
CF: Functor C C'
D, D': PreCategory
DF: Functor D D'
G: Functor D C
F: Functor C D
A: F -| G
G': Functor D' C'
F': Functor C' D'
A': F' -| G'
T: NaturalTransformation (CF o G) (G' o DF)
NaturalTransformation (F' o CF) (DF o F)
    Proof.
C, C': PreCategory
CF: Functor C C'
D, D': PreCategory
DF: Functor D D'
G: Functor D C
F: Functor C D
A: F -| G
G': Functor D' C'
F': Functor C' D'
A': F' -| G'
T: NaturalTransformation (CF o G) (G' o DF)
NaturalTransformation (F' o CF) (DF o F)
      refine ((_)
                o (counit A' oR (DF o F))
                o _
                o (F'
                     oL ((T oR F)
                           o _
                           o (CF oL unit A)
                           o _)))%natural_transformation;
      nt_solve_associator.
    Defined.
  End also_categories.

  (** *** functoriality in [G] *)
  Section only_functor.
    Variables C D : PreCategory.

    Variable G : Functor D C.
    Variable F : Functor C D.
    Variable A : F -| G.
    Variable G' : Functor D C.
    Variable F' : Functor C D.
    Variable A' : F' -| G'.
    Variable T : NaturalTransformation G G'.

    Definition left_morphism_of_nondep
    : NaturalTransformation F' F.
C, D: PreCategory
G: Functor D C
F: Functor C D
A: F -| G
G': Functor D C
F': Functor C D
A': F' -| G'
T: NaturalTransformation G G'
NaturalTransformation F' F
    Proof.
C, D: PreCategory
G: Functor D C
F: Functor C D
A: F -| G
G': Functor D C
F': Functor C D
A': F' -| G'
T: NaturalTransformation G G'
NaturalTransformation F' F
      refine (_ o (@left_morphism_of C C 1 D D 1 G F A G' F' A' (_ o T o _)) o _)%natural_transformation;
      nt_solve_associator.
    Defined.
  End only_functor.
End left.

Section right.
  (** ** action on morphisms of the construction of a right adjoint to [F] *)
  Definition right_morphism_of
             C C' CF
             D D' DF
             (F : Functor C D) (G : Functor D C) (A : F -| G)
             (F' : Functor C' D') (G' : Functor D' C') (A' : F' -| G')
             (T : NaturalTransformation (F' o CF) (DF o F))
  : NaturalTransformation (CF o G) (G' o DF)
    := (@left_morphism_of _ _ DF^op _ _ CF^op F^op G^op A^op F'^op G'^op A'^op T^op)^op.

  Definition right_morphism_of_nondep
             C D
             (F : Functor C D) (G : Functor D C) (A : F -| G)
             (F' : Functor C D) (G' : Functor D C) (A' : F' -| G')
             (T : NaturalTransformation F' F)
  : NaturalTransformation G G'
    := (@left_morphism_of_nondep _ _ F^op G^op A^op F'^op G'^op A'^op T^op)^op.
End right.