(** * Adjunctions as 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 Functor.Dual Category.Dual.
Require Import Adjoint.Core Adjoint.UnitCounit Adjoint.UnitCounitCoercions Adjoint.Dual.
Require Comma.Core.
Local Set Warnings Append "-notation-overridden". (* work around bug #5567, https://coq.inria.fr/bugs/show_bug.cgi?id=5567, notation-overridden,parsing should not trigger for only printing notations *)
Import Comma.Core.
Local Set Warnings Append "notation-overridden".
Require Import UniversalProperties Comma.Dual InitialTerminalCategory.Core InitialTerminalCategory.Functors.

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

Local Open Scope morphism_scope.

Section adjunction_universal.
  (** ** [F ⊣ G] gives an initial object of [(Y / G)] for all [Y : C] *)
  Section initial.
    Variables C D : PreCategory.
    Variable F : Functor C D.
    Variable G : Functor D C.
    Variable A : F -| G.
    Variable Y : C.

    Definition initial_morphism__of__adjunction
    : object (Y / G)
      := @CommaCategory.Build_object
           _ D C
           (! Y) G
           (center _)
           (F Y)
           ((unit A) Y).

    Definition is_initial_morphism__of__adjunction
    : IsInitialMorphism initial_morphism__of__adjunction
      := Build_IsInitialMorphism
           _
           _
           _
           _
           ((A : AdjunctionUnit _ _).2 _).
  End initial.

  Global Arguments initial_morphism__of__adjunction [C D F G] A Y.
  Global Arguments is_initial_morphism__of__adjunction [C D F G] A Y _.

  (** ** [F ⊣ G] gives a terminal object of [(F / X)] for all [X : D] *)
  Section terminal.
    Variables C D : PreCategory.
    Variable F : Functor C D.
    Variable G : Functor D C.
    Variable A : F -| G.
    Variable X : D.

    Definition terminal_morphism__of__adjunction
    : object (F / X)
      := Eval simpl in
          dual_functor
            (! X)^op F^op
            (initial_morphism__of__adjunction A^op X).

    Definition is_terminal_morphism__of__adjunction
    : IsTerminalMorphism terminal_morphism__of__adjunction
      := is_initial_morphism__of__adjunction A^op X.
  End terminal.

  Global Arguments terminal_morphism__of__adjunction [C D F G] A X.
  Global Arguments is_terminal_morphism__of__adjunction [C D F G] A X _.
End adjunction_universal.

Section adjunction_from_universal.
  (** ** an initial object of [(Y / G)] for all [Y : C] gives a left adjoint to [G] *)
  Section initial.
    Variables C D : PreCategory.

    Variable G : Functor D C.
    Context `(HM : forall Y, @IsInitialMorphism _ _ Y G (M Y)).

    Local Notation obj_of Y :=
      (IsInitialMorphism_object (@HM Y))
        (only parsing).

    Local Notation mor_of Y0 Y1 f :=
      (let etaY1 := IsInitialMorphism_morphism (@HM Y1) in
       IsInitialMorphism_property_morphism (@HM Y0) _ (etaY1 o f))
        (only parsing).

    Lemma identity_of Y : mor_of Y Y 1 = 1.
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
Y: C
(let etaY1 := IsInitialMorphism_morphism (HM (Y:=Y))
   in
 IsInitialMorphism_property_morphism (HM (Y:=Y))
   (IsInitialMorphism_object (HM (Y:=Y))) (etaY1 o 1)) =
1
    Proof.
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
Y: C
(let etaY1 := IsInitialMorphism_morphism (HM (Y:=Y))
   in
 IsInitialMorphism_property_morphism (HM (Y:=Y))
   (IsInitialMorphism_object (HM (Y:=Y))) (etaY1 o 1)) =
1
      simpl.
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
Y: C
IsInitialMorphism_property_morphism (HM (Y:=Y))
  (IsInitialMorphism_object (HM (Y:=Y)))
  (IsInitialMorphism_morphism (HM (Y:=Y)) o 1) = 1
      erewrite IsInitialMorphism_property_morphism_unique; [ reflexivity | ].
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
Y: C
G _1 1 o IsInitialMorphism_morphism (HM (Y:=Y)) =
IsInitialMorphism_morphism (HM (Y:=Y)) o 1
      rewrite ?identity_of, ?left_identity, ?right_identity.
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
Y: C
IsInitialMorphism_morphism (HM (Y:=Y)) =
IsInitialMorphism_morphism (HM (Y:=Y))
      reflexivity.
    Qed.

    Lemma composition_of x y z g f
    : mor_of _ _ (f o g) = mor_of y z f o mor_of x y g.
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
x, y, z: C
g: morphism C x y
f: morphism C y z
(let etaY1 := IsInitialMorphism_morphism (HM (Y:=z))
   in
 IsInitialMorphism_property_morphism (HM (Y:=x))
   (IsInitialMorphism_object (HM (Y:=z)))
   (etaY1 o (f o g))) =
(let etaY1 := IsInitialMorphism_morphism (HM (Y:=z))
   in
 IsInitialMorphism_property_morphism (HM (Y:=y))
   (IsInitialMorphism_object (HM (Y:=z))) (etaY1 o f))
o (let etaY1 := IsInitialMorphism_morphism (HM (Y:=y))
     in
   IsInitialMorphism_property_morphism (HM (Y:=x))
     (IsInitialMorphism_object (HM (Y:=y)))
     (etaY1 o g))
    Proof.
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
x, y, z: C
g: morphism C x y
f: morphism C y z
(let etaY1 := IsInitialMorphism_morphism (HM (Y:=z))
   in
 IsInitialMorphism_property_morphism (HM (Y:=x))
   (IsInitialMorphism_object (HM (Y:=z)))
   (etaY1 o (f o g))) =
(let etaY1 := IsInitialMorphism_morphism (HM (Y:=z))
   in
 IsInitialMorphism_property_morphism (HM (Y:=y))
   (IsInitialMorphism_object (HM (Y:=z))) (etaY1 o f))
o (let etaY1 := IsInitialMorphism_morphism (HM (Y:=y))
     in
   IsInitialMorphism_property_morphism (HM (Y:=x))
     (IsInitialMorphism_object (HM (Y:=y)))
     (etaY1 o g))
      simpl.
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
x, y, z: C
g: morphism C x y
f: morphism C y z
IsInitialMorphism_property_morphism (HM (Y:=x))
  (IsInitialMorphism_object (HM (Y:=z)))
  (IsInitialMorphism_morphism (HM (Y:=z)) o (f o g)) =
IsInitialMorphism_property_morphism (HM (Y:=y))
  (IsInitialMorphism_object (HM (Y:=z)))
  (IsInitialMorphism_morphism (HM (Y:=z)) o f)
o IsInitialMorphism_property_morphism (HM (Y:=x))
    (IsInitialMorphism_object (HM (Y:=y)))
    (IsInitialMorphism_morphism (HM (Y:=y)) o g)
      erewrite IsInitialMorphism_property_morphism_unique; [ reflexivity | ].
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
x, y, z: C
g: morphism C x y
f: morphism C y z
G
_1 (IsInitialMorphism_property_morphism (HM (Y:=y))
      (IsInitialMorphism_object (HM (Y:=z)))
      (IsInitialMorphism_morphism (HM (Y:=z)) o f)
    o IsInitialMorphism_property_morphism (HM (Y:=x))
        (IsInitialMorphism_object (HM (Y:=y)))
        (IsInitialMorphism_morphism (HM (Y:=y)) o g))
o IsInitialMorphism_morphism (HM (Y:=x)) =
IsInitialMorphism_morphism (HM (Y:=z)) o (f o g)
      rewrite ?composition_of.
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
x, y, z: C
g: morphism C x y
f: morphism C y z
G
_1 (IsInitialMorphism_property_morphism (HM (Y:=y))
      (IsInitialMorphism_object (HM (Y:=z)))
      (IsInitialMorphism_morphism (HM (Y:=z)) o f))
o G
  _1 (IsInitialMorphism_property_morphism (HM (Y:=x))
        (IsInitialMorphism_object (HM (Y:=y)))
        (IsInitialMorphism_morphism (HM (Y:=y)) o g))
o IsInitialMorphism_morphism (HM (Y:=x)) =
IsInitialMorphism_morphism (HM (Y:=z)) o (f o g)
      repeat
        try_associativity_quick
        rewrite IsInitialMorphism_property_morphism_property.
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
x, y, z: C
g: morphism C x y
f: morphism C y z
IsInitialMorphism_morphism (HM (Y:=z)) o f o g =
IsInitialMorphism_morphism (HM (Y:=z)) o f o g
      reflexivity.
    Qed.

    Definition functor__of__initial_morphism : Functor C D
      := Build_Functor
           C D
           (fun x => obj_of x)
           (fun s d m => mor_of s d m)
           composition_of
           identity_of.

    Definition adjunction__of__initial_morphism
    : functor__of__initial_morphism -| G.
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
functor__of__initial_morphism -| G
    Proof.
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
functor__of__initial_morphism -| G
      refine (adjunction_unit_counit__of__adjunction_unit _).
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
AdjunctionUnit functor__of__initial_morphism G
      eexists (Build_NaturalTransformation
                1
                (G o functor__of__initial_morphism)
                (fun x => IsInitialMorphism_morphism (@HM x))
                (fun s d m =>
                   symmetry
                     _ _
                     (IsInitialMorphism_property_morphism_property (@HM s) _ _))).
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
forall (c : C) (d : D)
(f : morphism C c (G _0 d)%object),
Contr
  {g
  : morphism D
      (functor__of__initial_morphism _0 c)%object d &
  G _1 g
  o Build_NaturalTransformation 1
      (G o functor__of__initial_morphism)
      (fun x : C =>
       IsInitialMorphism_morphism (HM (Y:=x)))
      (fun (s d0 : C) (m : morphism C s d0) =>
       symmetry
         (G
          _1 (IsInitialMorphism_property_morphism
                (HM (Y:=s))
                (functor__of__initial_morphism _0 d0)
                (IsInitialMorphism_morphism
                   (HM (Y:=d0)) o 1 _1 m))
          o IsInitialMorphism_morphism (HM (Y:=s)))
         (IsInitialMorphism_morphism (HM (Y:=d0))
          o 1 _1 m)
         (IsInitialMorphism_property_morphism_property
            (HM (Y:=s))
            (functor__of__initial_morphism _0 d0)
            (IsInitialMorphism_morphism (HM (Y:=d0))
             o 1 _1 m))) c = f}
      simpl.
C, D: PreCategory
G: Functor D C
M: forall x : C, (x / G)%category
HM: forall Y : C, IsInitialMorphism (M Y)
forall (c : C) (d : D)
(f : morphism C c (G _0 d)%object),
Contr
  {g
  : morphism D (IsInitialMorphism_object (HM (Y:=c)))
      d &
  G _1 g o IsInitialMorphism_morphism (HM (Y:=c)) = f}
      exact (fun c => @IsInitialMorphism_property _ _ c G (M c) (@HM c)).
    Defined.
  End initial.

  (** ** a terminal object of [(F / X)] for all [X : D] gives a right adjoint to [F] *)
  Section terminal.
    Variables C D : PreCategory.

    Variable F : Functor C D.
    Context `(HM : forall X, @IsTerminalMorphism _ _ F X (M X)).

    Definition functor__of__terminal_morphism : Functor D C
      := (@functor__of__initial_morphism
            (D^op) (C^op)
            (F^op)
            (fun x : D => dual_functor F !x (M x)) HM)^op.

    Definition adjunction__of__terminal_morphism
    : F -| functor__of__terminal_morphism
      := ((@adjunction__of__initial_morphism
             (D^op) (C^op)
             (F^op)
             (fun x : D => dual_functor F !x (M x)) HM)^op)%adjunction.
  End terminal.
End adjunction_from_universal.