(** * Pointwise Adjunctions *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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 Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

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.