Require Import Category.Core Functor.Core FunctorCategory.Core Category.Prod.
Require Import Functor.Prod Functor.Composition.Core NaturalTransformation.Composition.Laws NaturalTransformation.Composition.Core.
Require Import Types.Prod.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope natural_transformation_scope.
Local Open Scope functor_scope.

Local Notation fst_type := Basics.Overture.fst.
Local Notation snd_type := Basics.Overture.snd.
Local Notation pair_type := Basics.Overture.pair.

Section law3.
  Context `{Funext}.
  Variables C1 C2 D : PreCategory.

  Definition functor
  : Functor (D → C1 × C2) ((D → C1) × (D → C2))
    := Build_Functor
         (D → C1 × C2) ((D → C1) × (D → C2))
         (fun H ⇒ (fst o H, snd o H)%core)
         (fun s d m ⇒ (fst oL m, snd oL m)%core)
         (fun _ _ _ _ _ ⇒ path_prod' (composition_of_whisker_l _ _ _)
                                      (composition_of_whisker_l _ _ _))
         (fun _ ⇒ path_prod' (whisker_l_right_identity _ _)
                              (whisker_l_right_identity _ _)).

  Definition inverse
  : Functor ((D → C1) × (D → C2)) (D → C1 × C2)
    := Functor.Prod.Functorial.functor _ _ _.
End law3.