From Tealeaves Require Export
  Classes.Categorical.Applicative.
  From Tealeaves Require Import
  Classes.Comonoid
  Classes.Kleisli.TraversableFunctor.

Export Comonoid (dup).

Import Applicative.Notations.

(** * Diagonal (Duplication) Applicative Functor *)
(**********************************************************************)
Definition Diagonal (A: Type): Type := A * A.

#[export] Instance Map_Diagonal: Map Diagonal :=
  fun A B f => map_both f: A * A -> B * B.

#[export, program] Instance Functor_Diagonal: Functor Diagonal.

Solve All Obligations with
  (intros; now ext [?]).

(** ** Applicative Functor Instance *)
(**********************************************************************)
#[export] Instance Pure_Diagonal: Pure Diagonal := @dup.

#[export] Instance Mult_Diagonal: Mult Diagonal :=
  fun A B (x: Diagonal A * Diagonal B) =>
    ((fst (fst x), fst (snd x)), (snd (fst x), snd (snd x))).

#[export, program] Instance Applicative_Diagonal: Applicative Diagonal.

Solve Obligations with
  (unfold Diagonal; intros; now destruct_all_pairs).

(** ** Traversable Functor Instance *)
(**********************************************************************)
#[export] Instance Traverse_Diagonal: Traverse (fun A => A * A).
Traverse (fun A : Type => A * A)
Proof.
Traverse (fun A : Type => A * A)
  intros G GMap GPure GMult A B f [a1 a2].
G: Type -> Type
GMap: Map G
GPure: Pure G
GMult: Mult G
A, B: Type
f: A -> G B
a1, a2: A
G (B * B)
  exact (pure pair <⋆> f a1 <⋆> f a2).
Defined.

Lemma traverse_Diagonal_rw {A B: Type} {G}
  `{Map G} `{Mult G} `{Pure G} (f: A -> G B) (a1 a2: A):
  traverse (T := fun A => A * A) f (a1, a2) =
    pure pair <⋆> f a1 <⋆> f a2.
A, B: Type
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
f: A -> G B
a1, a2: A
traverse f (a1, a2) = pure pair <⋆> f a1 <⋆> f a2
Proof.
A, B: Type
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
f: A -> G B
a1, a2: A
traverse f (a1, a2) = pure pair <⋆> f a1 <⋆> f a2
  reflexivity.
Qed.

#[export] Instance TraversableFunctor_Diagonal:
  TraversableFunctor (fun A => A * A).
TraversableFunctor (fun A : Type => A * A)
Proof.
TraversableFunctor (fun A : Type => A * A)
  constructor.
forall A : Type, traverse id = id
forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall (A B C : Type) (g : B -> G2 C) (f : A -> G1 B),
map (traverse g) ∘ traverse f = traverse (kc2 g f)
forall (G1 G2 : Type -> Type) (H : Map G1)
  (H0 : Mult G1) (H1 : Pure G1) (H2 : Map G2)
  (H3 : Mult G2) (H4 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : A -> G1 B),
ϕ (B * B) ∘ traverse f = traverse (ϕ B ∘ f)
  -
forall A : Type, traverse id = id intros.
A: Type
traverse id = id ext [a1 a2].
A: Type
a1, a2: A
traverse id (a1, a2) = id (a1, a2) reflexivity.
  -
forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall (A B C : Type) (g : B -> G2 C) (f : A -> G1 B),
map (traverse g) ∘ traverse f = traverse (kc2 g f) intros.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (traverse g) ∘ traverse f = traverse (kc2 g f) ext [a1 a2].
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
(map (traverse g) ∘ traverse f) (a1, a2) =
traverse (kc2 g f) (a1, a2) unfold compose, kc2.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
map (traverse g) (traverse f (a1, a2)) =
traverse (map g ∘ f) (a1, a2)
    cbn.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
map (traverse g) (pure pair <⋆> f a1 <⋆> f a2) =
pure pair <⋆> (map g ∘ f) a1 <⋆> (map g ∘ f) a2
    do 2 rewrite map_ap.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
map (compose (compose (traverse g))) (pure pair) <⋆>
f a1 <⋆> f a2 =
pure pair <⋆> (map g ∘ f) a1 <⋆> (map g ∘ f) a2
    rewrite app_pure_natural.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
pure pair <⋆> (map g ∘ f) a1 <⋆> (map g ∘ f) a2
    change (fun a => G1 (G2 a)) with (G1 ∘ G2).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
pure pair <⋆> (map g ∘ f) a1 <⋆> (map g ∘ f) a2
    rewrite (ap_compose2 G2 G1).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
map (ap G2) (pure pair <⋆> (map g ∘ f) a1) <⋆>
(map g ∘ f) a2
    rewrite (ap_compose2 G2 G1).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
map (ap G2)
  (map (ap G2) (pure pair) <⋆> (map g ∘ f) a1) <⋆>
(map g ∘ f) a2
    unfold_ops @Pure_compose.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
map (ap G2)
  (map (ap G2) (pure (pure pair)) <⋆> (map g ∘ f) a1) <⋆>
(map g ∘ f) a2
    rewrite app_pure_natural.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
map (ap G2)
  (pure (ap G2 (pure pair)) <⋆> (map g ∘ f) a1) <⋆>
(map g ∘ f) a2
    rewrite map_ap.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
map (compose (ap G2)) (pure (ap G2 (pure pair))) <⋆>
(map g ∘ f) a1 <⋆> (map g ∘ f) a2
    rewrite app_pure_natural.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
pure (ap G2 ∘ ap G2 (pure pair)) <⋆> (map g ∘ f) a1 <⋆>
(map g ∘ f) a2
    unfold compose at 4 5.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
pure (ap G2 ∘ ap G2 (pure pair)) <⋆> map g (f a1) <⋆>
map g (f a2)
    rewrite <- (ap_map).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
map (precompose g)
  (pure (ap G2 ∘ ap G2 (pure pair)) <⋆> map g (f a1)) <⋆>
f a2
    rewrite map_ap.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
map (compose (precompose g))
  (pure (ap G2 ∘ ap G2 (pure pair))) <⋆> 
map g (f a1) <⋆> f a2
    rewrite app_pure_natural.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
pure (precompose g ∘ (ap G2 ∘ ap G2 (pure pair))) <⋆>
map g (f a1) <⋆> f a2
    rewrite <- (ap_map).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
map (precompose g)
  (pure (precompose g ∘ (ap G2 ∘ ap G2 (pure pair)))) <⋆>
f a1 <⋆> f a2
    rewrite app_pure_natural.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
a1, a2: A
pure (compose (traverse g) ∘ pair) <⋆> f a1 <⋆> f a2 =
pure
  (precompose g
     (precompose g ∘ (ap G2 ∘ ap G2 (pure pair)))) <⋆>
f a1 <⋆> f a2
    reflexivity.
  -
forall (G1 G2 : Type -> Type) 
  (H : Map G1) (H0 : Mult G1) 
  (H1 : Pure G1) (H2 : Map G2) 
  (H3 : Mult G2) (H4 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : A -> G1 B),
ϕ (B * B) ∘ traverse f = traverse (ϕ B ∘ f) intros.
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (B * B) ∘ traverse f = traverse (ϕ B ∘ f)
    ext [a1 a2].
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
a1, a2: A
(ϕ (B * B) ∘ traverse f) (a1, a2) =
traverse (ϕ B ∘ f) (a1, a2)
    unfold compose at 1.
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
a1, a2: A
ϕ (B * B) (traverse f (a1, a2)) =
traverse (ϕ B ∘ f) (a1, a2)
    cbn.
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
a1, a2: A
ϕ (B * B) (pure pair <⋆> f a1 <⋆> f a2) =
pure pair <⋆> (ϕ B ∘ f) a1 <⋆> (ϕ B ∘ f) a2
    rewrite ap_morphism_1.
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
a1, a2: A
ϕ (B -> B * B) (pure pair <⋆> f a1) <⋆> ϕ B (f a2) =
pure pair <⋆> (ϕ B ∘ f) a1 <⋆> (ϕ B ∘ f) a2
    rewrite ap_morphism_1.
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
a1, a2: A
ϕ (B -> B -> B * B) (pure pair) <⋆> ϕ B (f a1) <⋆>
ϕ B (f a2) =
pure pair <⋆> (ϕ B ∘ f) a1 <⋆> (ϕ B ∘ f) a2
    rewrite appmor_pure.
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
a1, a2: A
pure pair <⋆> ϕ B (f a1) <⋆> ϕ B (f a2) =
pure pair <⋆> (ϕ B ∘ f) a1 <⋆> (ϕ B ∘ f) a2
    reflexivity.
Qed.