TraversableMonad.v

From Tealeaves Require Import
  Classes.Categorical.TraversableMonad
  Classes.Kleisli.TraversableMonad
  Classes.Coalgebraic.TraversableMonad
  Adapters.CategoricalToKleisli.TraversableMonad
  Adapters.KleisliToCategorical.TraversableMonad
  Adapters.CoalgebraicToKleisli.TraversableMonad
  Adapters.KleisliToCoalgebraic.TraversableMonad.

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

#[local] Generalizable Variables T.

(** * Categorical ~> Kleisli ~> Categorical *)
(**********************************************************************)
Module Categorical_Kleisli_Categorical.

  Context
    `{mapT: Map T}
    `{distT: ApplicativeDist T}
    `{joinT: Join T}
    `{Return T}
    `{! Categorical.TraversableMonad.TraversableMonad T}.

  Definition bindt':
    Bindt T T :=
    CategoricalToKleisli.TraversableMonad.DerivedOperations.Bindt_Categorical T.

  Definition map2: Map T :=
    DerivedOperations.Map_Bindt T T (Bindt_TU := bindt').

  Definition dist2: ApplicativeDist T :=
    DerivedOperations.Dist_Bindt T (Bindt_TT := bindt').

  Definition join2: Join T :=
    DerivedOperations.Join_Bindt T (Bindt_TT := bindt').

  Goal mapT = map2.mapT = map2
  Proof.mapT = map2
    ext A B f.A, B: Type
f: A -> B
mapT A B f = map2 A B f
    unfold map2.A, B: Type
f: A -> B
mapT A B f = DerivedOperations.Map_Bindt T T A B f
    unfold DerivedOperations.Map_Bindt.A, B: Type
f: A -> B
mapT A B f = bindt (ret ∘ f)
    unfold bindt.A, B: Type
f: A -> B
mapT A B f =
bindt' (fun A : Type => A) Map_I Pure_I Mult_I A B
  (ret ∘ f)
    unfold bindt'.A, B: Type
f: A -> B
mapT A B f =
DerivedOperations.Bindt_Categorical T
  (fun A : Type => A) Map_I Pure_I Mult_I A B
  (ret ∘ f)
    unfold DerivedOperations.Bindt_Categorical.A, B: Type
f: A -> B
mapT A B f =
map join ∘ dist T (fun A : Type => A) ∘ map (ret ∘ f)
    unfold_ops @Map_I.A, B: Type
f: A -> B
mapT A B f =
join ∘ dist T (fun A : Type => A) ∘ map (ret ∘ f)
    rewrite (dist_unit (F := T)).A, B: Type
f: A -> B
mapT A B f = join ∘ id ∘ map (ret ∘ f)
    change (?g ∘ id) with g.A, B: Type
f: A -> B
mapT A B f = join ∘ map (ret ∘ f)
    rewrite <- (fun_map_map (F := T)).A, B: Type
f: A -> B
mapT A B f = join ∘ (map ret ∘ map f)
    reassociate <- on right.A, B: Type
f: A -> B
mapT A B f = join ∘ map ret ∘ map f
    rewrite (mon_join_map_ret (T := T)).A, B: Type
f: A -> B
mapT A B f = id ∘ map f
    reflexivity.
  Qed.

  Goal forall G `{Applicative G},
      @distT G _ _ _ = @dist2 G _ _ _.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
distT G Map_G Pure_G Mult_G =
dist2 G Map_G Pure_G Mult_G
  Proof.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
distT G Map_G Pure_G Mult_G =
dist2 G Map_G Pure_G Mult_G
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
distT G Map_G Pure_G Mult_G =
dist2 G Map_G Pure_G Mult_G
    ext A.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
dist2 G Map_G Pure_G Mult_G A
    unfold dist2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
DerivedOperations.Dist_Bindt T G Map_G Pure_G Mult_G A
    unfold DerivedOperations.Dist_Bindt.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A = bindt (map ret)
    unfold bindt.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
bindt' G Map_G Pure_G Mult_G (G A) A (map ret)
    unfold bindt'.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
DerivedOperations.Bindt_Categorical T G Map_G Pure_G
  Mult_G (G A) A (map ret)
    unfold DerivedOperations.Bindt_Categorical.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ dist T G ∘ map (map ret)
    change (map (map (ret (T := T)))) with
      (map (F := T ∘ G) (ret (T := T) (A := A))).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ dist T G ∘ map ret
    reassociate -> on right.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ (dist T G ∘ map ret)
    unfold_compose_in_compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ (dist T G ∘ map ret)
    rewrite <- (natural (Natural := dist_natural (F := T))
                  (ϕ := @dist T _ G _ _ _)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ (map ret ∘ dist T G)
    reassociate <- on right.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ map ret ∘ dist T G
    unfold_ops @Map_compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ map (map ret) ∘ dist T G
    rewrite (fun_map_map (F := G)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map (join ∘ map ret) ∘ dist T G
    rewrite (mon_join_map_ret (T := T)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A = map id ∘ dist T G
    rewrite (fun_map_id (F := G)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A = id ∘ dist T G
    reflexivity.
  Qed.

  Goal joinT = join2.joinT = join2
  Proof.joinT = join2
    ext A.A: Type
joinT A = join2 A
    unfold join2.A: Type
joinT A = DerivedOperations.Join_Bindt T A
    unfold DerivedOperations.Join_Bindt.A: Type
joinT A = bindt id
    unfold bindt.A: Type
joinT A =
bindt' (fun A : Type => A) Map_I Pure_I Mult_I (T A) A
  id
    unfold bindt'.A: Type
joinT A =
DerivedOperations.Bindt_Categorical T
  (fun A : Type => A) Map_I Pure_I Mult_I (T A) A id
    unfold DerivedOperations.Bindt_Categorical.A: Type
joinT A =
map join ∘ dist T (fun A : Type => A) ∘ map id
    rewrite (fun_map_id (F := T)).A: Type
joinT A = map join ∘ dist T (fun A : Type => A) ∘ id
    unfold_ops @Map_I.A: Type
joinT A = join ∘ dist T (fun A : Type => A) ∘ id
    rewrite (dist_unit (F := T)).A: Type
joinT A = join ∘ id ∘ id
    reflexivity.
  Qed.

End Categorical_Kleisli_Categorical.

(** * Kleisli ~> Categorical ~> Kleisli *)
(**********************************************************************)
Module Kleisli_Categorical_Kleisli.

  Context
    `{bindtT: Bindt T T}
    `{Return T}
    `{! Kleisli.TraversableMonad.TraversableMonad T}.

  Definition map': Map T :=
    DerivedOperations.Map_Bindt T T.
  Definition dist': ApplicativeDist T :=
    DerivedOperations.Dist_Bindt T.
  Definition join': Join T :=
    DerivedOperations.Join_Bindt T.

  Definition bindt2: Bindt T T :=
    DerivedOperations.Bindt_Categorical T
      (Map_T := map') (Join_T := join') (Dist_T := dist').

  Goal forall A B G `{Applicative G},
      @bindtT G _ _ _ A B = @bindt2 G _ _ _ A B.forall (A B : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
bindtT G Map_G Pure_G Mult_G A B =
bindt2 G Map_G Pure_G Mult_G A B
  Proof.forall (A B : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
bindtT G Map_G Pure_G Mult_G A B =
bindt2 G Map_G Pure_G Mult_G A B
    intros.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
bindtT G Map_G Pure_G Mult_G A B =
bindt2 G Map_G Pure_G Mult_G A B ext f.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
bindt2 G Map_G Pure_G Mult_G A B f
    unfold bindt2.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
DerivedOperations.Bindt_Categorical T G Map_G Pure_G
  Mult_G A B f
    unfold DerivedOperations.Bindt_Categorical.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map join ∘ dist T G ∘ map f
    unfold join.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (join' B) ∘ dist T G ∘ map f
    unfold join'.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (DerivedOperations.Join_Bindt T B) ∘ dist T G
∘ map f
    unfold DerivedOperations.Join_Bindt.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ dist T G ∘ map f
    unfold dist.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ dist' G Map_G Pure_G Mult_G (T B)
∘ map f
    unfold dist'.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id)
∘ DerivedOperations.Dist_Bindt T G Map_G Pure_G Mult_G
    (T B) ∘ map f
    unfold DerivedOperations.Dist_Bindt.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ bindt (map ret) ∘ map f
    unfold map at 3.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ bindt (map ret) ∘ map' A (G (T B)) f
    unfold map'.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ bindt (map ret)
∘ DerivedOperations.Map_Bindt T T A (G (T B)) f
    unfold DerivedOperations.Map_Bindt.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ bindt (map ret) ∘ bindt (ret ∘ f)
    reassociate -> on right.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ (bindt (map ret) ∘ bindt (ret ∘ f))
    change (bindt (A := G (T B)) (B := T B)
              (map (F := G) (ret (A := T B)))) with
      (map (F := fun A => A) (bindt (A := G (T B)) (B := T B)
                                (map (F := G) ret))).A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id)
∘ (map (bindt (map ret)) ∘ bindt (ret ∘ f))
    unfold_compose_in_compose.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id)
∘ (map (bindt (map ret)) ∘ bindt (ret ∘ f))
    rewrite (ktm_bindt2 (G1 := fun A => A)).A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ bindt (map ret ⋆6 ret ∘ f)
    unfold kc6.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id)
∘ bindt (map (bindt (map ret)) ∘ (ret ∘ f))
    unfold_ops @Map_I.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ bindt (bindt (map ret) ∘ (ret ∘ f))
    reassociate <- on right.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ bindt (bindt (map ret) ∘ ret ∘ f)
    rewrite (ktm_bindt0 (T := T)).A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ bindt (map ret ∘ f)
    rewrite (bindt_app_id_l).A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ bindt (map ret ∘ f)
    change ((fun A => A) ∘ ?G) with G.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ bindt (map ret ∘ f)
    unfold compose at 2.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
map (bindt id) ∘ bindt (map ret ∘ f)
    rewrite (ktm_bindt2 (T := T) (G1 := G) (G2 := fun A => A)).A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
bindt (id ⋆6 map ret ∘ f)
    rewrite bindt_app_id_r.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
bindt (id ⋆6 map ret ∘ f)
    unfold kc6.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
bindt (map (bindt id) ∘ (map ret ∘ f))
    reassociate <-.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
bindt (map (bindt id) ∘ map ret ∘ f)
    rewrite (fun_map_map).A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
bindt (map (bindt id ∘ ret) ∘ f)
    rewrite (ktm_bindt0 (G := fun A => A)).A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
bindt (map id ∘ f)
    rewrite fun_map_id.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f = bindt (id ∘ f)
    reflexivity.
  Qed.

End Kleisli_Categorical_Kleisli.


(** * Coalgebraic ~> Kleisli ~> Coalgebraic *)
(**********************************************************************)
Module Coalgebraic_Kleisli_Coalgebraic.

  Context
    `{toBatch6_T: ToBatch6 T T}
    `{Return T}
    `{! Coalgebraic.TraversableMonad.TraversableMonad T}.

  Definition bindt': Bindt T T :=
    @DerivedOperations.Bindt_ToBatch6 T T toBatch6_T.

  Definition toBatch6_2: ToBatch6 T T :=
    @DerivedOperations.ToBatch6_Bindt T T bindt'.

  Goal forall A B, @toBatch6_T A B = @toBatch6_2 A B.forall A B : Type, toBatch6_T A B = toBatch6_2 A B
  Proof.forall A B : Type, toBatch6_T A B = toBatch6_2 A B
    intros.A, B: Type
toBatch6_T A B = toBatch6_2 A B
    unfold toBatch6_2.A, B: Type
toBatch6_T A B = DerivedOperations.ToBatch6_Bindt A B
    unfold DerivedOperations.ToBatch6_Bindt.A, B: Type
toBatch6_T A B = bindt (batch A (T B))
    unfold bindt.A, B: Type
toBatch6_T A B =
bindt' (Batch A (T B)) Map_Batch Pure_Batch Mult_Batch
  A B (batch A (T B))
    unfold bindt'.A, B: Type
toBatch6_T A B =
DerivedOperations.Bindt_ToBatch6 T T (Batch A (T B))
  Map_Batch Pure_Batch Mult_Batch A B (batch A (T B))
    unfold DerivedOperations.Bindt_ToBatch6.A, B: Type
toBatch6_T A B = runBatch (batch A (T B)) ∘ toBatch6
    rewrite runBatch_batch_id.A, B: Type
toBatch6_T A B = id ∘ toBatch6
    reflexivity.
  Qed.

End Coalgebraic_Kleisli_Coalgebraic.


(** * Kleisli ~> Coalgebraic ~> Kleisli *)
(**********************************************************************)
Module Kleisli_Coalgebraic_Kleisli.

  Context
    `{bindtT: Bindt T T}
    `{Return T}
    `{! Kleisli.TraversableMonad.TraversableMonad T}.

  Definition toBatch6': ToBatch6 T T :=
    DerivedOperations.ToBatch6_Bindt.

  Definition bindt2: Bindt T T :=
    DerivedOperations.Bindt_ToBatch6 T T
      (H := toBatch6').

  Goal forall A B G `{Applicative G},
      @bindtT G _ _ _ A B = @bindt2 G _ _ _ A B.forall (A B : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
bindtT G Map_G Pure_G Mult_G A B =
bindt2 G Map_G Pure_G Mult_G A B
  Proof.forall (A B : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
bindtT G Map_G Pure_G Mult_G A B =
bindt2 G Map_G Pure_G Mult_G A B
    intros.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
bindtT G Map_G Pure_G Mult_G A B =
bindt2 G Map_G Pure_G Mult_G A B ext f.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
bindt2 G Map_G Pure_G Mult_G A B f
    unfold bindt2.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
DerivedOperations.Bindt_ToBatch6 T T G Map_G Pure_G
  Mult_G A B f
    unfold DerivedOperations.Bindt_ToBatch6.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
runBatch f ∘ toBatch6
    unfold toBatch6.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
runBatch f ∘ toBatch6' A B
    unfold toBatch6'.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
runBatch f ∘ DerivedOperations.ToBatch6_Bindt A B
    unfold DerivedOperations.ToBatch6_Bindt.A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
runBatch f ∘ bindt (batch A (T B))
    rewrite (ktm_morph (U := T)
               (morphism := Batch.ApplicativeMorphism_runBatch)
               (ϕ := @Batch.runBatch _ _ G _ _ _ f)).A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f =
bindt (runBatch f ∘ batch A (T B))
    rewrite (Batch.runBatch_batch G).A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
f: A -> G (T B)
bindtT G Map_G Pure_G Mult_G A B f = bindt f
    reflexivity.
  Qed.

End Kleisli_Coalgebraic_Kleisli.