(** * Laws about an exponential of a product and a product of exponentials *)
Require Import Category.Core Functor.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Functor.Prod.
Require Import Functor.Paths.
Require Import Functor.Identity Functor.Composition.Core.
Require Import ExponentialLaws.Law3.Functors.
Require Import Types.Prod ExponentialLaws.Tactics.

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

Local Open Scope functor_scope.

(** ** [(y × z)ⁿ ≅ yⁿ × zⁿ] *)
Section Law3.
  Context `{Funext}.
  Variables C1 C2 D : PreCategory.

  Lemma helper (c : Functor D C1 * Functor D C2)
  : ((fst o (Basics.Overture.fst c * Basics.Overture.snd c))%functor,
     (snd o (Basics.Overture.fst c * Basics.Overture.snd c))%functor)%core = c.
H: Funext
C1, C2, D: PreCategory
c: (Functor D C1 * Functor D C2)%type
(fst o (Overture.fst c * Overture.snd c),
snd o (Overture.fst c * Overture.snd c))%core = c
  Proof.
H: Funext
C1, C2, D: PreCategory
c: (Functor D C1 * Functor D C2)%type
(fst o (Overture.fst c * Overture.snd c),
snd o (Overture.fst c * Overture.snd c))%core = c
    apply path_prod;
    [ apply compose_fst_prod
    | apply compose_snd_prod ].
  Defined.

  Lemma Law
  : functor C1 C2 D o inverse C1 C2 D = 1
    /\ inverse C1 C2 D o functor C1 C2 D = 1.
H: Funext
C1, C2, D: PreCategory
((functor C1 C2 D o inverse C1 C2 D = 1) *
 (inverse C1 C2 D o functor C1 C2 D = 1))%type
  Proof.
H: Funext
C1, C2, D: PreCategory
((functor C1 C2 D o inverse C1 C2 D = 1) *
 (inverse C1 C2 D o functor C1 C2 D = 1))%type
    split; path_functor;
    [ (exists (path_forall _ _ helper))
    | (exists (path_forall _ _ (fun _ => Functor.Prod.Universal.unique idpath idpath))) ];
    exp_laws_t;
    unfold helper, compose_fst_prod, compose_snd_prod, Functor.Prod.Universal.unique, Functor.Prod.Universal.unique_helper;
    exp_laws_t.
  Qed.
End Law3.