Library HoTT.Categories.NaturalTransformation.Pointwise

Pointwise Natural Transformations

Require Import Category.Core Functor.Core NaturalTransformation.Core.
Require Import FunctorCategory.Core NaturalTransformation.Paths Functor.Composition.Core NaturalTransformation.Composition.Core.
Require Import Functor.Pointwise.Core.

Set Implicit Arguments.
Generalizable All Variables.

Recall that a "pointwise" functor is a functor Aᴮ → Cᴰ induced by functors D → B and A → C. Given two functors D → B and a natural transformation between them, there is an induced natural transformation between the resulting functors between functor categories, and similarly for two functors A → C. In this file, we construct these natural transformations. They will be used to construct the pointwise induced adjunction Fˣ ⊣ Gˣ of an adjunction F ⊣ G for all categories X.

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

Section pointwise.
  Context `{Funext}.

  Variables C D C' D' : PreCategory.

  Local Ltac t :=
    path_natural_transformation; simpl;
    rewrite <- ?composition_of;
    try apply ap;
    first [ apply commutes
          | symmetry; apply commutes ].

Tˣ for a natural transformation T : F → G and a functor x : C → D

  Definition pointwise_l
             (F G : Functor C D)
             (T : NaturalTransformation F G)
             (F' : Functor C' D')
  : NaturalTransformation (pointwise F F') (pointwise G F').
  Proof.
    refine (Build_NaturalTransformation
              (pointwise F F') (pointwise G F')
              (fun f : object (D → C') ⇒ (F' o f ) oL T)%natural_transformation
              _).
    abstract t.
  Defined.

Fᵀ for a natural transformation T : F' → G' and a functor F : C → D

  Definition pointwise_r
             (F : Functor C D)
             (F' G' : Functor C' D')
             (T' : NaturalTransformation F' G')
  : NaturalTransformation (pointwise F F') (pointwise F G').
  Proof.
    refine (Build_NaturalTransformation
              (pointwise F F') (pointwise F G')
              (fun f : object (D → C') ⇒ T' oR f oR F)%natural_transformation
              _).
    abstract t.
  Defined.
End pointwise.