(** * Functoriality of the construction of adjunctions from universal morphisms *)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).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'.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)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' Frefine (_ 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.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