(** * Pointwise Adjunctions *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.
Require Import Functor.Identity.
Require Import Functor.Composition.Core NaturalTransformation.Composition.Core.
Require Import Adjoint.Core Adjoint.UnitCounit Adjoint.UnitCounitCoercions.
Require Import Functor.Pointwise.Core.
Require NaturalTransformation.Pointwise.
Require Functor.Pointwise.Properties.
Require Import Category.Morphisms FunctorCategory.Morphisms.
Require Import FunctorCategory.Core.
Import NaturalTransformation.Identity.NaturalTransformationIdentityNotations.
Require Import NaturalTransformation.Paths Functor.Paths.
Require Import Basics.PathGroupoids HoTT.Tactics Types.Arrow.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope morphism_scope.
Local Open Scope functor_scope.
Local Open Scope natural_transformation_scope.

Section AdjointPointwise.
  Context `{Funext}.

  Variables C D : PreCategory.

  (** ** [F ⊣ G] → [E^F ⊣ E^G] *)
  Section l.
    Variable E : PreCategory.

    Variable F : Functor C D.
    Variable G : Functor D C.

    Variable A : F -| G.

    Definition unit_l
    : NaturalTransformation (identity (E -> C))
                            ((pointwise (identity E) G) o (pointwise (identity E) F)).
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
NaturalTransformation 1 (pointwise 1 G o pointwise 1 F)
    Proof.
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
NaturalTransformation 1 (pointwise 1 G o pointwise 1 F)
      pose proof (A : AdjunctionUnit _ _) as A''.
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
A'': AdjunctionUnit F G
NaturalTransformation 1 (pointwise 1 G o pointwise 1 F)
      refine (_ o (((idtoiso (C := (_ -> _)) (Functor.Pointwise.Properties.identity_of _ _))^-1)%morphism : morphism _ _ _)).
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
A'': AdjunctionUnit F G
NaturalTransformation (pointwise 1 1) (pointwise 1 G o pointwise 1 F)
      refine (_ o NaturalTransformation.Pointwise.pointwise_r (Functor.Identity.identity E) (proj1 A'')).
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
A'': AdjunctionUnit F G
NaturalTransformation (pointwise 1 (G o F)) (pointwise 1 G o pointwise 1 F)
      refine (((idtoiso
                  (C := (_ -> _))
                  (Functor.Pointwise.Properties.composition_of
                     (Functor.Identity.identity E) F
                     (Functor.Identity.identity E) G)) : morphism _ _ _)
                o _).
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
A'': AdjunctionUnit F G
NaturalTransformation (pointwise 1 (G o F)) (pointwise (1 o 1) (G o F))
      refine (NaturalTransformation.Pointwise.pointwise_l _ _).
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
A'': AdjunctionUnit F G
NaturalTransformation 1 (1 o 1)
      exact (NaturalTransformation.Composition.Laws.left_identity_natural_transformation_2 _).
    Defined.

    Definition counit_l
    : NaturalTransformation (pointwise (identity E) F o pointwise (identity E) G)
                            (identity (E -> D)).
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
NaturalTransformation (pointwise 1 F o pointwise 1 G) 1
    Proof.
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
NaturalTransformation (pointwise 1 F o pointwise 1 G) 1
      pose proof (A : AdjunctionCounit _ _) as A''.
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
A'': AdjunctionCounit F G
NaturalTransformation (pointwise 1 F o pointwise 1 G) 1
      refine ((((idtoiso (C := (_ -> _)) (Functor.Pointwise.Properties.identity_of _ _)))%morphism : morphism _ _ _) o _).
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
A'': AdjunctionCounit F G
NaturalTransformation (pointwise 1 F o pointwise 1 G) (pointwise 1 1)
      refine (NaturalTransformation.Pointwise.pointwise_r (Functor.Identity.identity E) (proj1 A'') o _).
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
A'': AdjunctionCounit F G
NaturalTransformation (pointwise 1 F o pointwise 1 G) (pointwise 1 (F o G))
      refine (_ o
                (((idtoiso
                     (C := (_ -> _))
                     (Functor.Pointwise.Properties.composition_of
                        (Functor.Identity.identity E) G
                        (Functor.Identity.identity E) F))^-1)%morphism : morphism _ _ _)).
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
A'': AdjunctionCounit F G
NaturalTransformation (pointwise (1 o 1) (F o G)) (pointwise 1 (F o G))
      refine (NaturalTransformation.Pointwise.pointwise_l _ _).
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
A'': AdjunctionCounit F G
NaturalTransformation (1 o 1) 1
      exact (NaturalTransformation.Composition.Laws.left_identity_natural_transformation_1 _).
    Defined.

    Create HintDb adjoint_pointwise discriminated.
    Hint Rewrite
         identity_of left_identity right_identity
         eta_idtoiso composition_of idtoiso_functor
         @ap_V @ap10_V @ap10_path_forall
         path_functor_uncurried_fst
    : adjoint_pointwise.

    Definition pointwise_l : pointwise (identity E) F -| pointwise (identity E) G.
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
pointwise 1 F -| pointwise 1 G
    Proof.
H: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
pointwise 1 F -| pointwise 1 G
      exists unit_l counit_l;
      abstract (
          path_natural_transformation;
          intros;
          destruct A;
          simpl in *;
            repeat match goal with
                      | _ => progress simpl
                      | _ => progress autorewrite with adjoint_pointwise
                      | [ |- context[ap object_of (path_functor_uncurried ?F ?G (?HO; ?HM))] ]
                        => rewrite (@path_functor_uncurried_fst _ _ _ F G HO HM)
                      | _ => progress unfold Functor.Pointwise.Properties.identity_of
                      | _ => progress unfold Functor.Pointwise.Properties.composition_of
                      | _ => progress unfold Functor.Pointwise.Properties.identity_of_helper
                      | _ => progress unfold Functor.Pointwise.Properties.composition_of_helper
                      | _ => progress unfold Functor.Pointwise.Properties.identity_of_helper_helper
                      | _ => progress unfold Functor.Pointwise.Properties.composition_of_helper_helper
                      | [ H : _ |- _ ] => apply H
                    end
        ). (* 23.345 s *)
    Defined.
  End l.

  (** ** [F ⊣ G] → [Gᴱ ⊣ Fᴱ] *)
  Section r.
    Variable F : Functor C D.
    Variable G : Functor D C.

    Variable A : F -| G.

    Variable E : PreCategory.

    Definition unit_r
    : NaturalTransformation (identity (C -> E))
                            ((pointwise F (identity E)) o (pointwise G (identity E))).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
NaturalTransformation 1 (pointwise F 1 o pointwise G 1)
    Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
NaturalTransformation 1 (pointwise F 1 o pointwise G 1)
      pose proof (A : AdjunctionUnit _ _) as A''.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
A'': AdjunctionUnit F G
NaturalTransformation 1 (pointwise F 1 o pointwise G 1)
      refine (_ o (((idtoiso (C := (_ -> _)) (Functor.Pointwise.Properties.identity_of _ _))^-1)%morphism : morphism _ _ _)).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
A'': AdjunctionUnit F G
NaturalTransformation (pointwise 1 1) (pointwise F 1 o pointwise G 1)
      refine (_ o NaturalTransformation.Pointwise.pointwise_l (proj1 A'') (Functor.Identity.identity E)).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
A'': AdjunctionUnit F G
NaturalTransformation (pointwise (G o F) 1) (pointwise F 1 o pointwise G 1)
      refine (((idtoiso
                  (C := (_ -> _))
                  (Functor.Pointwise.Properties.composition_of
                     G (Functor.Identity.identity E)
                     F (Functor.Identity.identity E))) : morphism _ _ _)
                o _).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
A'': AdjunctionUnit F G
NaturalTransformation (pointwise (G o F) 1) (pointwise (G o F) (1 o 1))
      refine (NaturalTransformation.Pointwise.pointwise_r _ _).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
A'': AdjunctionUnit F G
NaturalTransformation 1 (1 o 1)
      exact (NaturalTransformation.Composition.Laws.left_identity_natural_transformation_2 _).
    Defined.

    Definition counit_r
    : NaturalTransformation (pointwise G (identity E) o pointwise F (identity E))
                            (identity (D -> E)).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
NaturalTransformation (pointwise G 1 o pointwise F 1) 1
    Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
NaturalTransformation (pointwise G 1 o pointwise F 1) 1
      pose proof (A : AdjunctionCounit _ _) as A''.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
A'': AdjunctionCounit F G
NaturalTransformation (pointwise G 1 o pointwise F 1) 1
      refine ((((idtoiso (C := (_ -> _)) (Functor.Pointwise.Properties.identity_of _ _)))%morphism : morphism _ _ _) o _).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
A'': AdjunctionCounit F G
NaturalTransformation (pointwise G 1 o pointwise F 1) (pointwise 1 1)
      refine (NaturalTransformation.Pointwise.pointwise_l (proj1 A'') (Functor.Identity.identity E) o _).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
A'': AdjunctionCounit F G
NaturalTransformation (pointwise G 1 o pointwise F 1) (pointwise (F o G) 1)
      refine (_ o
                (((idtoiso
                     (C := (_ -> _))
                     (Functor.Pointwise.Properties.composition_of
                        F (Functor.Identity.identity E)
                        G (Functor.Identity.identity E)))^-1)%morphism : morphism _ _ _)).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
A'': AdjunctionCounit F G
NaturalTransformation (pointwise (F o G) (1 o 1)) (pointwise (F o G) 1)
      refine (NaturalTransformation.Pointwise.pointwise_r _ _).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
A'': AdjunctionCounit F G
NaturalTransformation (1 o 1) 1
      exact (NaturalTransformation.Composition.Laws.left_identity_natural_transformation_1 _).
    Defined.

    Create HintDb adjoint_pointwise discriminated.
    Hint Rewrite
         identity_of left_identity right_identity
         eta_idtoiso composition_of idtoiso_functor
         @ap_V @ap10_V @ap10_path_forall
         path_functor_uncurried_fst
    : adjoint_pointwise.

    Definition pointwise_r : pointwise G (identity E) -| pointwise F (identity E).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
pointwise G 1 -| pointwise F 1
    Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
E: PreCategory
pointwise G 1 -| pointwise F 1
      exists unit_r counit_r;
      abstract (
          path_natural_transformation;
          intros;
          destruct A;
          simpl in *;
            repeat match goal with
                      | _ => reflexivity
                      | _ => progress simpl
                      | _ => progress autorewrite with adjoint_pointwise
                      | [ |- context[ap object_of (path_functor_uncurried ?F ?G (?HO; ?HM))] ]
                        => rewrite (@path_functor_uncurried_fst _ _ _ F G HO HM)
                      | _ => progress unfold Functor.Pointwise.Properties.identity_of
                      | _ => progress unfold Functor.Pointwise.Properties.composition_of
                      | _ => progress unfold Functor.Pointwise.Properties.identity_of_helper
                      | _ => progress unfold Functor.Pointwise.Properties.composition_of_helper
                      | _ => progress unfold Functor.Pointwise.Properties.identity_of_helper_helper
                      | _ => progress unfold Functor.Pointwise.Properties.composition_of_helper_helper
                      | _ => rewrite <- composition_of; progress rewrite_hyp
                    end
        ). (* 19.097 *)
    Defined.
  End r.
End AdjointPointwise.