From Tealeaves.Classes Require Export
  Functor
  Categorical.Applicative
  Monoid.

Import Monoid.Notations.

(** * Cartesian Product of Functors *)
(**********************************************************************)
Inductive ProductFunctor (G1 G2: Type -> Type) (A: Type) :=
| product: G1 A -> G2 A -> ProductFunctor G1 G2 A.

#[global] Arguments product {G1 G2}%function_scope {A}%type_scope _ _.

#[local] Notation "G1 ◻ G2" :=
  (ProductFunctor G1 G2) (at level 50): tealeaves_scope.

Definition pi1 {F G A}: (F ◻ G) A -> F A :=
  fun '(product x _) => x.

Definition pi2 {F G A}: (F ◻ G) A -> G A :=
  fun '(product _ y) => y.

Theorem product_eta G1 G2 A: forall (x: (G1 ◻ G2) A),
    x = product (pi1 x) (pi2 x).
G1, G2: Type -> Type
A: Type
forall x : (G1 ◻ G2) A, x = product (pi1 x) (pi2 x)
Proof.
G1, G2: Type -> Type
A: Type
forall x : (G1 ◻ G2) A, x = product (pi1 x) (pi2 x)
  intros.
G1, G2: Type -> Type
A: Type
x: (G1 ◻ G2) A
x = product (pi1 x) (pi2 x) now destruct x.
Qed.

(** ** Functor Instance *)
(**********************************************************************)
#[export] Instance Map_Product (F G: Type -> Type)
  `{Map F} `{Map G}: Map (F ◻ G) :=
  fun A B (f: A -> B) (p: (F ◻ G) A) =>
    match p with product x y => product (map f x) (map f y)
    end.

#[export] Instance Functor_Product
  (F G: Type -> Type) `{Functor F} `{Functor G}: Functor (F ◻ G).
F, G: Type -> Type
Map_F: Map F
H: Functor F
Map_F0: Map G
H0: Functor G
Functor (F ◻ G)
Proof.
F, G: Type -> Type
Map_F: Map F
H: Functor F
Map_F0: Map G
H0: Functor G
Functor (F ◻ G)
  constructor.
F, G: Type -> Type
Map_F: Map F
H: Functor F
Map_F0: Map G
H0: Functor G
forall A : Type, map id = id
F, G: Type -> Type
Map_F: Map F
H: Functor F
Map_F0: Map G
H0: Functor G
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
  -
F, G: Type -> Type
Map_F: Map F
H: Functor F
Map_F0: Map G
H0: Functor G
forall A : Type, map id = id introv.
F, G: Type -> Type
Map_F: Map F
H: Functor F
Map_F0: Map G
H0: Functor G
A: Type
map id = id ext [?].
F, G: Type -> Type
Map_F: Map F
H: Functor F
Map_F0: Map G
H0: Functor G
A: Type
f: F A
g: G A
map id (product f g) = id (product f g) cbn.
F, G: Type -> Type
Map_F: Map F
H: Functor F
Map_F0: Map G
H0: Functor G
A: Type
f: F A
g: G A
product (map id f) (map id g) = id (product f g) now rewrite 2(fun_map_id _).
  -
F, G: Type -> Type
Map_F: Map F
H: Functor F
Map_F0: Map G
H0: Functor G
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f) introv.
F, G: Type -> Type
Map_F: Map F
H: Functor F
Map_F0: Map G
H0: Functor G
A, B, C: Type
f: A -> B
g: B -> C
map g ∘ map f = map (g ∘ f) ext [?].
F, G: Type -> Type
Map_F: Map F
H: Functor F
Map_F0: Map G
H0: Functor G
A, B, C: Type
f: A -> B
g: B -> C
f0: F A
g0: G A
(map g ∘ map f) (product f0 g0) =
map (g ∘ f) (product f0 g0) cbn.
F, G: Type -> Type
Map_F: Map F
H: Functor F
Map_F0: Map G
H0: Functor G
A, B, C: Type
f: A -> B
g: B -> C
f0: F A
g0: G A
product (map g (map f f0)) (map g (map f g0)) =
product (map (g ∘ f) f0) (map (g ∘ f) g0) now rewrite <- 2(fun_map_map _).
Qed.

(** * Applicative Functor Instance *)
(**********************************************************************)

(** ** Operations *)
(**********************************************************************)
#[export] Instance Pure_Product (F G: Type -> Type)
  `{Pure F} `{Pure G}: Pure (F ◻ G) :=
  fun A (a: A) => product (pure a) (pure a).

#[export] Instance Mult_Product (F G: Type -> Type)
  `{Mult F} `{Mult G}: Mult (F ◻ G) :=
  fun A B (p: (F ◻ G) A * (F ◻ G) B) =>
    match p with
    | (product fa ga , product fb gb) =>
        product (mult (fa, fb)) (mult (ga, gb))
    end.

(** ** Applicative Laws *)
(**********************************************************************)
Section product_applicative.

  Context
    (F G: Type -> Type)
    `{Applicative F}
    `{Applicative G}.

  #[export] Instance Applicative_Product: Applicative (F ◻ G).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
Applicative (F ◻ G)
  Proof.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
Applicative (F ◻ G)
    constructor; try typeclasses eauto.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B : Type) (f : A -> B) (x : A),
map f (pure x) = pure (f x)
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B C D : Type) 
  (f : A -> C) (g : B -> D) 
  (x : (F ◻ G) A) (y : (F ◻ G) B),
mult (map f x, map g y) =
map (map_tensor f g) (mult (x, y))
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B C : Type) (x : (F ◻ G) A) 
  (y : (F ◻ G) B) (z : (F ◻ G) C),
map associator (mult (mult (x, y), z)) =
mult (x, mult (y, z))
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A : Type) (x : (F ◻ G) A),
map left_unitor (mult (pure tt, x)) = x
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A : Type) (x : (F ◻ G) A),
map right_unitor (mult (x, pure tt)) = x
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
    -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B : Type) (f : A -> B) (x : A),
map f (pure x) = pure (f x) introv.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B: Type
f: A -> B
x: A
map f (pure x) = pure (f x) cbn.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B: Type
f: A -> B
x: A
product (map f (pure x)) (map f (pure x)) = pure (f x) now rewrite 2(app_pure_natural _).
    -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B C D : Type) (f : A -> C) (g : B -> D)
  (x : (F ◻ G) A) (y : (F ◻ G) B),
mult (map f x, map g y) =
map (map_tensor f g) (mult (x, y)) introv.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B, C, D: Type
f: A -> C
g: B -> D
x: (F ◻ G) A
y: (F ◻ G) B
mult (map f x, map g y) =
map (map_tensor f g) (mult (x, y)) unfold transparent tcs.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B, C, D: Type
f: A -> C
g: B -> D
x: (F ◻ G) A
y: (F ◻ G) B
(let (p0, p1) :=
   (match x with
    | product x y => product (map f x) (map f y)
    end,
    match y with
    | product x y => product (map g x) (map g y)
    end) in
 match p0 with
 | product fa ga =>
     match p1 with
     | product fb gb =>
         product (mult (fa, fb)) (mult (ga, gb))
     end
 end) =
match
  (let (p0, p1) := (x, y) in
   match p0 with
   | product fa ga =>
       match p1 with
       | product fb gb =>
           product (mult (fa, fb)) (mult (ga, gb))
       end
   end)
with
| product x y =>
    product (map (map_tensor f g) x)
      (map (map_tensor f g) y)
end destruct x, y.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B, C, D: Type
f: A -> C
g: B -> D
f0: F A
g0: G A
f1: F B
g1: G B
product (mult (map f f0, map g f1))
  (mult (map f g0, map g g1)) =
product (map (map_tensor f g) (mult (f0, f1)))
  (map (map_tensor f g) (mult (g0, g1)))
      now rewrite 2(app_mult_natural _).
    -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B C : Type) (x : (F ◻ G) A) (y : (F ◻ G) B)
  (z : (F ◻ G) C),
map associator (mult (mult (x, y), z)) =
mult (x, mult (y, z)) introv.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B, C: Type
x: (F ◻ G) A
y: (F ◻ G) B
z: (F ◻ G) C
map associator (mult (mult (x, y), z)) =
mult (x, mult (y, z)) unfold transparent tcs.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B, C: Type
x: (F ◻ G) A
y: (F ◻ G) B
z: (F ◻ G) C
match
  (let (p0, p1) :=
     (let (p0, p1) := (x, y) in
      match p0 with
      | product fa ga =>
          match p1 with
          | product fb gb =>
              product (mult (fa, fb)) (mult (ga, gb))
          end
      end, z) in
   match p0 with
   | product fa ga =>
       match p1 with
       | product fb gb =>
           product (mult (fa, fb)) (mult (ga, gb))
       end
   end)
with
| product x y =>
    product (map associator x) (map associator y)
end =
(let (p0, p1) :=
   (x,
    let (p0, p1) := (y, z) in
    match p0 with
    | product fa ga =>
        match p1 with
        | product fb gb =>
            product (mult (fa, fb)) (mult (ga, gb))
        end
    end) in
 match p0 with
 | product fa ga =>
     match p1 with
     | product fb gb =>
         product (mult (fa, fb)) (mult (ga, gb))
     end
 end) destruct x, y, z.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B, C: Type
f: F A
g: G A
f0: F B
g0: G B
f1: F C
g1: G C
product (map associator (mult (mult (f, f0), f1)))
  (map associator (mult (mult (g, g0), g1))) =
product (mult (f, mult (f0, f1)))
  (mult (g, mult (g0, g1)))
      now rewrite 2(app_assoc _).
    -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A : Type) (x : (F ◻ G) A),
map left_unitor (mult (pure tt, x)) = x introv.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A: Type
x: (F ◻ G) A
map left_unitor (mult (pure tt, x)) = x unfold transparent tcs.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A: Type
x: (F ◻ G) A
match
  (let (p0, p1) := (product (pure tt) (pure tt), x) in
   match p0 with
   | product fa ga =>
       match p1 with
       | product fb gb =>
           product (mult (fa, fb)) (mult (ga, gb))
       end
   end)
with
| product x y =>
    product (map left_unitor x) (map left_unitor y)
end = x destruct x.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A: Type
f: F A
g: G A
product (map left_unitor (mult (pure tt, f)))
  (map left_unitor (mult (pure tt, g))) = product f g
      now rewrite 2(app_unital_l _).
    -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A : Type) (x : (F ◻ G) A),
map right_unitor (mult (x, pure tt)) = x introv.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A: Type
x: (F ◻ G) A
map right_unitor (mult (x, pure tt)) = x unfold transparent tcs.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A: Type
x: (F ◻ G) A
match
  (let (p0, p1) := (x, product (pure tt) (pure tt)) in
   match p0 with
   | product fa ga =>
       match p1 with
       | product fb gb =>
           product (mult (fa, fb)) (mult (ga, gb))
       end
   end)
with
| product x y =>
    product (map right_unitor x) (map right_unitor y)
end = x destruct x.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A: Type
f: F A
g: G A
product (map right_unitor (mult (f, pure tt)))
  (map right_unitor (mult (g, pure tt))) = product f g
      now rewrite 2(app_unital_r _).
    -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b) introv.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B: Type
a: A
b: B
mult (pure a, pure b) = pure (a, b) unfold transparent tcs.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B: Type
a: A
b: B
(let (p0, p1) :=
   (product (pure a) (pure a),
    product (pure b) (pure b)) in
 match p0 with
 | product fa ga =>
     match p1 with
     | product fb gb =>
         product (mult (fa, fb)) (mult (ga, gb))
     end
 end) = product (pure (a, b)) (pure (a, b)) cbn.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B: Type
a: A
b: B
product (mult (pure a, pure b))
  (mult (pure a, pure b)) =
product (pure (a, b)) (pure (a, b))
      now rewrite 2(app_mult_pure _).
  Qed.

End product_applicative.

(** ** Projections as Applicative Homomorphisms *)
(**********************************************************************)
Theorem ApplicativeMorphism_pi1
  (F G: Type -> Type)
  `{Applicative F}
  `{Applicative G}
 : ApplicativeMorphism (F ◻ G) F (@pi1 _ _).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
ApplicativeMorphism (F ◻ G) F (@pi1 F G)
Proof.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
ApplicativeMorphism (F ◻ G) F (@pi1 F G)
  intros.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
ApplicativeMorphism (F ◻ G) F (@pi1 F G) constructor; try typeclasses eauto.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B : Type) (f : A -> B) (x : (F ◻ G) A),
pi1 (map f x) = map f (pi1 x)
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A : Type) (a : A), pi1 (pure a) = pure a
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B : Type) (x : (F ◻ G) A) (y : (F ◻ G) B),
pi1 (mult (x, y)) = mult (pi1 x, pi1 y)
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B : Type) (f : A -> B) (x : (F ◻ G) A),
pi1 (map f x) = map f (pi1 x) intros.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B: Type
f: A -> B
x: (F ◻ G) A
pi1 (map f x) = map f (pi1 x) now destruct x.
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A : Type) (a : A), pi1 (pure a) = pure a intros.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A: Type
a: A
pi1 (pure a) = pure a reflexivity.
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B : Type) (x : (F ◻ G) A) (y : (F ◻ G) B),
pi1 (mult (x, y)) = mult (pi1 x, pi1 y) intros.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B: Type
x: (F ◻ G) A
y: (F ◻ G) B
pi1 (mult (x, y)) = mult (pi1 x, pi1 y) now destruct x, y.
Qed.

Theorem ApplicativeMorphism_pi2
  (F G: Type -> Type)
  `{Applicative F}
  `{Applicative G}
 : ApplicativeMorphism (F ◻ G) G (@pi2 _ _).
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
ApplicativeMorphism (F ◻ G) G (@pi2 F G)
Proof.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
ApplicativeMorphism (F ◻ G) G (@pi2 F G)
  intros.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
ApplicativeMorphism (F ◻ G) G (@pi2 F G) constructor; try typeclasses eauto.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B : Type) (f : A -> B) (x : (F ◻ G) A),
pi2 (map f x) = map f (pi2 x)
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A : Type) (a : A), pi2 (pure a) = pure a
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B : Type) (x : (F ◻ G) A) (y : (F ◻ G) B),
pi2 (mult (x, y)) = mult (pi2 x, pi2 y)
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B : Type) (f : A -> B) (x : (F ◻ G) A),
pi2 (map f x) = map f (pi2 x) intros.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B: Type
f: A -> B
x: (F ◻ G) A
pi2 (map f x) = map f (pi2 x) now destruct x.
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A : Type) (a : A), pi2 (pure a) = pure a intros.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A: Type
a: A
pi2 (pure a) = pure a reflexivity.
  -
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
forall (A B : Type) (x : (F ◻ G) A) (y : (F ◻ G) B),
pi2 (mult (x, y)) = mult (pi2 x, pi2 y) intros.
F, G: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Map_G0: Map G
Pure_G0: Pure G
Mult_G0: Mult G
H0: Applicative G
A, B: Type
x: (F ◻ G) A
y: (F ◻ G) B
pi2 (mult (x, y)) = mult (pi2 x, pi2 y) now destruct x, y.
Qed.

(** ** Parallel Composition of Applicative Homomorphisms *)
(**********************************************************************)
Theorem ApplicativeMorphism_product
  (F1 F2 G1 G2: Type -> Type)
  `{Applicative F1}
  `{Applicative F2}
  `{Applicative G1}
  `{Applicative G2}
  ϕ1 ϕ2
  `{! ApplicativeMorphism F1 G1 ϕ1}
  `{! ApplicativeMorphism F2 G2 ϕ2}:
  ApplicativeMorphism (F1 ◻ F2) (G1 ◻ G2)
    (fun A '(product f1 f2) => product (ϕ1 A f1) (ϕ2 A f2)).
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
ApplicativeMorphism (F1 ◻ F2) (G1 ◻ G2)
  (fun (A : Type) '(product f1 f2) =>
   product (ϕ1 A f1) (ϕ2 A f2))
Proof.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
ApplicativeMorphism (F1 ◻ F2) (G1 ◻ G2)
  (fun (A : Type) '(product f1 f2) =>
   product (ϕ1 A f1) (ϕ2 A f2))
  intros.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
ApplicativeMorphism (F1 ◻ F2) (G1 ◻ G2)
  (fun (A : Type) '(product f1 f2) =>
   product (ϕ1 A f1) (ϕ2 A f2)) inversion ApplicativeMorphism0.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
ApplicativeMorphism (F1 ◻ F2) (G1 ◻ G2)
  (fun (A : Type) '(product f1 f2) =>
   product (ϕ1 A f1) (ϕ2 A f2))
  inversion ApplicativeMorphism1.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
ApplicativeMorphism (F1 ◻ F2) (G1 ◻ G2)
  (fun (A : Type) '(product f1 f2) =>
   product (ϕ1 A f1) (ϕ2 A f2))
  constructor; try typeclasses eauto.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
forall (A B : Type) (f : A -> B) (x : (F1 ◻ F2) A),
(let
 'product f1 f2 := map f x in
  product (ϕ1 B f1) (ϕ2 B f2)) =
map f
  (let
   'product f1 f2 := x in product (ϕ1 A f1) (ϕ2 A f2))
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
forall (A : Type) (a : A),
(let
 'product f1 f2 := pure a in
  product (ϕ1 A f1) (ϕ2 A f2)) = 
pure a
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
forall (A B : Type) (x : (F1 ◻ F2) A)
  (y : (F1 ◻ F2) B),
(let
 'product f1 f2 := mult (x, y) in
  product (ϕ1 (A * B) f1) (ϕ2 (A * B) f2)) =
mult
  (let
   'product f1 f2 := x in product (ϕ1 A f1) (ϕ2 A f2),
   let
   'product f1 f2 := y in product (ϕ1 B f1) (ϕ2 B f2))
  -
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
forall (A B : Type) (f : A -> B) (x : (F1 ◻ F2) A),
(let
 'product f1 f2 := map f x in
  product (ϕ1 B f1) (ϕ2 B f2)) =
map f
  (let
   'product f1 f2 := x in product (ϕ1 A f1) (ϕ2 A f2)) intros.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A, B: Type
f: A -> B
x: (F1 ◻ F2) A
(let
 'product f1 f2 := map f x in
  product (ϕ1 B f1) (ϕ2 B f2)) =
map f
  (let
   'product f1 f2 := x in product (ϕ1 A f1) (ϕ2 A f2)) destruct x.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A, B: Type
f: A -> B
f0: F1 A
f1: F2 A
(let
 'product f1 f2 := map f (product f0 f1) in
  product (ϕ1 B f1) (ϕ2 B f2)) =
map f (product (ϕ1 A f0) (ϕ2 A f1)) cbn.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A, B: Type
f: A -> B
f0: F1 A
f1: F2 A
product (ϕ1 B (map f f0)) (ϕ2 B (map f f1)) =
product (map f (ϕ1 A f0)) (map f (ϕ2 A f1))
    rewrite appmor_natural.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A, B: Type
f: A -> B
f0: F1 A
f1: F2 A
product (map f (ϕ1 A f0)) (ϕ2 B (map f f1)) =
product (map f (ϕ1 A f0)) (map f (ϕ2 A f1))
    rewrite appmor_natural0.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A, B: Type
f: A -> B
f0: F1 A
f1: F2 A
product (map f (ϕ1 A f0)) (map f (ϕ2 A f1)) =
product (map f (ϕ1 A f0)) (map f (ϕ2 A f1))
    reflexivity.
  -
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
forall (A : Type) (a : A),
(let
 'product f1 f2 := pure a in
  product (ϕ1 A f1) (ϕ2 A f2)) = pure a intros.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A: Type
a: A
(let
 'product f1 f2 := pure a in
  product (ϕ1 A f1) (ϕ2 A f2)) = pure a cbn.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A: Type
a: A
product (ϕ1 A (pure a)) (ϕ2 A (pure a)) = pure a
    rewrite appmor_pure.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A: Type
a: A
product (pure a) (ϕ2 A (pure a)) = pure a
    rewrite appmor_pure0.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A: Type
a: A
product (pure a) (pure a) = pure a
    reflexivity.
  -
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
forall (A B : Type) (x : (F1 ◻ F2) A)
  (y : (F1 ◻ F2) B),
(let
 'product f1 f2 := mult (x, y) in
  product (ϕ1 (A * B) f1) (ϕ2 (A * B) f2)) =
mult
  (let
   'product f1 f2 := x in product (ϕ1 A f1) (ϕ2 A f2),
   let
   'product f1 f2 := y in product (ϕ1 B f1) (ϕ2 B f2)) intros.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A, B: Type
x: (F1 ◻ F2) A
y: (F1 ◻ F2) B
(let
 'product f1 f2 := mult (x, y) in
  product (ϕ1 (A * B) f1) (ϕ2 (A * B) f2)) =
mult
  (let
   'product f1 f2 := x in product (ϕ1 A f1) (ϕ2 A f2),
   let
   'product f1 f2 := y in product (ϕ1 B f1) (ϕ2 B f2)) destruct x; destruct y.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A, B: Type
f: F1 A
f0: F2 A
f1: F1 B
f2: F2 B
(let
 'product f1 f2 := mult (product f f0, product f1 f2)
  in product (ϕ1 (A * B) f1) (ϕ2 (A * B) f2)) =
mult
  (product (ϕ1 A f) (ϕ2 A f0),
   product (ϕ1 B f1) (ϕ2 B f2)) cbn.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A, B: Type
f: F1 A
f0: F2 A
f1: F1 B
f2: F2 B
product (ϕ1 (A * B) (mult (f, f1)))
  (ϕ2 (A * B) (mult (f0, f2))) =
product (mult (ϕ1 A f, ϕ1 B f1))
  (mult (ϕ2 A f0, ϕ2 B f2))
    rewrite appmor_mult.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A, B: Type
f: F1 A
f0: F2 A
f1: F1 B
f2: F2 B
product (mult (ϕ1 A f, ϕ1 B f1))
  (ϕ2 (A * B) (mult (f0, f2))) =
product (mult (ϕ1 A f, ϕ1 B f1))
  (mult (ϕ2 A f0, ϕ2 B f2))
    rewrite appmor_mult0.
F1, F2, G1, G2: Type -> Type
Map_G: Map F1
Pure_G: Pure F1
Mult_G: Mult F1
H: Applicative F1
Map_G0: Map F2
Pure_G0: Pure F2
Mult_G0: Mult F2
H0: Applicative F2
Map_G1: Map G1
Pure_G1: Pure G1
Mult_G1: Mult G1
H1: Applicative G1
Map_G2: Map G2
Pure_G2: Pure G2
Mult_G2: Mult G2
H2: Applicative G2
ϕ1: forall A : Type, F1 A -> G1 A
ϕ2: forall A : Type, F2 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism F1 G1 ϕ1
ApplicativeMorphism1: ApplicativeMorphism F2 G2 ϕ2
appmor_app_F: Applicative F1
appmor_app_G: Applicative G1
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : F1 A),
ϕ1 B (map f x) = map f (ϕ1 A x)
appmor_pure: forall (A : Type) (a : A),
ϕ1 A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : F1 A)
  (y : F1 B),
ϕ1 (A * B) (mult (x, y)) =
mult (ϕ1 A x, ϕ1 B y)
appmor_app_F0: Applicative F2
appmor_app_G0: Applicative G2
appmor_natural0: forall (A B : Type) (f : A -> B)
  (x : F2 A),
ϕ2 B (map f x) = map f (ϕ2 A x)
appmor_pure0: forall (A : Type) (a : A),
ϕ2 A (pure a) = pure a
appmor_mult0: forall (A B : Type) (x : F2 A)
  (y : F2 B),
ϕ2 (A * B) (mult (x, y)) =
mult (ϕ2 A x, ϕ2 B y)
A, B: Type
f: F1 A
f0: F2 A
f1: F1 B
f2: F2 B
product (mult (ϕ1 A f, ϕ1 B f1))
  (mult (ϕ2 A f0, ϕ2 B f2)) =
product (mult (ϕ1 A f, ϕ1 B f1))
  (mult (ϕ2 A f0, ϕ2 B f2))
    reflexivity.
Qed.

(** * Notations *)
(**********************************************************************)
Module Notations.
  Notation "F ◻ G" :=
    (ProductFunctor F G) (at level 50): tealeaves_scope.
End Notations.