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

Import Monoid.Notations.
Import Applicative.Notations.
Import Product.Notations.
Import DecoratedTraversableFunctor.Notations.

#[local] Generalizable Variables E T G ϕ.

(** * Coalgebraic DTFs to Kleisli DTFs *)
(**********************************************************************)

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

  #[export] Instance Mapdt_ToBatch3
    (E: Type) (T: Type -> Type)
    `{ToBatch3_ET: ToBatch3 E T}:
  Mapdt E T := fun G _ _ _ A B f =>
                 (runBatch f ∘ toBatch3: T A -> G (T B)).

End DerivedOperations.

Module DerivedInstances.

  Import DerivedOperations.

  Section with_algebra.

    Context
      `{Coalgebraic.DecoratedTraversableFunctor.DecoratedTraversableFunctor E T}.

    (** ** <<⋆3>> as <<runBatch ∘ map runBatch ∘ double_batch3>> *)
    (******************************************************************)
    Lemma kc3_spec:
      forall `{Applicative G1}
        `{Applicative G2},
      forall (A B C: Type)
        (g: E * B -> G2 C) (f: E * A -> G1 B),
        g ⋆3 f =
          runBatch (G := G1) f (C := G2 C) ∘
            map (F := Batch (E * A) B)
            (runBatch (G := G2) g (C := C)) ∘ double_batch3 C.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E 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 : E * B -> G2 C)
  (f : E * A -> G1 B),
g ⋆3 f =
runBatch f ∘ map (runBatch g) ∘ double_batch3 C
    Proof.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E 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 : E * B -> G2 C)
  (f : E * A -> G1 B),
g ⋆3 f =
runBatch f ∘ map (runBatch g) ∘ double_batch3 C
      intros.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
g ⋆3 f =
runBatch f ∘ map (runBatch g) ∘ double_batch3 C ext [e a].
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
e: E
a: A
(g ⋆3 f) (e, a) =
(runBatch f ∘ map (runBatch g) ∘ double_batch3 C)
  (e, a)
      unfold compose.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
e: E
a: A
(g ⋆3 f) (e, a) =
runBatch f (map (runBatch g) (double_batch3 C (e, a)))
      rewrite (double_batch3_rw (e, a)).
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
e: E
a: A
(g ⋆3 f) (e, a) =
runBatch f
  (map (runBatch g)
     (Step (Done (batch (E * B) C ∘ pair e)) (e, a)))
      rewrite map_Batch_rw2.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
e: E
a: A
(g ⋆3 f) (e, a) =
runBatch f
  (Step
     (map (compose (runBatch g))
        (Done (batch (E * B) C ∘ pair e))) (e, a))
      rewrite map_Batch_rw1.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
e: E
a: A
(g ⋆3 f) (e, a) =
runBatch f
  (Step
     (Done (runBatch g ∘ (batch (E * B) C ∘ pair e)))
     (e, a))
      rewrite runBatch_rw2.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
e: E
a: A
(g ⋆3 f) (e, a) =
runBatch f
  (Done (runBatch g ∘ (batch (E * B) C ∘ pair e))) <⋆>
f (e, a)
      rewrite runBatch_rw1.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
e: E
a: A
(g ⋆3 f) (e, a) =
pure (runBatch g ∘ (batch (E * B) C ∘ pair e)) <⋆>
f (e, a)
      rewrite <- (map_to_ap).
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
e: E
a: A
(g ⋆3 f) (e, a) =
map (runBatch g ∘ (batch (E * B) C ∘ pair e))
  (f (e, a))
      reassociate <- on right.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
e: E
a: A
(g ⋆3 f) (e, a) =
map (runBatch g ∘ batch (E * B) C ∘ pair e) (f (e, a))
      rewrite (runBatch_batch G2).
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
e: E
a: A
(g ⋆3 f) (e, a) = map (g ∘ pair e) (f (e, a))
      rewrite kc3_spec.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
e: E
a: A
map (g ∘ pair e) (f (e, a)) =
map (g ∘ pair e) (f (e, a))
      reflexivity.
    Qed.

    (** ** Derived Laws *)
    (******************************************************************)
    Lemma kdtf_mapdt1_T: forall (A: Type),
        mapdt (G := fun A => A) (extract (W := (E ×))) = @id (T A).
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
forall A : Type, mapdt extract = id
    Proof.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
forall A : Type, mapdt extract = id
      intros.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
A: Type
mapdt extract = id
      unfold_ops @Mapdt_ToBatch3.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
A: Type
runBatch extract ∘ toBatch3 = id
      rewrite (runBatch_via_traverse (F := fun A => A)).
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
A: Type
map extract_Batch ∘ traverse extract ∘ toBatch3 = id
      rewrite <- TraversableFunctor.map_to_traverse.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
A: Type
map extract_Batch ∘ map extract ∘ toBatch3 = id
      rewrite <- dtf_extract.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
A: Type
map extract_Batch ∘ map extract ∘ toBatch3 =
extract_Batch ∘ mapfst_Batch extract ∘ toBatch3
      reflexivity.
    Qed.

    Lemma kdtf_mapdt2_T:
      forall `{Applicative G1}
        `{Applicative G2},
      forall (A B C: Type) (g: E * B -> G2 C) (f: E * A -> G1 B),
        map (F := G1) (mapdt g) ∘ mapdt f =
          mapdt (G := G1 ∘ G2) (g ⋆3 f).
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E 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 : E * B -> G2 C)
  (f : E * A -> G1 B),
map (mapdt g) ∘ mapdt f = mapdt (g ⋆3 f)
    Proof.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E 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 : E * B -> G2 C)
  (f : E * A -> G1 B),
map (mapdt g) ∘ mapdt f = mapdt (g ⋆3 f)
      intros.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (mapdt g) ∘ mapdt f = mapdt (g ⋆3 f)
      unfold_ops @Mapdt_ToBatch3.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (runBatch g ∘ toBatch3) ∘ (runBatch f ∘ toBatch3) =
runBatch (g ⋆3 f) ∘ toBatch3
      reassociate <- on left.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (runBatch g ∘ toBatch3) ∘ runBatch f ∘ toBatch3 =
runBatch (g ⋆3 f) ∘ toBatch3
      rewrite <- (fun_map_map (F := G1)).
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (runBatch g) ∘ map toBatch3 ∘ runBatch f
∘ toBatch3 = runBatch (g ⋆3 f) ∘ toBatch3
      reassociate -> near (runBatch f).
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (runBatch g) ∘ (map toBatch3 ∘ runBatch f)
∘ toBatch3 = runBatch (g ⋆3 f) ∘ toBatch3
      rewrite natural.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (runBatch g) ∘ (runBatch f ∘ map toBatch3)
∘ toBatch3 = runBatch (g ⋆3 f) ∘ toBatch3
      reassociate <- on left.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (runBatch g) ∘ runBatch f ∘ map toBatch3
∘ toBatch3 = runBatch (g ⋆3 f) ∘ toBatch3
      reassociate -> near toBatch3.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (runBatch g) ∘ runBatch f
∘ (map toBatch3 ∘ toBatch3) =
runBatch (g ⋆3 f) ∘ toBatch3
      rewrite <- dtf_duplicate.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (runBatch g) ∘ runBatch f
∘ (cojoin_Batch3 ∘ toBatch3) =
runBatch (g ⋆3 f) ∘ toBatch3
      rewrite cojoin_Batch3_to_runBatch.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (runBatch g) ∘ runBatch f
∘ (runBatch (double_batch3 C) ∘ toBatch3) =
runBatch (g ⋆3 f) ∘ toBatch3
      reassociate <- on left.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (runBatch g) ∘ runBatch f
∘ runBatch (double_batch3 C) ∘ toBatch3 =
runBatch (g ⋆3 f) ∘ toBatch3
      rewrite natural.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
runBatch f ∘ map (runBatch g)
∘ runBatch (double_batch3 C) ∘ toBatch3 =
runBatch (g ⋆3 f) ∘ toBatch3
      rewrite (runBatch_morphism'
                 (homomorphism :=
                    ApplicativeMorphism_parallel
                      (Batch (E * A) B) (Batch (E * B) C) G1 G2)).
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
runBatch
  (runBatch f ∘ map (runBatch g) ∘ double_batch3 C)
∘ toBatch3 = runBatch (g ⋆3 f) ∘ toBatch3
      rewrite kc3_spec.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
runBatch
  (runBatch f ∘ map (runBatch g) ∘ double_batch3 C)
∘ toBatch3 =
runBatch
  (runBatch f ∘ map (runBatch g) ∘ double_batch3 C)
∘ toBatch3
      reflexivity.
    Qed.

    Lemma kdtf_morph_T:
      forall (G1 G2: Type -> Type) `{morph: ApplicativeMorphism G1 G2 ϕ},
      forall (A B: Type) (f: E * A -> G1 B),
        ϕ (T B) ∘ mapdt f = mapdt (ϕ B ∘ f).
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
forall (G1 G2 : Type -> Type) (H1 : Map G1)
  (H2 : Mult G1) (H3 : Pure G1) (H4 : Map G2)
  (H5 : Mult G2) (H6 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : E * A -> G1 B),
ϕ (T B) ∘ mapdt f = mapdt (ϕ B ∘ f)
    Proof.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
forall (G1 G2 : Type -> Type) (H1 : Map G1)
  (H2 : Mult G1) (H3 : Pure G1) (H4 : Map G2)
  (H5 : Mult G2) (H6 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : E * A -> G1 B),
ϕ (T B) ∘ mapdt f = mapdt (ϕ B ∘ f)
      intros.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
ϕ (T B) ∘ mapdt f = mapdt (ϕ B ∘ f) ext t.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
t: T A
(ϕ (T B) ∘ mapdt f) t = mapdt (ϕ B ∘ f) t
      unfold_ops @Mapdt_ToBatch3.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
t: T A
(ϕ (T B) ∘ (runBatch f ∘ toBatch3)) t =
(runBatch (ϕ B ∘ f) ∘ toBatch3) t
      reassociate <- on left.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
t: T A
(ϕ (T B) ∘ runBatch f ∘ toBatch3) t =
(runBatch (ϕ B ∘ f) ∘ toBatch3) t
      rewrite runBatch_morphism'.
E: Type
T: Type -> Type
H: ToBatch3 E T
H0: DecoratedTraversableFunctor E T
G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
t: T A
(runBatch (ϕ B ∘ f) ∘ toBatch3) t =
(runBatch (ϕ B ∘ f) ∘ toBatch3) t
      reflexivity.
    Qed.

    (** ** Typeclass Instances *)
    (******************************************************************)
    #[export] Instance TraversableFunctor_Kleisli_Coalgebra:
      Classes.Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor E T :=
      {|
        kdtf_mapdt1 := kdtf_mapdt1_T;
        kdtf_mapdt2 := @kdtf_mapdt2_T;
        kdtf_morph := kdtf_morph_T;
      |}.

  End with_algebra.

End DerivedInstances.