DecoratedTraversableMonad.v

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

Import Product.Notations.
Import Kleisli.DecoratedTraversableMonad.Notations.
Import Kleisli.Comonad.Notations.
Import Batch.Notations.
Import Monoid.Notations.

#[local] Generalizable Variables U W G T M A B.

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


(** * DecoratedTraversableMonads as <<Batch7>> coalgebras *)
(**********************************************************************)
Module DerivedOperations.

  #[export] Instance ToBatch7_Binddt
    `{Binddt_WTU: Binddt W T U}:
  Coalgebraic.DecoratedTraversableMonad.ToBatch7 W T U :=
  (fun A B => binddt (G := Batch (W * A) (T B))
                (batch (T B)): U A -> Batch (W * A) (T B) (U B)).

End DerivedOperations.

Class Compat_ToBatch7_Binddt
  (W: Type)
  (T: Type -> Type)
  (U: Type -> Type)
  `{Binddt_inst: Binddt W T U}
  `{ToBatch7_inst: ToBatch7 W T U} :=
  compat_toBatch7_binddt:
    ToBatch7_inst = DerivedOperations.ToBatch7_Binddt.

Lemma toBatch7_to_binddt
  `{Compat_ToBatch7_Binddt W T U}:
  forall A B, toBatch7 (W := W) (T := T) (U := U) =
                binddt (G := Batch (W * A) (T B)) (batch (T B)).W: Type
T, U: Type -> Type
Binddt_inst: Binddt W T U
ToBatch7_inst: ToBatch7 W T U
H: Compat_ToBatch7_Binddt W T U
forall A B : Type, toBatch7 = binddt (batch (T B))
Proof.W: Type
T, U: Type -> Type
Binddt_inst: Binddt W T U
ToBatch7_inst: ToBatch7 W T U
H: Compat_ToBatch7_Binddt W T U
forall A B : Type, toBatch7 = binddt (batch (T B))
  intros.W: Type
T, U: Type -> Type
Binddt_inst: Binddt W T U
ToBatch7_inst: ToBatch7 W T U
H: Compat_ToBatch7_Binddt W T U
A, B: Type
toBatch7 = binddt (batch (T B))
  rewrite compat_toBatch7_binddt.W: Type
T, U: Type -> Type
Binddt_inst: Binddt W T U
ToBatch7_inst: ToBatch7 W T U
H: Compat_ToBatch7_Binddt W T U
A, B: Type
DerivedOperations.ToBatch7_Binddt A B =
binddt (batch (T B))
  reflexivity.
Qed.

#[export] Instance Compat_ToBatch7_Binddt_Self
  `{Binddt W T U}:
  Compat_ToBatch7_Binddt W T U
    (ToBatch7_inst := DerivedOperations.ToBatch7_Binddt)
  := ltac:(hnf; reflexivity).

Section dtm_coalgebraic_laws.

  Context
    `{Binddt W T T}
    `{Binddt W T U}
    `{Monoid W}
    `{Return T}
    `{! Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad W T}
    `{! DecoratedTraversableRightPreModule W T U}.

  Context
    `{ToBatch7_WTT: ToBatch7 W T T}
    `{ToBatch7_WTU: ToBatch7 W T U}
    `{! Compat_ToBatch7_Binddt W T T}
    `{! Compat_ToBatch7_Binddt W T U}.

  (** ** <<double_batch7>> as <<batch ⋆7 batch>> *)
  (********************************************************************)
  Lemma double_Batch7_spec: forall (A B C: Type),
      double_batch7 (A := A) (A' := B) =
        batch (T C) ⋆7 (batch (T B)).W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
forall A B C : Type,
double_batch7 = batch (T C) ⋆7 batch (T B)
  Proof.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
forall A B C : Type,
double_batch7 = batch (T C) ⋆7 batch (T B)
    intros.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
double_batch7 = batch (T C) ⋆7 batch (T B)
    unfold double_batch7.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
(fun '(w, a) =>
 (map (mapfst_Batch (incr w) ∘ toBatch7) ∘ batch (T B))
   (w, a)) = batch (T C) ⋆7 batch (T B)
    ext [w a].W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
w: W
a: A
(map (mapfst_Batch (incr w) ∘ toBatch7) ∘ batch (T B))
  (w, a) = (batch (T C) ⋆7 batch (T B)) (w, a)
    cbn.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
w: W
a: A
Done (mapfst_Batch (incr w) ∘ toBatch7 ∘ id) ⧆ (w, a) =
Done (binddt (batch (T C) ⦿ w) ∘ id) ⧆ (w, a)
    change (?f ∘ id) with f.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
w: W
a: A
Done (mapfst_Batch (incr w) ∘ toBatch7) ⧆ (w, a) =
Done (binddt (batch (T C) ⦿ w)) ⧆ (w, a)
    rewrite toBatch7_to_binddt.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
w: W
a: A
Done (mapfst_Batch (incr w) ∘ binddt (batch (T C)))
⧆ (w, a) = Done (binddt (batch (T C) ⦿ w)) ⧆ (w, a)
    rewrite (kdtm_morph
               (Batch (W * B) (T C))
               (Batch (W * B) (T C))
               (ϕ := fun C => mapfst_Batch (incr w))).W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
w: W
a: A
Done (binddt (mapfst_Batch (incr w) ∘ batch (T C)))
⧆ (w, a) = Done (binddt (batch (T C) ⦿ w)) ⧆ (w, a)
    rewrite ret_natural.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
w: W
a: A
Done (binddt (batch (T C) ∘ incr w)) ⧆ (w, a) =
Done (binddt (batch (T C) ⦿ w)) ⧆ (w, a)
    reflexivity.
  Qed.

  (** ** Derived Laws *)
  (********************************************************************)
  Lemma toBatch7_ret_Kleisli: forall A B: Type,
      toBatch7 ∘ ret (T := T) (A := A) = batch (T B) ∘ ret (T := (W ×)).W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
forall A B : Type, toBatch7 ∘ ret = batch (T B) ∘ ret
  Proof.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
forall A B : Type, toBatch7 ∘ ret = batch (T B) ∘ ret
    intros.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B: Type
toBatch7 ∘ ret = batch (T B) ∘ ret
    rewrite toBatch7_to_binddt.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B: Type
binddt (batch (T B)) ∘ ret = batch (T B) ∘ ret
    rewrite kdtm_binddt0.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B: Type
batch (T B) ∘ ret = batch (T B) ∘ ret
    reflexivity.
  Qed.

  Lemma toBatch7_extract_Kleisli: forall (A: Type),
      extract_Batch ∘ mapfst_Batch (ret ∘ extract (W := (W ×)))
        ∘ toBatch7 = @id (T A).W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
forall A : Type,
extract_Batch ∘ mapfst_Batch (ret ∘ extract)
∘ toBatch7 = id
  Proof.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
forall A : Type,
extract_Batch ∘ mapfst_Batch (ret ∘ extract)
∘ toBatch7 = id
    intros.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A: Type
extract_Batch ∘ mapfst_Batch (ret ∘ extract)
∘ toBatch7 = id
    rewrite toBatch7_to_binddt.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A: Type
extract_Batch ∘ mapfst_Batch (ret ∘ extract)
∘ binddt (batch (T A)) = id
    reassociate -> on left.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A: Type
extract_Batch
∘ (mapfst_Batch (ret ∘ extract) ∘ binddt (batch (T A))) =
id
    rewrite (kdtm_morph (U := T) (B := A)
               (Batch (W * A) (T A))
               (Batch (T A) (T A))
               (ϕ := fun C => mapfst_Batch (ret ∘ extract))).W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A: Type
extract_Batch
∘ binddt (mapfst_Batch (ret ∘ extract) ∘ batch (T A)) =
id
    rewrite (kdtm_morph (U := T) (B := A)
               (Batch (T A) (T A))
               (fun A => A)
               (ϕ := fun C => extract_Batch)).W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A: Type
binddt
  (extract_Batch
   ∘ (mapfst_Batch (ret ∘ extract) ∘ batch (T A))) =
id
    rewrite ret_natural.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A: Type
binddt
  (extract_Batch ∘ (batch (T A) ∘ (ret ∘ extract))) =
id
    reassociate <- on left.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A: Type
binddt (extract_Batch ∘ batch (T A) ∘ (ret ∘ extract)) =
id
    rewrite extract_Batch_batch.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A: Type
binddt (id ∘ (ret ∘ extract)) = id
    change (id ∘ ?f) with f.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A: Type
binddt (ret ∘ extract) = id
    rewrite kdtm_binddt1.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A: Type
id = id
    reflexivity.
  Qed.

  Lemma toBatch7_duplicate_Kleisli: forall (A B C: Type),
      cojoin_Batch7 ∘ toBatch7 (A := A) (B := C) =
        map (F := Batch (W * A) (T B)) toBatch7 ∘ toBatch7.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
forall A B C : Type,
cojoin_Batch7 ∘ toBatch7 = map toBatch7 ∘ toBatch7
  Proof.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
forall A B C : Type,
cojoin_Batch7 ∘ toBatch7 = map toBatch7 ∘ toBatch7
    intros.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
cojoin_Batch7 ∘ toBatch7 = map toBatch7 ∘ toBatch7
    rewrite cojoin_Batch7_to_runBatch.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
runBatch double_batch7 ∘ toBatch7 =
map toBatch7 ∘ toBatch7
    rewrite toBatch7_to_binddt.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
runBatch double_batch7 ∘ binddt (batch (T C)) =
map toBatch7 ∘ toBatch7
    rewrite toBatch7_to_binddt.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
runBatch double_batch7 ∘ binddt (batch (T C)) =
map (binddt (batch (T C))) ∘ toBatch7
    rewrite toBatch7_to_binddt.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
runBatch double_batch7 ∘ binddt (batch (T C)) =
map (binddt (batch (T C))) ∘ binddt (batch (T B))
    rewrite double_Batch7_spec.W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
runBatch (batch (T C) ⋆7 batch (T B))
∘ binddt (batch (T C)) =
map (binddt (batch (T C))) ∘ binddt (batch (T B))
    rewrite (kdtm_morph (U := U) (T := T) (W := W) (A := A) (B := C)
               (Batch (W * A) (T C))
               (Batch (W * A) (T B) ∘ Batch (W * B) (T C))
               (morph := ApplicativeMorphism_runBatch)).W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
binddt
  (runBatch (batch (T C) ⋆7 batch (T B)) ∘ batch (T C)) =
map (binddt (batch (T C))) ∘ binddt (batch (T B))
    rewrite (runBatch_batch _).W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
binddt (batch (T C) ⋆7 batch (T B)) =
map (binddt (batch (T C))) ∘ binddt (batch (T B))
    rewrite (kdtm_binddt2 _ _).W: Type
T: Type -> Type
H: Binddt W T T
U: Type -> Type
H0: Binddt W T U
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
H2: Return T
H3: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
ToBatch7_WTT: ToBatch7 W T T
ToBatch7_WTU: ToBatch7 W T U
Compat_ToBatch7_Binddt0: Compat_ToBatch7_Binddt W T T
Compat_ToBatch7_Binddt1: Compat_ToBatch7_Binddt W T U
A, B, C: Type
binddt (batch (T C) ⋆7 batch (T B)) =
binddt (batch (T C) ⋆7 batch (T B))
    reflexivity.
  Qed.

End dtm_coalgebraic_laws.

Module DerivedInstances.
  Section instances.

    Context
      `{Binddt W T T}
      `{Binddt W T U}
      `{Monoid W}
      `{Return T}
      `{! Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad W T}
      `{! DecoratedTraversableRightPreModule W T U}.

    Context
      `{ToBatch7_WTT: ToBatch7 W T T}
      `{ToBatch7_WTU: ToBatch7 W T U}
      `{! Compat_ToBatch7_Binddt W T T}
      `{! Compat_ToBatch7_Binddt W T U}.

    #[export] Instance DecoratedTraversableMonad_Coalgebraic_Kleisli:
      Coalgebraic.DecoratedTraversableMonad.DecoratedTraversableMonad W T :=
      {| dtm_ret := toBatch7_ret_Kleisli;
         dtm_extract := toBatch7_extract_Kleisli;
         dtm_duplicate := toBatch7_duplicate_Kleisli;
      |}.


  (*
    #[export] Instance Coalgebraic_DecoratedTraversableMonad_of_Kleisli:
    Coalgebraic.DecoratedTraversableMonad.DecoratedTraversableRightModule W T U :=
    {| dtm_ret := toBatch7_ret_Kleisli;
       dtm_extract := toBatch7_extract_Kleisli;
       dtm_duplicate := toBatch7_duplicate_Kleisli;
    |}.
   *)

  End instances.
End DerivedInstances.