(** * Exponential laws about products and sums in exponents *)
Require Import Functor.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Category.Sum Functor.Sum.
Require Import Functor.Paths.
Require Import Functor.Identity Functor.Composition.Core.
Require Import Types.Prod ExponentialLaws.Tactics.
Require Import ExponentialLaws.Law2.Functors.

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

Local Open Scope functor_scope.

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



  Lemma helper1 (c : Functor C1 D * Functor C2 D)
  : ((1 o (Basics.Overture.fst c + Basics.Overture.snd c) o inl C1 C2)%functor,
     (1 o (Basics.Overture.fst c + Basics.Overture.snd c) o inr C1 C2)%functor)%core = c.
H: Funext
D, C1, C2: PreCategory
c: Functor C1 D * Functor C2 D
(1 o (fst c + snd c) o inl C1 C2,
1 o (fst c + snd c) o inr C1 C2) = c
  Proof.
H: Funext
D, C1, C2: PreCategory
c: Functor C1 D * Functor C2 D
(1 o (fst c + snd c) o inl C1 C2,
1 o (fst c + snd c) o inr C1 C2) = c
    apply path_prod; simpl;
    path_functor.
  Defined.

  Lemma helper2_helper (c : Functor (C1 + C2) D) x
  : (1 o c o inl C1 C2 + 1 o c o inr C1 C2) x = c x.
H: Funext
D, C1, C2: PreCategory
c: Functor (C1 + C2) D
x: (C1 + C2)%category
((1 o c o inl C1 C2 + 1 o c o inr C1 C2) _0 x)%object =
(c _0 x)%object
  Proof.
H: Funext
D, C1, C2: PreCategory
c: Functor (C1 + C2) D
x: (C1 + C2)%category
((1 o c o inl C1 C2 + 1 o c o inr C1 C2) _0 x)%object =
(c _0 x)%object
    destruct x; reflexivity.
  Defined.

  Lemma helper2 (c : Functor (C1 + C2) D)
  : 1 o c o inl C1 C2 + 1 o c o inr C1 C2 = c.
H: Funext
D, C1, C2: PreCategory
c: Functor (C1 + C2) D
1 o c o inl C1 C2 + 1 o c o inr C1 C2 = c
  Proof.
H: Funext
D, C1, C2: PreCategory
c: Functor (C1 + C2) D
1 o c o inl C1 C2 + 1 o c o inr C1 C2 = c
    path_functor.
H: Funext
D, C1, C2: PreCategory
c: Functor (C1 + C2) D
{HO
: (fun cc' : C1 + C2 =>
   match cc' with
   | Overture.inl c0 =>
       (c _0 (Overture.inl c0))%object
   | Overture.inr c' =>
       (c _0 (Overture.inr c'))%object
   end) = c &
transport
  (fun GO : C1 + C2 -> D =>
   forall s d : C1 + C2,
   match s with
   | Overture.inl s0 =>
       match d with
       | Overture.inl d0 => morphism C1 s0 d0
       | Overture.inr _ => Empty
       end
   | Overture.inr s0 =>
       match d with
       | Overture.inl _ => Empty
       | Overture.inr d0 => morphism C2 s0 d0
       end
   end -> morphism D (GO s) (GO d)) HO
  (fun s d : C1 + C2 =>
   match
     s as s0
     return
       (match s0 with
        | Overture.inl s1 =>
            match d with
            | Overture.inl d0 => morphism C1 s1 d0
            | Overture.inr _ => Empty
            end
        | Overture.inr s1 =>
            match d with
            | Overture.inl _ => Empty
            | Overture.inr d0 => morphism C2 s1 d0
            end
        end ->
        morphism D
          match s0 with
          | Overture.inl c0 =>
              (c _0 (Overture.inl c0))%object
          | Overture.inr c' =>
              (c _0 (Overture.inr c'))%object
          end
          match d with
          | Overture.inl c0 =>
              (c _0 (Overture.inl c0))%object
          | Overture.inr c' =>
              (c _0 (Overture.inr c'))%object
          end)
   with
   | Overture.inl cs =>
       match
         d as d0
         return
           (match d0 with
            | Overture.inl d1 => morphism C1 cs d1
            | Overture.inr _ => Empty
            end ->
            morphism D (c _0 (Overture.inl cs))%object
              match d0 with
              | Overture.inl c0 =>
                  (c _0 (Overture.inl c0))%object
              | Overture.inr c' =>
                  (c _0 (Overture.inr c'))%object
              end)
       with
       | Overture.inl cd =>
           fun m : morphism C1 cs cd =>
           (c _1 m)%morphism
       | Overture.inr o =>
           fun m : Empty =>
           match
             m
             return
               (morphism D
                  (c _0 (Overture.inl cs))%object
                  (c _0 (Overture.inr o))%object)
           with
           end
       end
   | Overture.inr c's =>
       match
         d as d0
         return
           (match d0 with
            | Overture.inl _ => Empty
            | Overture.inr d1 => morphism C2 c's d1
            end ->
            morphism D
              (c _0 (Overture.inr c's))%object
              match d0 with
              | Overture.inl c0 =>
                  (c _0 (Overture.inl c0))%object
              | Overture.inr c' =>
                  (c _0 (Overture.inr c'))%object
              end)
       with
       | Overture.inl o =>
           fun m : Empty =>
           match
             m
             return
               (morphism D
                  (c _0 (Overture.inr c's))%object
                  (c _0 (Overture.inl o))%object)
           with
           end
       | Overture.inr c'd =>
           fun m : morphism C2 c's c'd =>
           (c _1 m)%morphism
       end
   end) = morphism_of c}
    (exists (path_forall _ _ (@helper2_helper c))).
H: Funext
D, C1, C2: PreCategory
c: Functor (C1 + C2) D
transport
  (fun GO : C1 + C2 -> D =>
   forall s d : C1 + C2,
   match s with
   | Overture.inl s0 =>
       match d with
       | Overture.inl d0 => morphism C1 s0 d0
       | Overture.inr _ => Empty
       end
   | Overture.inr s0 =>
       match d with
       | Overture.inl _ => Empty
       | Overture.inr d0 => morphism C2 s0 d0
       end
   end -> morphism D (GO s) (GO d))
  (path_forall (1 o c o inl C1 C2 + 1 o c o inr C1 C2)
     c (helper2_helper c))
  (fun s d : C1 + C2 =>
   match
     s as s0
     return
       (match s0 with
        | Overture.inl s1 =>
            match d with
            | Overture.inl d0 => morphism C1 s1 d0
            | Overture.inr _ => Empty
            end
        | Overture.inr s1 =>
            match d with
            | Overture.inl _ => Empty
            | Overture.inr d0 => morphism C2 s1 d0
            end
        end ->
        morphism D
          match s0 with
          | Overture.inl c0 =>
              (c _0 (Overture.inl c0))%object
          | Overture.inr c' =>
              (c _0 (Overture.inr c'))%object
          end
          match d with
          | Overture.inl c0 =>
              (c _0 (Overture.inl c0))%object
          | Overture.inr c' =>
              (c _0 (Overture.inr c'))%object
          end)
   with
   | Overture.inl cs =>
       match
         d as d0
         return
           (match d0 with
            | Overture.inl d1 => morphism C1 cs d1
            | Overture.inr _ => Empty
            end ->
            morphism D (c _0 (Overture.inl cs))%object
              match d0 with
              | Overture.inl c0 =>
                  (c _0 (Overture.inl c0))%object
              | Overture.inr c' =>
                  (c _0 (Overture.inr c'))%object
              end)
       with
       | Overture.inl cd =>
           fun m : morphism C1 cs cd =>
           (c _1 m)%morphism
       | Overture.inr o =>
           fun m : Empty =>
           match
             m
             return
               (morphism D
                  (c _0 (Overture.inl cs))%object
                  (c _0 (Overture.inr o))%object)
           with
           end
       end
   | Overture.inr c's =>
       match
         d as d0
         return
           (match d0 with
            | Overture.inl _ => Empty
            | Overture.inr d1 => morphism C2 c's d1
            end ->
            morphism D
              (c _0 (Overture.inr c's))%object
              match d0 with
              | Overture.inl c0 =>
                  (c _0 (Overture.inl c0))%object
              | Overture.inr c' =>
                  (c _0 (Overture.inr c'))%object
              end)
       with
       | Overture.inl o =>
           fun m : Empty =>
           match
             m
             return
               (morphism D
                  (c _0 (Overture.inr c's))%object
                  (c _0 (Overture.inl o))%object)
           with
           end
       | Overture.inr c'd =>
           fun m : morphism C2 c's c'd =>
           (c _1 m)%morphism
       end
   end) = morphism_of c
    abstract exp_laws_t.
  Defined.

  Lemma law
  : functor D C1 C2 o inverse D C1 C2 = 1
    /\ inverse D C1 C2 o functor D C1 C2 = 1.
H: Funext
D, C1, C2: PreCategory
(functor D C1 C2 o inverse D C1 C2 = 1) *
(inverse D C1 C2 o functor D C1 C2 = 1)
  Proof.
H: Funext
D, C1, C2: PreCategory
(functor D C1 C2 o inverse D C1 C2 = 1) *
(inverse D C1 C2 o functor D C1 C2 = 1)
    split;
    path_functor;
    [ (exists (path_forall _ _ helper1))
    | (exists (path_forall _ _ helper2)) ];
    exp_laws_t;
    unfold helper1, helper2;
    exp_laws_t.
  Qed.
End Law2.