From Tealeaves Require Import
  Functors.Early.Batch
  Classes.Coalgebraic.TraversableFunctor
  Classes.Kleisli.TraversableFunctor.

Import Batch.Notations.
Import Applicative.Notations.
Import Kleisli.TraversableFunctor.Notations.

#[local] Generalizable Variables ϕ T G A B C.

(** * Categorical Traversable Monads from Kleisli Traversable Monads *)
(**********************************************************************)

(** ** Derived Operations *)
(**********************************************************************)
Module DerivedOperations.

  #[export] Instance Traverse_ToBatch
    (T: Type -> Type) `{ToBatch T}: Traverse T :=
  fun G _ _ _ A B f =>
    runBatch (G := G) f (C := T B) ∘ toBatch.

End DerivedOperations.

Module DerivedInstances.

  Import DerivedOperations.

  Context
    `{Coalgebraic.TraversableFunctor.TraversableFunctor T}.

  (** ** <<⋆2>> as <<runBatch ∘ map runBatch ∘ double_batch>> *)
  (********************************************************************)
  Lemma kc2_spec:
    forall `{Applicative G1}
           `{Applicative G2}
           `(g: B -> G2 C) `(f: A -> G1 B),
      g ⋆2 f = runBatch (G := G1) f (C := G2 C) ∘
                 map (F := Batch A B) (runBatch (G := G2) g) ∘
                 double_batch.
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 (B C : Type) (g : B -> G2 C) (A : Type)
  (f : A -> G1 B),
g ⋆2 f = runBatch f ∘ map (runBatch g) ∘ double_batch
  Proof.
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 (B C : Type) (g : B -> G2 C) (A : Type)
  (f : A -> G1 B),
g ⋆2 f = runBatch f ∘ map (runBatch g) ∘ double_batch
    intros.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
B, C: Type
g: B -> G2 C
A: Type
f: A -> G1 B
g ⋆2 f = runBatch f ∘ map (runBatch g) ∘ double_batch
    ext a.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
B, C: Type
g: B -> G2 C
A: Type
f: A -> G1 B
a: A
(g ⋆2 f) a =
(runBatch f ∘ map (runBatch g) ∘ double_batch) a
    unfold compose.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
B, C: Type
g: B -> G2 C
A: Type
f: A -> G1 B
a: A
(g ⋆2 f) a =
runBatch f (map (runBatch g) (double_batch a))
    rewrite double_batch_rw.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
B, C: Type
g: B -> G2 C
A: Type
f: A -> G1 B
a: A
(g ⋆2 f) a =
runBatch f (map (runBatch g) (Done (batch B C) ⧆ a))
    rewrite map_Batch_rw2.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
B, C: Type
g: B -> G2 C
A: Type
f: A -> G1 B
a: A
(g ⋆2 f) a =
runBatch f
  (map (compose (runBatch g)) (Done (batch B C)) ⧆ a)
    rewrite map_Batch_rw1.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
B, C: Type
g: B -> G2 C
A: Type
f: A -> G1 B
a: A
(g ⋆2 f) a =
runBatch f (Done (runBatch g ∘ batch B C) ⧆ a)
    rewrite (runBatch_batch G2).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
B, C: Type
g: B -> G2 C
A: Type
f: A -> G1 B
a: A
(g ⋆2 f) a = runBatch f (Done g ⧆ a)
    rewrite runBatch_rw2.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
B, C: Type
g: B -> G2 C
A: Type
f: A -> G1 B
a: A
(g ⋆2 f) a = runBatch f (Done g) <⋆> f a
    rewrite runBatch_rw1.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
B, C: Type
g: B -> G2 C
A: Type
f: A -> G1 B
a: A
(g ⋆2 f) a = pure g <⋆> f a
    rewrite <- map_to_ap.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
B, C: Type
g: B -> G2 C
A: Type
f: A -> G1 B
a: A
(g ⋆2 f) a = map g (f a)
    reflexivity.
  Qed.

  (** ** Derived Laws *)
(**********************************************************************)
  Lemma traverse_id: forall (A: Type),
      traverse (G := fun A => A) id = @id (T A).
forall A : Type, traverse id = id
  Proof.
forall A : Type, traverse id = id
    intros.
A: Type
traverse id = id
    unfold_ops @Traverse_ToBatch.
A: Type
runBatch id ∘ toBatch = id
    rewrite <- extract_Batch_to_runBatch.
A: Type
extract_Batch ∘ toBatch = id
    rewrite trf_extract.
A: Type
id = id
    reflexivity.
  Qed.

  Lemma traverse_traverse:
    forall `{Applicative G1} `{Applicative G2},
    forall (A B C: Type)
           (g: B -> G2 C) (f: A -> G1 B),
      map (F := G1) (traverse (T := T) g) ∘ traverse (G := G1) f =
        traverse (G := G1 ∘ G2) (kc2 (G1 := G1) (G2 := G2) g f).
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 (g ⋆2 f)
  Proof.
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 (g ⋆2 f)
    intros.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (traverse g) ∘ traverse f = traverse (g ⋆2 f)
    unfold_ops @Traverse_ToBatch.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (runBatch g ∘ toBatch) ∘ (runBatch f ∘ toBatch) =
runBatch (g ⋆2 f) ∘ toBatch
    rewrite <- (fun_map_map (F := G1)).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (runBatch g) ∘ map toBatch
∘ (runBatch f ∘ toBatch) = runBatch (g ⋆2 f) ∘ toBatch
    reassociate -> on left.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (runBatch g)
∘ (map toBatch ∘ (runBatch f ∘ toBatch)) =
runBatch (g ⋆2 f) ∘ toBatch
    reassociate <- near (map (toBatch (A := B) (A' := C))).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (runBatch g)
∘ (map toBatch ∘ runBatch f ∘ toBatch) =
runBatch (g ⋆2 f) ∘ toBatch
    rewrite (natural (ϕ := @runBatch _ _ _ _ _ _ f)).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (runBatch g)
∘ (runBatch f ∘ map toBatch ∘ toBatch) =
runBatch (g ⋆2 f) ∘ toBatch
    reassociate -> on left.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (runBatch g)
∘ (runBatch f ∘ (map toBatch ∘ toBatch)) =
runBatch (g ⋆2 f) ∘ toBatch
    rewrite <- trf_duplicate.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (runBatch g)
∘ (runBatch f ∘ (cojoin_Batch ∘ toBatch)) =
runBatch (g ⋆2 f) ∘ toBatch
    rewrite cojoin_Batch_to_runBatch.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (runBatch g)
∘ (runBatch f ∘ (runBatch double_batch ∘ toBatch)) =
runBatch (g ⋆2 f) ∘ toBatch
    reassociate <- on left.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (runBatch g) ∘ runBatch f
∘ (runBatch double_batch ∘ toBatch) =
runBatch (g ⋆2 f) ∘ toBatch
    reassociate <- on left.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (runBatch g) ∘ runBatch f ∘ runBatch double_batch
∘ toBatch = runBatch (g ⋆2 f) ∘ toBatch
    rewrite (natural (ϕ := @runBatch _ _ _ _ _ _ f)).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
runBatch f ∘ map (runBatch g) ∘ runBatch double_batch
∘ toBatch = runBatch (g ⋆2 f) ∘ toBatch
    rewrite (runBatch_morphism'
               (homomorphism :=
                  ApplicativeMorphism_parallel
                    (Batch A B) (Batch B C) G1 G2)).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
runBatch
  (runBatch f ∘ map (runBatch g) ∘ double_batch)
∘ toBatch = runBatch (g ⋆2 f) ∘ toBatch
    rewrite kc2_spec.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
runBatch
  (runBatch f ∘ map (runBatch g) ∘ double_batch)
∘ toBatch =
runBatch
  (runBatch f ∘ map (runBatch g) ∘ double_batch)
∘ toBatch
    reflexivity.
  Qed.

  Lemma traverse_morphism:
    forall `{morphism: ApplicativeMorphism G1 G2 ϕ}
      (A B: Type) (f: A -> G1 B),
      ϕ (T B) ∘ traverse f = traverse (T := T) (ϕ B ∘ f).
forall (G1 G2 : Type -> Type) (H0 : Map G1)
  (H1 : Mult G1) (H2 : Pure G1) (H3 : Map G2)
  (H4 : Mult G2) (H5 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : A -> G1 B),
ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f)
  Proof.
forall (G1 G2 : Type -> Type) (H0 : Map G1)
  (H1 : Mult G1) (H2 : Pure G1) (H3 : Map G2)
  (H4 : Mult G2) (H5 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : A -> G1 B),
ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f)
    intros.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f)
    unfold_ops @Traverse_ToBatch.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (T B) ∘ (runBatch f ∘ toBatch) =
runBatch (ϕ B ∘ f) ∘ toBatch
    reassociate <- on left.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (T B) ∘ runBatch f ∘ toBatch =
runBatch (ϕ B ∘ f) ∘ toBatch
    rewrite (runBatch_morphism').
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
runBatch (ϕ B ∘ f) ∘ toBatch =
runBatch (ϕ B ∘ f) ∘ toBatch
    reflexivity.
  Qed.

  (** ** Typeclass Instances *)
  (********************************************************************)
  #[export] Instance TraversableFunctor_Kleisli_From_Coalgebraic:
    Kleisli.TraversableFunctor.TraversableFunctor T :=
    {| trf_traverse_id := traverse_id;
       trf_traverse_traverse := @traverse_traverse;
       trf_traverse_morphism := @traverse_morphism;
    |}.

End DerivedInstances.