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

Import Functors.Early.Batch.Notations.
Import Kleisli.TraversableMonad.Notations.

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

#[local] Arguments batch {A} (B)%type_scope _.
#[local] Arguments toBatch6 {T U}%function_scope {ToBatch6}
  {A} (B)%type_scope _.


(** * Coalgebraic Traversable Monads *)
(**********************************************************************)

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

  #[export] Instance ToBatch6_Bindt `{Bindt T U}
: Coalgebraic.TraversableMonad.ToBatch6 T U :=
  (fun A B => bindt (G := Batch A (T B)) (batch (T B)):
     U A -> Batch A (T B) (U B)).

End DerivedOperations.

Class Compat_ToBatch6_Bindt
  (T: Type -> Type)
  (U: Type -> Type)
  `{Bindt_TU: Bindt T U}
  `{ToBatch6_TU: ToBatch6 T U} :=
  compat_toBatch6_bindt:
    ToBatch6_TU = DerivedOperations.ToBatch6_Bindt.

Lemma toBatch6_to_bindt
  `{Compat_ToBatch6_Bindt T U}:
  forall A B, toBatch6 (T := T) (U := U) (A := A) B =
           bindt (G := Batch A (T B)) (batch (T B)).
T, U: Type -> Type
Bindt_TU: Bindt T U
ToBatch6_TU: ToBatch6 T U
H: Compat_ToBatch6_Bindt T U
forall A B : Type, toBatch6 B = bindt (batch (T B))
Proof.
T, U: Type -> Type
Bindt_TU: Bindt T U
ToBatch6_TU: ToBatch6 T U
H: Compat_ToBatch6_Bindt T U
forall A B : Type, toBatch6 B = bindt (batch (T B))
  intros.
T, U: Type -> Type
Bindt_TU: Bindt T U
ToBatch6_TU: ToBatch6 T U
H: Compat_ToBatch6_Bindt T U
A, B: Type
toBatch6 B = bindt (batch (T B))
  rewrite compat_toBatch6_bindt.
T, U: Type -> Type
Bindt_TU: Bindt T U
ToBatch6_TU: ToBatch6 T U
H: Compat_ToBatch6_Bindt T U
A, B: Type
DerivedOperations.ToBatch6_Bindt A B =
bindt (batch (T B))
  reflexivity.
Qed.

#[export] Instance Compat_ToBatch6_Bindt_Self
  `{Bindt T U}: Compat_ToBatch6_Bindt T U
                  (ToBatch6_TU := DerivedOperations.ToBatch6_Bindt)
  := ltac:(hnf; reflexivity).

Module DerivedInstances.
  Section to_coalgebraic.

    Context
      `{Kleisli.TraversableMonad.TraversableMonad T}
      `{Map U}
      `{Bindt T U}
      `{! Compat_Map_Bindt T U}
      `{! Kleisli.TraversableMonad.TraversableRightPreModule T U}.

    Context
      `{ToBatch6 T T}
      `{ToBatch6 T U}
      `{! Compat_ToBatch6_Bindt T U}
      `{! Compat_ToBatch6_Bindt T T}.

    (** ** <<double_batch6>> as <<batch ⋆6 batch>> *)
    (******************************************************************)
    Lemma double_batch6_spec: forall (A B C: Type),
        double_batch6 (T := T) (A := A) =
          batch (T C) ⋆6 batch (T B).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
forall A B C : Type,
double_batch6 = batch (T C) ⋆6 batch (T B)
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
forall A B C : Type,
double_batch6 = batch (T C) ⋆6 batch (T B)
      intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B, C: Type
double_batch6 = batch (T C) ⋆6 batch (T B)
      rewrite compat_toBatch6_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B, C: Type
double_batch6 = batch (T C) ⋆6 batch (T B)
      reflexivity.
    Qed.

    (** ** Derived Laws *)
    (******************************************************************)
    Lemma toBatch6_ret_Kleisli: forall A B: Type,
        toBatch6 B ∘ ret (T := T) (A := A) = batch (T B).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
forall A B : Type, toBatch6 B ∘ ret = batch (T B)
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
forall A B : Type, toBatch6 B ∘ ret = batch (T B)
      intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B: Type
toBatch6 B ∘ ret = batch (T B)
      rewrite toBatch6_to_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B: Type
bindt (batch (T B)) ∘ ret = batch (T B)
      rewrite (ktm_bindt0 A).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B: Type
batch (T B) = batch (T B)
      reflexivity.
    Qed.

    Lemma toBatch6_extract_Kleisli: forall (A: Type),
        extract_Batch ∘ mapfst_Batch ret ∘ toBatch6 A = @id (U A).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
forall A : Type,
extract_Batch ∘ mapfst_Batch ret ∘ toBatch6 A = id
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
forall A : Type,
extract_Batch ∘ mapfst_Batch ret ∘ toBatch6 A = id
      intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
extract_Batch ∘ mapfst_Batch ret ∘ toBatch6 A = id
      reassociate -> on left.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
extract_Batch ∘ (mapfst_Batch ret ∘ toBatch6 A) = id
      rewrite toBatch6_to_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
extract_Batch
∘ (mapfst_Batch ret ∘ bindt (batch (T A))) = id
      rewrite (ktm_morph
                 (G1 := Batch A (T A))
                 (G2 := Batch (T A) (T A))
                 (morphism := ApplicativeMorphism_mapfst_Batch
                                (ret (T := T) (A := A)))
                 A A
                 (batch (T A))).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
extract_Batch ∘ bindt (mapfst_Batch ret ∘ batch (T A)) =
id
      rewrite (ktm_morph
                 (G1 := Batch (T A) (T A))
                 (G2 := fun A => A)
                 (morphism := ApplicativeMorphism_extract_Batch (T A))).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
bindt
  (extract_Batch ∘ (mapfst_Batch ret ∘ batch (T A))) =
id
      reassociate <- on left.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
bindt (extract_Batch ∘ mapfst_Batch ret ∘ batch (T A)) =
id
      assert (cut: extract_Batch ∘ mapfst_Batch ret ∘ batch (T A)
                   = ret).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
extract_Batch ∘ mapfst_Batch ret ∘ batch (T A) = ret
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
cut: extract_Batch ∘ mapfst_Batch ret ∘ batch (T A) =
ret
bindt (extract_Batch ∘ mapfst_Batch ret ∘ batch (T A)) =
id
      {
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
extract_Batch ∘ mapfst_Batch ret ∘ batch (T A) = ret ext a.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
a: A
(extract_Batch ∘ mapfst_Batch ret ∘ batch (T A)) a =
ret a unfold compose.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
a: A
extract_Batch (mapfst_Batch ret (batch (T A) a)) =
ret a reflexivity. }
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
cut: extract_Batch ∘ mapfst_Batch ret ∘ batch (T A) =
ret
bindt (extract_Batch ∘ mapfst_Batch ret ∘ batch (T A)) =
id
      rewrite cut.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
cut: extract_Batch ∘ mapfst_Batch ret ∘ batch (T A) =
ret
bindt ret = id
      rewrite ktm_bindt1.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A: Type
cut: extract_Batch ∘ mapfst_Batch ret ∘ batch (T A) =
ret
id = id
      reflexivity.
    Qed.

    Lemma toBatch6_duplicate_Kleisli: forall (A B C: Type),
        cojoin_Batch6 A B C (R := U C) ∘ toBatch6 (T := T) C =
          map (F := Batch A (T B)) (toBatch6 C) ∘ toBatch6 (U := U) B.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
forall A B C : Type,
cojoin_Batch6 A B C ∘ toBatch6 C =
map (toBatch6 C) ∘ toBatch6 B
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
forall A B C : Type,
cojoin_Batch6 A B C ∘ toBatch6 C =
map (toBatch6 C) ∘ toBatch6 B
      intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B, C: Type
cojoin_Batch6 A B C ∘ toBatch6 C =
map (toBatch6 C) ∘ toBatch6 B
      rewrite toBatch6_to_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B, C: Type
cojoin_Batch6 A B C ∘ bindt (batch (T C)) =
map (toBatch6 C) ∘ toBatch6 B
      change (Batch A (T B) (Batch B (T C) ?x))
        with ((Batch A (T B) ∘ Batch B (T C)) x).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B, C: Type
cojoin_Batch6 A B C ∘ bindt (batch (T C)) =
map (toBatch6 C) ∘ toBatch6 B
      erewrite (ktm_morph (T := T)
                  (G1 := Batch A (T C))
                  (G2 := Batch A (T B) ∘ Batch B (T C))
                  (morphism := ApplicativeMorphism_cojoin_Batch6 _ _ _)
                  (ϕ := @cojoin_Batch6 T _ A B C)).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B, C: Type
bindt (cojoin_Batch6 A B C ∘ batch (T C)) =
map (toBatch6 C) ∘ toBatch6 B
      unfold_compose_in_compose.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B, C: Type
bindt (cojoin_Batch6 A B C ∘ batch (T C)) =
map (toBatch6 C) ∘ toBatch6 B
      rewrite (cojoin_Batch6_batch).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B, C: Type
bindt double_batch6 = map (toBatch6 C) ∘ toBatch6 B
      rewrite toBatch6_to_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B, C: Type
bindt double_batch6 =
map (bindt (batch (T C))) ∘ toBatch6 B
      rewrite toBatch6_to_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B, C: Type
bindt double_batch6 =
map (bindt (batch (T C))) ∘ bindt (batch (T B))
      rewrite (ktm_bindt2 _ _).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B, C: Type
bindt double_batch6 =
bindt (batch (T C) ⋆6 batch (T B))
      rewrite double_batch6_spec.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: Kleisli.TraversableMonad.TraversableMonad T
U: Type -> Type
H0: Map U
H1: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H2: Kleisli.TraversableMonad.TraversableRightPreModule
  T U
H3: ToBatch6 T T
H4: ToBatch6 T U
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T T
A, B, C: Type
bindt (batch (T C) ⋆6 batch (T B)) =
bindt (batch (T C) ⋆6 batch (T B))
      reflexivity.
    Qed.

  End to_coalgebraic.

  (** ** Typeclass Instances *)
  (********************************************************************)
  Section instances.

    Context
      `{Return T}
      `{Map T}
      `{Bindt T T}
      `{! Compat_Map_Bindt T T}
      `{! Kleisli.TraversableMonad.TraversableMonad T}
      `{Map U}
      `{Bindt T U}
      `{! Compat_Map_Bindt T U}
      `{! Kleisli.TraversableMonad.TraversableRightPreModule T U}.

    Context
      `{ToBatch6 T T}
      `{ToBatch6 T U}
      `{! Compat_ToBatch6_Bindt T U}
      `{! Compat_ToBatch6_Bindt T T}.

    #[export] Instance:
      Coalgebraic.TraversableMonad.TraversableRightPreModule T T :=
      {| trfm_extract := toBatch6_extract_Kleisli;
         trfm_duplicate := toBatch6_duplicate_Kleisli;
      |}.

    #[export] Instance Coalgebraic_TraversableRightPreModule_of_Kleisli:
      Coalgebraic.TraversableMonad.TraversableRightPreModule T U :=
      {| trfm_extract := toBatch6_extract_Kleisli;
         trfm_duplicate := toBatch6_duplicate_Kleisli;
      |}.

    #[export] Instance Coalgebraic_TraversableMonad_of_Kleisli:
      Coalgebraic.TraversableMonad.TraversableMonad T :=
      {| trfm_ret := toBatch6_ret_Kleisli;
      |}.

    #[export] Instance Coalgebraic_TraversableRightModule_of_Kleisli:
      Coalgebraic.TraversableMonad.TraversableRightModule T U :=
      {| trfmod_monad := _
      |}.

  End instances.

End DerivedInstances.