(** * Law about currying *)
Require Import Category.Core Functor.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Functor.Paths.
Require Import Functor.Identity Functor.Composition.Core.
Require Import ExponentialLaws.Law4.Functors.
Require Import ExponentialLaws.Tactics.

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

Local Open Scope functor_scope.

(** ** [(C₁ × C₂ → D) ≅ (C₁ → (C₂ → D))] *)
Section Law4.
  Context `{Funext}.
  Variables C1 C2 D : PreCategory.

  Lemma helper1 c
  : functor C1 C2 D (inverse C1 C2 D c) = c.
H: Funext
C1, C2, D: PreCategory
c: Core.functor_category (Prod.prod C1 C2) D
((functor C1 C2 D) _0 ((inverse C1 C2 D) _0 c))%object =
c
  Proof.
H: Funext
C1, C2, D: PreCategory
c: Core.functor_category (Prod.prod C1 C2) D
((functor C1 C2 D) _0 ((inverse C1 C2 D) _0 c))%object =
c
    path_functor.
H: Funext
C1, C2, D: PreCategory
c: Core.functor_category (Prod.prod C1 C2) D
transport
  (fun GO : C1 * C2 -> D =>
   forall s d : C1 * C2,
   morphism C1 (fst s) (fst d) *
   morphism C2 (snd s) (snd d) ->
   morphism D (GO s) (GO d)) 1
  (fun (s d : C1 * C2)
     (m : morphism C1 (fst s) (fst d) *
          morphism C2 (snd s) (snd d)) =>
   (c _1 (1, snd m) o c _1 (fst m, 1))%morphism) =
morphism_of c
    abstract (
        exp_laws_t;
        rewrite <- composition_of;
        exp_laws_t
      ).
  Defined.

  Lemma helper2_helper c x
  : inverse C1 C2 D (functor C1 C2 D c) x = c x.
H: Funext
C1, C2, D: PreCategory
c: Core.functor_category C1
  (Core.functor_category C2 D)
x: C1
(((inverse C1 C2 D) _0 ((functor C1 C2 D) _0 c)) _0 x)%object =
(c _0 x)%object
  Proof.
H: Funext
C1, C2, D: PreCategory
c: Core.functor_category C1
  (Core.functor_category C2 D)
x: C1
(((inverse C1 C2 D) _0 ((functor C1 C2 D) _0 c)) _0 x)%object =
(c _0 x)%object
    path_functor.
H: Funext
C1, C2, D: PreCategory
c: Core.functor_category C1
  (Core.functor_category C2 D)
x: C1
transport
  (fun GO : C2 -> D =>
   forall s d : C2,
   morphism C2 s d -> morphism D (GO s) (GO d)) 1
  (fun (s2 d2 : C2) (m2 : morphism C2 s2 d2) =>
   ((c _0 x)%object _1 m2
    o Core.components_of (c _1 1) s2)%morphism) =
morphism_of (c _0 x)%object
    abstract exp_laws_t.
  Defined.

  Lemma helper2 c
  : inverse C1 C2 D (functor C1 C2 D c) = c.
H: Funext
C1, C2, D: PreCategory
c: Core.functor_category C1
  (Core.functor_category C2 D)
((inverse C1 C2 D) _0 ((functor C1 C2 D) _0 c))%object =
c
  Proof.
H: Funext
C1, C2, D: PreCategory
c: Core.functor_category C1
  (Core.functor_category C2 D)
((inverse C1 C2 D) _0 ((functor C1 C2 D) _0 c))%object =
c
    path_functor.
H: Funext
C1, C2, D: PreCategory
c: Core.functor_category C1
  (Core.functor_category C2 D)
{HO
: inverse_object_of_object_of (functor_object_of c) =
  c &
transport
  (fun GO : C1 -> Functor C2 D =>
   forall s d : C1,
   morphism C1 s d ->
   Core.NaturalTransformation (GO s) (GO d)) HO
  (inverse_object_of_morphism_of (functor_object_of c)) =
morphism_of c}
    exists (path_forall _ _ (helper2_helper c)).
H: Funext
C1, C2, D: PreCategory
c: Core.functor_category C1
  (Core.functor_category C2 D)
transport
  (fun GO : C1 -> Functor C2 D =>
   forall s d : C1,
   morphism C1 s d ->
   Core.NaturalTransformation (GO s) (GO d))
  (path_forall
     ((inverse C1 C2 D) _0 ((functor C1 C2 D) _0 c))%object
     c (helper2_helper c))
  (inverse_object_of_morphism_of (functor_object_of c)) =
morphism_of c
    abstract (unfold helper2_helper; exp_laws_t).
  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)
  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)
    split;
    path_functor;
    [ (exists (path_forall _ _ helper1))
    | (exists (path_forall _ _ helper2)) ];
    unfold helper1, helper2, helper2_helper;
    exp_laws_t.
  Qed.
End Law4.