(** * Adjunctions as universal morphisms *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.
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.
Import Comma.Core.
Require Import UniversalProperties Comma.Dual InitialTerminalCategory.Core InitialTerminalCategory.Functors.

Set Implicit Arguments.
Generalizable All Variables.

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 Abbreviation obj_of Y :=
      (IsInitialMorphism_object (@HM Y))
        (only parsing).

    Local Abbreviation 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 Y0 : C, IsInitialMorphism (M Y0)
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 Y0 : C, IsInitialMorphism (M Y0)
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 Y0 : C, IsInitialMorphism (M Y0)
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 Y0 : C, IsInitialMorphism (M Y0)
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 Y0 : C, IsInitialMorphism (M Y0)
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 x0 : C, (x0 / 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 x0 : C, (x0 / 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 x0 : C, (x0 / 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 x0 : C, (x0 / 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 x0 : C, (x0 / 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 x0 : C, (x0 / 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.