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

Import Batch.Notations.
Import Monoid.Notations.
Import Applicative.Notations.
Import Product.Notations.
Import DecoratedTraversableMonad.Notations.

#[local] Generalizable Variables U W T G ϕ.

#[local] Arguments batch {A} (B)%type_scope _.


(** * Coalgebraic DTMsto Kleisli DTM *)
(**********************************************************************)

(** ** Derived Operation *)
(**********************************************************************)
#[export] Instance Binddt_ToBatch7
  (W: Type) (T: Type -> Type) `{ToBatch7 W T U}: Binddt W T U :=
  fun F _ _ _ A B f => runBatch f (C := U B) ∘ toBatch7.

Section with_algebra.

  Context
    `{Coalgebraic.DecoratedTraversableMonad.DecoratedTraversableMonad W T}.

  (** ** <<⋆7>> as <<runBatch ∘ map runBatch ∘ double_batch7>> *)
  (********************************************************************)
  Lemma kc7_spec:
    forall (G1 G2: Type -> Type)
      `{Applicative G1}
      `{Applicative G2},
    forall (A B C: Type)
      (g: W * B -> G2 (T C)) (f: W * A -> G1 (T B)),
      g ⋆7 f =
        runBatch (G := G1) f (C := G2 (T C)) ∘
          map (F := Batch (W * A) (T B))
          (runBatch (G := G2) g (C := T C)) ∘
          double_batch7.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
forall (G1 G2 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (Map_G0 : Map G2) (Pure_G0 : Pure G2)
  (Mult_G0 : Mult G2),
Applicative G2 ->
forall (A B C : Type) (g : W * B -> G2 (T C))
  (f : W * A -> G1 (T B)),
g ⋆7 f = runBatch f ∘ map (runBatch g) ∘ double_batch7
  Proof.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
forall (G1 G2 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (Map_G0 : Map G2) (Pure_G0 : Pure G2)
  (Mult_G0 : Mult G2),
Applicative G2 ->
forall (A B C : Type) (g : W * B -> G2 (T C))
  (f : W * A -> G1 (T B)),
g ⋆7 f = runBatch f ∘ map (runBatch g) ∘ double_batch7
    intros.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
g ⋆7 f = runBatch f ∘ map (runBatch g) ∘ double_batch7 ext [w a].
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
(g ⋆7 f) (w, a) =
(runBatch f ∘ map (runBatch g) ∘ double_batch7) (w, a)
    unfold compose.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
(g ⋆7 f) (w, a) =
runBatch f (map (runBatch g) (double_batch7 (w, a)))
    rewrite (double_batch7_rw (w, a)).
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
(g ⋆7 f) (w, a) =
runBatch f
  (map (runBatch g)
     (Done (mapfst_Batch (incr w) ∘ toBatch7) ⧆ (w, a)))
    rewrite map_Batch_rw2.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
(g ⋆7 f) (w, a) =
runBatch f
  (map (compose (runBatch g))
     (Done (mapfst_Batch (incr w) ∘ toBatch7))
   ⧆ (w, a))
    rewrite map_Batch_rw1.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
(g ⋆7 f) (w, a) =
runBatch f
  (Done
     (runBatch g ∘ (mapfst_Batch (incr w) ∘ toBatch7))
   ⧆ (w, a))
    rewrite runBatch_rw2.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
(g ⋆7 f) (w, a) =
runBatch f
  (Done
     (runBatch g ∘ (mapfst_Batch (incr w) ∘ toBatch7))) <⋆>
f (w, a)
    rewrite runBatch_rw1.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
(g ⋆7 f) (w, a) =
pure (runBatch g ∘ (mapfst_Batch (incr w) ∘ toBatch7)) <⋆>
f (w, a)
    rewrite <- (map_to_ap).
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
(g ⋆7 f) (w, a) =
map (runBatch g ∘ (mapfst_Batch (incr w) ∘ toBatch7))
  (f (w, a))
    reassociate <- on right.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
(g ⋆7 f) (w, a) =
map (runBatch g ∘ mapfst_Batch (incr w) ∘ toBatch7)
  (f (w, a))
    rewrite <- runBatch_mapfst'.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
(g ⋆7 f) (w, a) =
map (runBatch (g ∘ incr w) ∘ toBatch7) (f (w, a))
    reflexivity.
  Qed.

  (** ** Derived Laws *)
  (********************************************************************)
  Lemma kdtm_binddt0_T:
    forall (F: Type -> Type) `{Applicative F}
      (A B: Type)
      (f: W * A -> F (T B)),
      binddt f ∘ ret = f ∘ pair Ƶ.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type) (f : W * A -> F (T B)),
binddt f ∘ ret = f ∘ pair Ƶ
  Proof.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type) (f : W * A -> F (T B)),
binddt f ∘ ret = f ∘ pair Ƶ
    intros.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H4: Applicative F
A, B: Type
f: W * A -> F (T B)
binddt f ∘ ret = f ∘ pair Ƶ
    unfold_ops @Binddt_ToBatch7.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H4: Applicative F
A, B: Type
f: W * A -> F (T B)
runBatch f ∘ toBatch7 ∘ ret = f ∘ pair Ƶ
    reassociate -> on left.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H4: Applicative F
A, B: Type
f: W * A -> F (T B)
runBatch f ∘ (toBatch7 ∘ ret) = f ∘ pair Ƶ
    rewrite (dtm_ret (W := W) (T := T)).
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H4: Applicative F
A, B: Type
f: W * A -> F (T B)
runBatch f ∘ (Step (Done id) ∘ ret) = f ∘ pair Ƶ
    unfold compose; ext a.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H4: Applicative F
A, B: Type
f: W * A -> F (T B)
a: A
runBatch f (Done id ⧆ ret a) = f (Ƶ, a)
    rewrite runBatch_rw2.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H4: Applicative F
A, B: Type
f: W * A -> F (T B)
a: A
runBatch f (Done id) <⋆> f (ret a) = f (Ƶ, a)
    rewrite runBatch_rw1.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H4: Applicative F
A, B: Type
f: W * A -> F (T B)
a: A
pure id <⋆> f (ret a) = f (Ƶ, a)
    rewrite ap1.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H4: Applicative F
A, B: Type
f: W * A -> F (T B)
a: A
f (ret a) = f (Ƶ, a)
    reflexivity.
  Qed.

  Lemma kdtm_binddt1_T: forall (A: Type),
      binddt (G := fun A: Type => A)
        (ret (T := T) ∘ extract (W := (W ×))) = @id (T A).
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
forall A : Type, binddt (ret ∘ extract) = id
  Proof.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
forall A : Type, binddt (ret ∘ extract) = id
    intros.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
A: Type
binddt (ret ∘ extract) = id
    unfold_ops @Binddt_ToBatch7.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
A: Type
runBatch (ret ∘ extract) ∘ toBatch7 = id
    rewrite (runBatch_via_traverse (F := fun A => A)).
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
A: Type
map extract_Batch ∘ traverse (ret ∘ extract)
∘ toBatch7 = id
    rewrite <- TraversableFunctor.map_to_traverse.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
A: Type
map extract_Batch ∘ map (ret ∘ extract) ∘ toBatch7 =
id
    apply dtm_extract.
  Qed.

  Lemma kdtm_binddt2_T:
    forall (G1 G2: Type -> Type) (H1: Map G1) (H2: Pure G1) (H5: Mult G1),
      Applicative G1 ->
      forall (H7: Map G2) (H8: Pure G2) (H9: Mult G2),
        Applicative G2 ->
        forall (A B C: Type) (g: W * B -> G2 (T C)) (f: W * A -> G1 (T B)),
          map (F := G1) (binddt g) ∘ binddt f =
            binddt (G := G1 ∘ G2) (g ⋆7 f).
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
forall (G1 G2 : Type -> Type) (H3 : Map G1)
  (H4 : Pure G1) (H5 : Mult G1),
Applicative G1 ->
forall (H7 : Map G2) (H8 : Pure G2) (H9 : Mult G2),
Applicative G2 ->
forall (A B C : Type) (g : W * B -> G2 (T C))
  (f : W * A -> G1 (T B)),
map (binddt g) ∘ binddt f = binddt (g ⋆7 f)
  Proof.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
forall (G1 G2 : Type -> Type) (H3 : Map G1)
  (H4 : Pure G1) (H5 : Mult G1),
Applicative G1 ->
forall (H7 : Map G2) (H8 : Pure G2) (H9 : Mult G2),
Applicative G2 ->
forall (A B C : Type) (g : W * B -> G2 (T C))
  (f : W * A -> G1 (T B)),
map (binddt g) ∘ binddt f = binddt (g ⋆7 f)
    intros.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
map (binddt g) ∘ binddt f = binddt (g ⋆7 f)
    unfold_ops @Binddt_ToBatch7.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
map (runBatch g ∘ toBatch7) ∘ (runBatch f ∘ toBatch7) =
runBatch (g ⋆7 f) ∘ toBatch7
    reassociate <- on left.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
map (runBatch g ∘ toBatch7) ∘ runBatch f ∘ toBatch7 =
runBatch (g ⋆7 f) ∘ toBatch7
    rewrite <- (fun_map_map (F := G1) (Functor := app_functor)).
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
map (runBatch g) ∘ map toBatch7 ∘ runBatch f
∘ toBatch7 = runBatch (g ⋆7 f) ∘ toBatch7
    reassociate -> near (runBatch f).
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
map (runBatch g) ∘ (map toBatch7 ∘ runBatch f)
∘ toBatch7 = runBatch (g ⋆7 f) ∘ toBatch7
    rewrite natural.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
map (runBatch g) ∘ (runBatch f ∘ map toBatch7)
∘ toBatch7 = runBatch (g ⋆7 f) ∘ toBatch7
    reassociate <- on left.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
map (runBatch g) ∘ runBatch f ∘ map toBatch7
∘ toBatch7 = runBatch (g ⋆7 f) ∘ toBatch7
    reassociate -> near toBatch7.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
map (runBatch g) ∘ runBatch f
∘ (map toBatch7 ∘ toBatch7) =
runBatch (g ⋆7 f) ∘ toBatch7
    rewrite <- dtm_duplicate.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
map (runBatch g) ∘ runBatch f
∘ (cojoin_Batch7 ∘ toBatch7) =
runBatch (g ⋆7 f) ∘ toBatch7
    rewrite cojoin_Batch7_to_runBatch.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
map (runBatch g) ∘ runBatch f
∘ (runBatch double_batch7 ∘ toBatch7) =
runBatch (g ⋆7 f) ∘ toBatch7
    reassociate <- on left.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
map (runBatch g) ∘ runBatch f ∘ runBatch double_batch7
∘ toBatch7 = runBatch (g ⋆7 f) ∘ toBatch7
    rewrite natural.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
runBatch f ∘ map (runBatch g) ∘ runBatch double_batch7
∘ toBatch7 = runBatch (g ⋆7 f) ∘ toBatch7
    rewrite (runBatch_morphism'
               (homomorphism :=
                  ApplicativeMorphism_parallel
                    (Batch (W * A) (T B)) (Batch (W * B) (T C)) G1 G2)).
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
runBatch
  (runBatch f ∘ map (runBatch g) ∘ double_batch7)
∘ toBatch7 = runBatch (g ⋆7 f) ∘ toBatch7
    rewrite (kc7_spec G1 G2).
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
H7: Applicative G1
H8: Map G2
H9: Pure G2
H10: Mult G2
H11: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
runBatch
  (runBatch f ∘ map (runBatch g) ∘ double_batch7)
∘ toBatch7 =
runBatch
  (runBatch f ∘ map (runBatch g) ∘ double_batch7)
∘ toBatch7
    reflexivity.
  Qed.

  Lemma kdtm_morph_T:
    forall (G1 G2: Type -> Type) `{morph: ApplicativeMorphism G1 G2 ϕ},
    forall (A B: Type) (f: W * A -> G1 (T B)),
      ϕ (T B) ∘ binddt f = binddt (ϕ (T B) ∘ f).
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
forall (G1 G2 : Type -> Type) (H4 : Map G1)
  (H5 : Mult G1) (H6 : Pure G1) (H7 : Map G2)
  (H8 : Mult G2) (H9 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : W * A -> G1 (T B)),
ϕ (T B) ∘ binddt f = binddt (ϕ (T B) ∘ f)
  Proof.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
forall (G1 G2 : Type -> Type) (H4 : Map G1)
  (H5 : Mult G1) (H6 : Pure G1) (H7 : Map G2)
  (H8 : Mult G2) (H9 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : W * A -> G1 (T B)),
ϕ (T B) ∘ binddt f = binddt (ϕ (T B) ∘ f)
    intros.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
ϕ (T B) ∘ binddt f = binddt (ϕ (T B) ∘ f) ext t.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
t: T A
(ϕ (T B) ∘ binddt f) t = binddt (ϕ (T B) ∘ f) t
    unfold_ops @Binddt_ToBatch7.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
t: T A
(ϕ (T B) ∘ (runBatch f ∘ toBatch7)) t =
(runBatch (ϕ (T B) ∘ f) ∘ toBatch7) t
    reassociate <- on left.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
t: T A
(ϕ (T B) ∘ runBatch f ∘ toBatch7) t =
(runBatch (ϕ (T B) ∘ f) ∘ toBatch7) t
    rewrite runBatch_morphism'.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
t: T A
(runBatch (ϕ (T B) ∘ f) ∘ toBatch7) t =
(runBatch (ϕ (T B) ∘ f) ∘ toBatch7) t
    reflexivity.
  Qed.

  (** ** Typeclass Instances *)
  (********************************************************************)
  #[export] Instance DecoratedTraversableRightPreModule_Kleisli_Coalgebra:
    Classes.Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad W T.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
  Proof.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
    constructor.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
Monoid W
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : W * A -> G (T B)),
binddt f ∘ ret = f ∘ ret
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
DecoratedTraversableRightPreModule W T T
    -
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
Monoid W typeclasses eauto.
    -
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : W * A -> G (T B)),
binddt f ∘ ret = f ∘ ret intros.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H4: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f ∘ ret = f ∘ ret apply (kdtm_binddt0_T G).
    -
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
DecoratedTraversableRightPreModule W T T constructor; intros.
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
A: Type
binddt (ret ∘ extract) = id
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
map (binddt g) ∘ binddt f = binddt (g ⋆7 f)
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
ϕ (T B) ∘ binddt f = binddt (ϕ (T B) ∘ f)
      +
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
A: Type
binddt (ret ∘ extract) = id apply kdtm_binddt1_T.
      +
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
map (binddt g) ∘ binddt f = binddt (g ⋆7 f) apply (kdtm_binddt2_T G1 G2); auto.
      +
W: Type
T: Type -> Type
H: Monoid_op W
H0: Monoid_unit W
H1: Return T
H2: ToBatch7 W T T
H3: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
ϕ (T B) ∘ binddt f = binddt (ϕ (T B) ∘ f) apply kdtm_morph_T; auto.
  Qed.

  #[export] Instance DecoratedTraversableMonad_Kleisli_Coalgebra:
    Classes.Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad W T :=
    {|
      kdtm_binddt0 := kdtm_binddt0_T;
    |}.

End with_algebra.