(** * Natural transformations involving product categories *)
Require Import Category.Core Functor.Core Category.Prod Functor.Prod.Core NaturalTransformation.Core.
Require Import Types.Prod.

Set Implicit Arguments.
Generalizable All Variables.

(** ** Product of natural transformations *)
Section prod.
  Context {A : PreCategory}.
  Context {B : PreCategory}.
  Context {C : PreCategory}.
  Variables F F' : Functor A B.
  Variables G G' : Functor A C.
  Variable T : NaturalTransformation F F'.
  Variable U : NaturalTransformation G G'.

  Definition prod
  : NaturalTransformation (F * G) (F' * G')
    := Build_NaturalTransformation
         (F * G) (F' * G')
         (fun x : A => (T x, U x))
         (fun _ _ _ => path_prod' (commutes T _ _ _) (commutes U _ _ _)).
End prod.

Local Infix "*" := prod : natural_transformation_scope.

(** ** Natural transformations between partially applied functors *)
Section induced.
  Variables C D E : PreCategory.

  Variable F : Functor (C * D) E.

  Local Ltac t :=
    simpl; intros;
    rewrite <- !composition_of;
    simpl;
    rewrite ?left_identity, ?right_identity;
    reflexivity.

  Definition induced_fst s d (m : morphism C s d)
  : NaturalTransformation (Functor.Prod.Core.induced_snd F s)
                          (Functor.Prod.Core.induced_snd F d).
C, D, E: PreCategory
F: Functor (C * D) E
s, d: C
m: morphism C s d
NaturalTransformation (induced_snd F s) (induced_snd F d)
  Proof.
C, D, E: PreCategory
F: Functor (C * D) E
s, d: C
m: morphism C s d
NaturalTransformation (induced_snd F s) (induced_snd F d)
    let F0 := match goal with |- NaturalTransformation ?F0 ?G0 => constr:(F0) end in
    let G0 := match goal with |- NaturalTransformation ?F0 ?G0 => constr:(G0) end in
    refine (Build_NaturalTransformation
              F0 G0
              (fun d => @morphism_of _ _ F (_, _) (_, _) (m, @identity D d))
              _).
C, D, E: PreCategory
F: Functor (C * D) E
s, d: C
m: morphism C s d
forall (s0 d0 : D) (m0 : morphism D s0 d0),
(F _1 (m, 1) o (induced_snd F s) _1 m0)%morphism =
((induced_snd F d) _1 m0 o F _1 (m, 1))%morphism
    abstract t.
  Defined.

  Definition induced_snd s d (m : morphism D s d)
  : NaturalTransformation (Functor.Prod.Core.induced_fst F s)
                          (Functor.Prod.Core.induced_fst F d).
C, D, E: PreCategory
F: Functor (C * D) E
s, d: D
m: morphism D s d
NaturalTransformation (Core.induced_fst F s) (Core.induced_fst F d)
  Proof.
C, D, E: PreCategory
F: Functor (C * D) E
s, d: D
m: morphism D s d
NaturalTransformation (Core.induced_fst F s) (Core.induced_fst F d)
    let F0 := match goal with |- NaturalTransformation ?F0 ?G0 => constr:(F0) end in
    let G0 := match goal with |- NaturalTransformation ?F0 ?G0 => constr:(G0) end in
    refine (Build_NaturalTransformation
              F0 G0
              (fun c => @morphism_of _ _ F (_, _) (_, _) (@identity C c, m))
              _).
C, D, E: PreCategory
F: Functor (C * D) E
s, d: D
m: morphism D s d
forall (s0 d0 : C) (m0 : morphism C s0 d0),
(F _1 (1, m) o (Core.induced_fst F s) _1 m0)%morphism =
((Core.induced_fst F d) _1 m0 o F _1 (1, m))%morphism
    abstract t.
  Defined.
End induced.

Module Export NaturalTransformationProdNotations.
  Infix "*" := prod : natural_transformation_scope.
End NaturalTransformationProdNotations.