(** * Properties of pointwise functors *)
Require Import Category.Core Functor.Core Functor.Pointwise.Core NaturalTransformation.Core NaturalTransformation.Paths Functor.Composition.Core Functor.Identity Functor.Paths.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import PathGroupoids Types.Forall HoTT.Tactics.
Require Import Basics.Tactics.

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

Local Open Scope category_scope.
Local Open Scope functor_scope.

Section parts.
  Context `{Funext}.

  (** We could do this all in a big [repeat match], but we split it
      up, to shave off about two seconds per proof. *)
  Local Ltac functor_pointwise_t helper_lem_match helper_lem :=
    repeat (apply path_forall; intro);
    rewrite !transport_forall_constant, !path_forall_2_beta;
    path_natural_transformation;
    repeat match goal with
             | [ |- context[components_of (transport ?P ?p ?z)] ]
               => simpl rewrite (@ap_transport _ P _ _ _ p (fun _ => components_of) z)
           end;
    rewrite !transport_forall_constant;
    transport_to_ap;
    repeat match goal with
             | [ x : _ |- context[ap (fun x3 : ?T => ?f (object_of x3 ?z))] ]
               => rewrite (@ap_compose' _ _ _ (fun x3' : T => object_of x3') (fun Ox3 => f (Ox3 x)))
             | [ x : _ |- context[ap (fun x3 : ?T => ?f (object_of x3 ?z) ?w)] ]
               => rewrite (@ap_compose' _ _ _ (fun x3' : T => object_of x3') (fun Ox3 => f (Ox3 x) w))
           end;
    repeat match goal with
             | _ => done
             | [ |- context[fun F => @object_of ?C ?D F] ]
               => progress change (fun F' => @object_of C D F') with (@object_of C D)
             | [ |- context[helper_lem_match ?x] ]
               => rewrite (helper_lem x)
           end.

  (** ** respects identity *)
  Section identity_of.
    Variables C D : PreCategory.

    Lemma identity_of_helper_helper (x : Functor C D)
    : 1 o x o 1 = x.
H: Funext
C, D: PreCategory
x: Functor C D
1 o x o 1 = x
    Proof.
H: Funext
C, D: PreCategory
x: Functor C D
1 o x o 1 = x
      path_functor.
    Defined.

    Definition identity_of_helper_helper_object_of x
    : ap object_of (identity_of_helper_helper x) = idpath
      := path_functor_uncurried_fst _ _ _.

    Lemma identity_of_helper
    : (fun x : Functor C D => 1 o x o 1) = idmap.
H: Funext
C, D: PreCategory
(fun x : Functor C D => 1 o x o 1) = idmap
    Proof.
H: Funext
C, D: PreCategory
(fun x : Functor C D => 1 o x o 1) = idmap
      apply path_forall; intro x.
H: Funext
C, D: PreCategory
x: Functor C D
1 o x o 1 = x
      apply identity_of_helper_helper.
    Defined.

    Lemma identity_of
    : pointwise (identity C) (identity D) = identity _.
H: Funext
C, D: PreCategory
pointwise 1 1 = 1
    Proof.
H: Funext
C, D: PreCategory
pointwise 1 1 = 1
      path_functor.
H: Funext
C, D: PreCategory
{HO : (fun x : Functor C D => 1 o x o 1) = idmap &
transport
  (fun GO : Functor C D -> Functor C D =>
   forall s d : Functor C D,
   NaturalTransformation s d ->
   NaturalTransformation (GO s) (GO d)) HO
  (pointwise_morphism_of 1 1) =
(fun s d : Functor C D => idmap)}
      exists identity_of_helper.
H: Funext
C, D: PreCategory
transport
  (fun GO : Functor C D -> Functor C D =>
   forall s d : Functor C D,
   NaturalTransformation s d ->
   NaturalTransformation (GO s) (GO d))
  identity_of_helper (pointwise_morphism_of 1 1) =
(fun s d : Functor C D => idmap)
      unfold identity_of_helper.
H: Funext
C, D: PreCategory
transport
  (fun GO : Functor C D -> Functor C D =>
   forall s d : Functor C D,
   NaturalTransformation s d ->
   NaturalTransformation (GO s) (GO d))
  (path_forall (fun x : Functor C D => 1 o x o 1)
     idmap
     (fun x : Functor C D =>
      identity_of_helper_helper x))
  (pointwise_morphism_of 1 1) =
(fun s d : Functor C D => idmap)
      abstract functor_pointwise_t
               identity_of_helper_helper
               identity_of_helper_helper_object_of.
    Defined.
  End identity_of.

  (** ** respects composition *)
  Section composition_of.
    Variables C D C' D' C'' D'' : PreCategory.

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

    Lemma composition_of_helper_helper (x : Functor C'' D)
    : G' o G o x o (F' o F) = G' o (G o x o F') o F.
H: Funext
C, D, C', D', C'', D'': PreCategory
F': Functor C' C''
G: Functor D D'
F: Functor C C'
G': Functor D' D''
x: Functor C'' D
G' o G o x o (F' o F) = G' o (G o x o F') o F
    Proof.
H: Funext
C, D, C', D', C'', D'': PreCategory
F': Functor C' C''
G: Functor D D'
F: Functor C C'
G': Functor D' D''
x: Functor C'' D
G' o G o x o (F' o F) = G' o (G o x o F') o F
      path_functor.
    Defined.

    Definition composition_of_helper_helper_object_of x
    : ap object_of (composition_of_helper_helper x) = idpath
      := path_functor_uncurried_fst _ _ _.

    Lemma composition_of_helper
    : (fun x => G' o G o x o (F' o F)) = (fun x => G' o (G o x o F') o F).
H: Funext
C, D, C', D', C'', D'': PreCategory
F': Functor C' C''
G: Functor D D'
F: Functor C C'
G': Functor D' D''
(fun x : Functor C'' D => G' o G o x o (F' o F)) =
(fun x : Functor C'' D => G' o (G o x o F') o F)
    Proof.
H: Funext
C, D, C', D', C'', D'': PreCategory
F': Functor C' C''
G: Functor D D'
F: Functor C C'
G': Functor D' D''
(fun x : Functor C'' D => G' o G o x o (F' o F)) =
(fun x : Functor C'' D => G' o (G o x o F') o F)
      apply path_forall; intro x.
H: Funext
C, D, C', D', C'', D'': PreCategory
F': Functor C' C''
G: Functor D D'
F: Functor C C'
G': Functor D' D''
x: Functor C'' D
G' o G o x o (F' o F) = G' o (G o x o F') o F
      apply composition_of_helper_helper.
    Defined.

    Lemma composition_of
    : pointwise (F' o F) (G' o G) = pointwise F G' o pointwise F' G.
H: Funext
C, D, C', D', C'', D'': PreCategory
F': Functor C' C''
G: Functor D D'
F: Functor C C'
G': Functor D' D''
pointwise (F' o F) (G' o G) =
pointwise F G' o pointwise F' G
    Proof.
H: Funext
C, D, C', D', C'', D'': PreCategory
F': Functor C' C''
G: Functor D D'
F: Functor C C'
G': Functor D' D''
pointwise (F' o F) (G' o G) =
pointwise F G' o pointwise F' G
      path_functor.
H: Funext
C, D, C', D', C'', D'': PreCategory
F': Functor C' C''
G: Functor D D'
F: Functor C C'
G': Functor D' D''
{HO
: (fun x : Functor C'' D => G' o G o x o (F' o F)) =
  (fun c : Functor C'' D => G' o (G o c o F') o F) &
transport
  (fun GO : Functor C'' D -> Functor C D'' =>
   forall s d : Functor C'' D,
   NaturalTransformation s d ->
   NaturalTransformation (GO s) (GO d)) HO
  (pointwise_morphism_of (F' o F) (G' o G)) =
(fun (s d : Functor C'' D)
   (m : NaturalTransformation s d) =>
 Core.whisker_r
   (Core.whisker_l G'
      (Core.whisker_r (Core.whisker_l G m) F')) F)}
      exists composition_of_helper.
H: Funext
C, D, C', D', C'', D'': PreCategory
F': Functor C' C''
G: Functor D D'
F: Functor C C'
G': Functor D' D''
transport
  (fun GO : Functor C'' D -> Functor C D'' =>
   forall s d : Functor C'' D,
   NaturalTransformation s d ->
   NaturalTransformation (GO s) (GO d))
  composition_of_helper
  (pointwise_morphism_of (F' o F) (G' o G)) =
(fun (s d : Functor C'' D)
   (m : NaturalTransformation s d) =>
 Core.whisker_r
   (Core.whisker_l G'
      (Core.whisker_r (Core.whisker_l G m) F')) F)
      unfold composition_of_helper.
H: Funext
C, D, C', D', C'', D'': PreCategory
F': Functor C' C''
G: Functor D D'
F: Functor C C'
G': Functor D' D''
transport
  (fun GO : Functor C'' D -> Functor C D'' =>
   forall s d : Functor C'' D,
   NaturalTransformation s d ->
   NaturalTransformation (GO s) (GO d))
  (path_forall
     (fun x : Functor C'' D => G' o G o x o (F' o F))
     (fun x : Functor C'' D => G' o (G o x o F') o F)
     (fun x : Functor C'' D =>
      composition_of_helper_helper x))
  (pointwise_morphism_of (F' o F) (G' o G)) =
(fun (s d : Functor C'' D)
   (m : NaturalTransformation s d) =>
 Core.whisker_r
   (Core.whisker_l G'
      (Core.whisker_r (Core.whisker_l G m) F')) F)
      abstract functor_pointwise_t
               composition_of_helper_helper
               composition_of_helper_helper_object_of.
    Defined.
  End composition_of.
End parts.