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

Import Batch.Notations.
Import Applicative.Notations.
Import TraversableMonad.Notations.

#[local] Generalizable Variables T G ϕ.

(** * Kleisli Traversable Monad from Kleisli Traversable Monad *)
(**********************************************************************)

(** ** Derived Operation <<toBatch6>> *)
(**********************************************************************)
Module DerivedOperations.

  #[export] Instance Bindt_ToBatch6
    (T U: Type -> Type) `{ToBatch6 T U}: Bindt T U :=
  fun G _ _ _ A B f => runBatch (G := G) f (C := U B) ∘ toBatch6.

End DerivedOperations.

Module DerivedInstances.

  Import DerivedOperations.

  Section with_algebra.

    Context
      `{Coalgebraic.TraversableMonad.TraversableMonad T}.

    (** ** <<⋆6>> as <<runBatch ∘ map runBatch ∘ double_batch6>> *)
    (******************************************************************)
    Lemma kc6_spec
      {A B C: Type}
      (G1 G2: Type -> Type)
      `{Map G1} `{Pure G1} `{Mult G1} `{! Applicative G1}
      `{Map G2} `{Pure G2} `{Mult G2} `{! Applicative G2}
      (g: B -> G2 (T C))
      (f: A -> G1 (T B)):
      kc6 (G1 := G1) (G2 := G2) g f =
        runBatch f (C := G2 (T C)) ∘
          map (F := Batch A (T B)) (runBatch g)
          ∘ double_batch6.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, B, C: Type
G1, G2: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
Applicative0: Applicative G1
H5: Map G2
H6: Pure G2
H7: Mult G2
Applicative1: Applicative G2
g: B -> G2 (T C)
f: A -> G1 (T B)
g ⋆6 f = runBatch f ∘ map (runBatch g) ∘ double_batch6
    Proof.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, B, C: Type
G1, G2: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
Applicative0: Applicative G1
H5: Map G2
H6: Pure G2
H7: Mult G2
Applicative1: Applicative G2
g: B -> G2 (T C)
f: A -> G1 (T B)
g ⋆6 f = runBatch f ∘ map (runBatch g) ∘ double_batch6
      ext a.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, B, C: Type
G1, G2: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
Applicative0: Applicative G1
H5: Map G2
H6: Pure G2
H7: Mult G2
Applicative1: Applicative G2
g: B -> G2 (T C)
f: A -> G1 (T B)
a: A
(g ⋆6 f) a =
(runBatch f ∘ map (runBatch g) ∘ double_batch6) a
      unfold compose.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, B, C: Type
G1, G2: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
Applicative0: Applicative G1
H5: Map G2
H6: Pure G2
H7: Mult G2
Applicative1: Applicative G2
g: B -> G2 (T C)
f: A -> G1 (T B)
a: A
(g ⋆6 f) a =
runBatch f (map (runBatch g) (double_batch6 a))
      rewrite double_batch6_rw.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, B, C: Type
G1, G2: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
Applicative0: Applicative G1
H5: Map G2
H6: Pure G2
H7: Mult G2
Applicative1: Applicative G2
g: B -> G2 (T C)
f: A -> G1 (T B)
a: A
(g ⋆6 f) a =
runBatch f (map (runBatch g) (Done toBatch6 ⧆ a))
      rewrite map_Batch_rw2.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, B, C: Type
G1, G2: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
Applicative0: Applicative G1
H5: Map G2
H6: Pure G2
H7: Mult G2
Applicative1: Applicative G2
g: B -> G2 (T C)
f: A -> G1 (T B)
a: A
(g ⋆6 f) a =
runBatch f
  (map (compose (runBatch g)) (Done toBatch6) ⧆ a)
      rewrite map_Batch_rw1.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, B, C: Type
G1, G2: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
Applicative0: Applicative G1
H5: Map G2
H6: Pure G2
H7: Mult G2
Applicative1: Applicative G2
g: B -> G2 (T C)
f: A -> G1 (T B)
a: A
(g ⋆6 f) a =
runBatch f (Done (runBatch g ∘ toBatch6) ⧆ a)
      rewrite runBatch_rw2.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, B, C: Type
G1, G2: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
Applicative0: Applicative G1
H5: Map G2
H6: Pure G2
H7: Mult G2
Applicative1: Applicative G2
g: B -> G2 (T C)
f: A -> G1 (T B)
a: A
(g ⋆6 f) a =
runBatch f (Done (runBatch g ∘ toBatch6)) <⋆> f a
      rewrite runBatch_rw1.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, B, C: Type
G1, G2: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
Applicative0: Applicative G1
H5: Map G2
H6: Pure G2
H7: Mult G2
Applicative1: Applicative G2
g: B -> G2 (T C)
f: A -> G1 (T B)
a: A
(g ⋆6 f) a = pure (runBatch g ∘ toBatch6) <⋆> f a
      rewrite <- map_to_ap.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, B, C: Type
G1, G2: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
Applicative0: Applicative G1
H5: Map G2
H6: Pure G2
H7: Mult G2
Applicative1: Applicative G2
g: B -> G2 (T C)
f: A -> G1 (T B)
a: A
(g ⋆6 f) a = map (runBatch g ∘ toBatch6) (f a)
      reflexivity.
    Qed.

    (** ** Derived Laws *)
    (******************************************************************)
    Lemma ktm_bindt0_T:
      forall `{Applicative G} (A B: Type) (f: A -> G (T B)),
        bindt (T := T) (G := G) f ∘ ret = f.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> G (T B)),
bindt f ∘ ret = f
    Proof.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> G (T B)),
bindt f ∘ ret = f
      intros.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A, B: Type
f: A -> G (T B)
bindt f ∘ ret = f
      unfold_ops Bindt_ToBatch6.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A, B: Type
f: A -> G (T B)
runBatch f ∘ toBatch6 ∘ ret = f
      reassociate -> on left.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A, B: Type
f: A -> G (T B)
runBatch f ∘ (toBatch6 ∘ ret) = f
      rewrite trfm_ret.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A, B: Type
f: A -> G (T B)
runBatch f ∘ batch A (T B) = f
      rewrite (runBatch_batch G).
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A, B: Type
f: A -> G (T B)
f = f
      reflexivity.
    Qed.

    Lemma ktm_bindt1_T: forall (A: Type),
        bindt (G := fun A: Type => A) (ret (T := T)) = (@id (T A)).
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
forall A : Type, bindt ret = id
    Proof.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
forall A : Type, bindt ret = id
      intros.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A: Type
bindt ret = id
      unfold_ops Bindt_ToBatch6.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A: Type
runBatch ret ∘ toBatch6 = id
      assert
        (cut:
          runBatch (G := fun A => A) (ret (T := T) (A := A)) (C := T A) =
            extract_Batch ∘ mapfst_Batch ret).
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A: Type
runBatch ret = extract_Batch ∘ mapfst_Batch ret
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A: Type
cut: runBatch ret = extract_Batch ∘ mapfst_Batch ret
runBatch ret ∘ toBatch6 = id
      {
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A: Type
runBatch ret = extract_Batch ∘ mapfst_Batch ret unfold compose.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A: Type
runBatch ret = extract_Batch ○ mapfst_Batch ret ext b.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A: Type
b: Batch A (T A) (T A)
runBatch ret b = extract_Batch (mapfst_Batch ret b) induction b.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, C: Type
c: C
runBatch ret (Done c) =
extract_Batch (mapfst_Batch ret (Done c))
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, C: Type
b: Batch A (T A) (T A -> C)
a: A
IHb: runBatch ret b = extract_Batch (mapfst_Batch ret b)
runBatch ret (b ⧆ a) =
extract_Batch (mapfst_Batch ret (b ⧆ a))
        -
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, C: Type
c: C
runBatch ret (Done c) =
extract_Batch (mapfst_Batch ret (Done c)) reflexivity.
        -
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, C: Type
b: Batch A (T A) (T A -> C)
a: A
IHb: runBatch ret b = extract_Batch (mapfst_Batch ret b)
runBatch ret (b ⧆ a) =
extract_Batch (mapfst_Batch ret (b ⧆ a)) cbn.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, C: Type
b: Batch A (T A) (T A -> C)
a: A
IHb: runBatch ret b = extract_Batch (mapfst_Batch ret b)
runBatch ret b (ret a) =
extract_Batch (mapfst_Batch ret b) (ret a) rewrite IHb.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A, C: Type
b: Batch A (T A) (T A -> C)
a: A
IHb: runBatch ret b = extract_Batch (mapfst_Batch ret b)
extract_Batch (mapfst_Batch ret b) (ret a) =
extract_Batch (mapfst_Batch ret b) (ret a)
          reflexivity. }
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A: Type
cut: runBatch ret = extract_Batch ∘ mapfst_Batch ret
runBatch ret ∘ toBatch6 = id
      rewrite cut.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A: Type
cut: runBatch ret = extract_Batch ∘ mapfst_Batch ret
extract_Batch ∘ mapfst_Batch ret ∘ toBatch6 = id
      rewrite trfm_extract.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
A: Type
cut: runBatch ret = extract_Batch ∘ mapfst_Batch ret
id = id
      reflexivity.
    Qed.

    Lemma ktm_bindt2_T:
      forall `{Applicative G1} `{Applicative G2},
      forall (A B C: Type) (g: B -> G2 (T C)) (f: A -> G1 (T B)),
        map (F := G1) (bindt (G := G2) g) ∘ bindt (G := G1) f =
          bindt (G := G1 ∘ G2) (kc6 (G1 := G1) (G2 := G2) g f).
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
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 (T C))
  (f : A -> G1 (T B)),
map (bindt g) ∘ bindt f = bindt (g ⋆6 f)
    Proof.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
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 (T C))
  (f : A -> G1 (T B)),
map (bindt g) ∘ bindt f = bindt (g ⋆6 f)
      intros.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (bindt g) ∘ bindt f = bindt (g ⋆6 f)
      unfold_ops Bindt_ToBatch6.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (runBatch g ∘ toBatch6) ∘ (runBatch f ∘ toBatch6) =
runBatch (g ⋆6 f) ∘ toBatch6
      reassociate <- on left.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (runBatch g ∘ toBatch6) ∘ runBatch f ∘ toBatch6 =
runBatch (g ⋆6 f) ∘ toBatch6
      rewrite <- (fun_map_map (F := G1)).
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (runBatch g) ∘ map toBatch6 ∘ runBatch f
∘ toBatch6 = runBatch (g ⋆6 f) ∘ toBatch6
      reassociate -> near (runBatch f).
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (runBatch g) ∘ (map toBatch6 ∘ runBatch f)
∘ toBatch6 = runBatch (g ⋆6 f) ∘ toBatch6
      rewrite natural.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (runBatch g) ∘ (runBatch f ∘ map toBatch6)
∘ toBatch6 = runBatch (g ⋆6 f) ∘ toBatch6
      reassociate <- on left.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (runBatch g) ∘ runBatch f ∘ map toBatch6
∘ toBatch6 = runBatch (g ⋆6 f) ∘ toBatch6
      reassociate -> near toBatch6.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (runBatch g) ∘ runBatch f
∘ (map toBatch6 ∘ toBatch6) =
runBatch (g ⋆6 f) ∘ toBatch6
      rewrite <- trfm_duplicate.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (runBatch g) ∘ runBatch f
∘ (cojoin_Batch6 A B C ∘ toBatch6) =
runBatch (g ⋆6 f) ∘ toBatch6
      rewrite cojoin_Batch6_to_runBatch.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (runBatch g) ∘ runBatch f
∘ (runBatch double_batch6 ∘ toBatch6) =
runBatch (g ⋆6 f) ∘ toBatch6
      reassociate <- on left.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (runBatch g) ∘ runBatch f ∘ runBatch double_batch6
∘ toBatch6 = runBatch (g ⋆6 f) ∘ toBatch6
      rewrite natural.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
runBatch f ∘ map (runBatch g) ∘ runBatch double_batch6
∘ toBatch6 = runBatch (g ⋆6 f) ∘ toBatch6
      rewrite (runBatch_morphism'
                 (homomorphism :=
                    ApplicativeMorphism_parallel
                      (Batch A (T B)) (Batch B (T C)) G1 G2)).
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
runBatch
  (runBatch f ∘ map (runBatch g) ∘ double_batch6)
∘ toBatch6 = runBatch (g ⋆6 f) ∘ toBatch6
      rewrite (kc6_spec G1 G2).
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
runBatch
  (runBatch f ∘ map (runBatch g) ∘ double_batch6)
∘ toBatch6 =
runBatch
  (runBatch f ∘ map (runBatch g) ∘ double_batch6)
∘ toBatch6
      reflexivity.
    Qed.

    Lemma ktm_morph_T:
      forall `{ApplicativeMorphism G1 G2 ϕ},
      forall (A B: Type) (f: A -> G1 (T B)),
        ϕ (T B) ∘ bindt (G := G1) f = bindt (G := G2) (ϕ (T B) ∘ f).
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
forall (G1 G2 : Type -> Type) (H2 : Map G1)
  (H3 : Mult G1) (H4 : Pure G1) (H5 : Map G2)
  (H6 : Mult G2) (H7 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : A -> G1 (T B)),
ϕ (T B) ∘ bindt f = bindt (ϕ (T B) ∘ f)
    Proof.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
forall (G1 G2 : Type -> Type) (H2 : Map G1)
  (H3 : Mult G1) (H4 : Pure G1) (H5 : Map G2)
  (H6 : Mult G2) (H7 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : A -> G1 (T B)),
ϕ (T B) ∘ bindt f = bindt (ϕ (T B) ∘ f)
      intros.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H8: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
ϕ (T B) ∘ bindt f = bindt (ϕ (T B) ∘ f)
      unfold_ops Bindt_ToBatch6.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H8: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
ϕ (T B) ∘ (runBatch f ∘ toBatch6) =
runBatch (ϕ (T B) ∘ f) ∘ toBatch6
      reassociate <- on left.
T: Type -> Type
H: Return T
H0: ToBatch6 T T
H1: TraversableMonad T
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H8: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
ϕ (T B) ∘ runBatch f ∘ toBatch6 =
runBatch (ϕ (T B) ∘ f) ∘ toBatch6
      now rewrite runBatch_morphism'.
    Qed.


    (** ** Typeclass Instances *)
    (******************************************************************)
    #[export] Instance:
      Kleisli.TraversableMonad.TraversableRightPreModule T T :=
      {| ktm_bindt1 := ktm_bindt1_T;
         ktm_bindt2 := @ktm_bindt2_T;
         ktm_morph := @ktm_morph_T;
      |}.

    #[export] Instance TraversableMonad_Kleisli_Coalgebraic:
      Kleisli.TraversableMonad.TraversableMonad T :=
      {| ktm_bindt0 := @ktm_bindt0_T;
      |}.

  End with_algebra.

End DerivedInstances.