From Tealeaves Require Export
  Classes.Categorical.Applicative
  Classes.Categorical.Monad (Return, ret).

#[local] Generalizable Variables U T G A B C D ϕ M f.

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

(** ** The [bindt] operation *)
(**********************************************************************)
Class Bindt (T: Type -> Type) (U: Type -> Type) :=
  bindt:
    forall (G: Type -> Type)
      `{Map_G: Map G} `{Pure_G: Pure G} `{Mult_G: Mult G}
      (A B: Type), (A -> G (T B)) -> U A -> G (U B).

#[global] Arguments bindt {T U}%function_scope {Bindt} {G}%function_scope
  {Map_G Pure_G Mult_G} {A B}%type_scope _%function_scope _.

(** ** Kleisli Composition *)
(**********************************************************************)
Definition kc6
  `{Bindt T T}
  {A B C: Type}
  {G1 G2: Type -> Type}
  `{Map G1} `{Pure G1} `{Mult G1}
  `{Map G2} `{Pure G2} `{Mult G2}:
  (B -> G2 (T C)) ->
  (A -> G1 (T B)) ->
  (A -> G1 (G2 (T C))) :=
  fun g f => map (F := G1) (bindt g) ∘ f.

#[local] Infix "⋆6" := (kc6) (at level 60): tealeaves_scope.

(** ** Typeclass *)
(**********************************************************************)
Class TraversableRightPreModule (T: Type -> Type) (U: Type -> Type)
  `{Return_T: Return T}
  `{Bindt_TT: Bindt T T}
  `{Bindt_TU: Bindt T U} :=
  { ktm_bindt1: forall (A: Type),
      bindt (U := U) (G := fun A => A) (ret (T := T)) = @id (U A);
    ktm_bindt2:
    forall `{Applicative G1} `{Applicative G2} (A B C: Type)
      (g: B -> G2 (T C)) (f: A -> G1 (T B)),
      map (F := G1) (bindt g) ∘ bindt (U := U) f =
        bindt (U := U) (kc6 (G1 := G1) (G2 := G2) g f);
    ktm_morph:
    forall `{morphism: ApplicativeMorphism G1 G2 ϕ}
      (A B: Type) `(f: A -> G1 (T B)),
      ϕ (U B) ∘ bindt (U := U) f = bindt (ϕ (T B) ∘ f);
  }.

Class TraversableMonad (T: Type -> Type)
  `{Return_T: Return T}
  `{Bindt_TT: Bindt T T} :=
  { ktm_bindt0:
    forall `{Applicative G} (A B: Type) (f: A -> G (T B)),
      bindt f ∘ ret = f;
    ktm_premod :> TraversableRightPreModule T T;
  }.

Class TraversableRightModule (T U: Type -> Type)
  `{Return_T: Return T}
  `{Bindt_TT: Bindt T T}
  `{Bindt_TU: Bindt T U} :=
  { ktmod_monad :> TraversableMonad T;
    ktmod_premod :> TraversableRightPreModule T U;
  }.

#[local] Instance TraversableRightModule_TraversableMonad
  (T: Type -> Type)
  `{TraversableMonad_T: TraversableMonad T}:
  TraversableRightModule T T :=
  {| ktmod_premod := ktm_premod;
  |}.

(** ** Kleisli Category laws *)
(**********************************************************************)
Section Kleisli_composition.

  Context
    `{TraversableMonad T}
    `{Applicative G1}
    `{Applicative G2}
    `{Applicative G3}.

  Lemma kc6_id_l_I: forall `(g: A -> G2 (T B)),
      kc6 (T := T) (G1 := fun A => A) g (ret (T := T)) = g.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
forall (A B : Type) (g : A -> G2 (T B)), g ⋆6 ret = g
  Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
forall (A B : Type) (g : A -> G2 (T B)), g ⋆6 ret = g
    intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
A, B: Type
g: A -> G2 (T B)
g ⋆6 ret = g
    unfold kc6.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
A, B: Type
g: A -> G2 (T B)
map (bindt g) ∘ ret = g
    unfold_ops @Map_I.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
A, B: Type
g: A -> G2 (T B)
bindt g ∘ ret = g
    rewrite ktm_bindt0.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
A, B: Type
g: A -> G2 (T B)
g = g
    reflexivity.
  Qed.

  Lemma kc6_id_l: forall `(g: A -> G2 (T B)),
      kc6 (T := T) g (map (F := G1) ret) = map g.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
forall (A B : Type) (g : A -> G2 (T B)),
g ⋆6 map ret = map g
  Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
forall (A B : Type) (g : A -> G2 (T B)),
g ⋆6 map ret = map g
    intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
A, B: Type
g: A -> G2 (T B)
g ⋆6 map ret = map g
    unfold kc6.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
A, B: Type
g: A -> G2 (T B)
map (bindt g) ∘ map ret = map g
    rewrite (fun_map_map (F := G1)).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
A, B: Type
g: A -> G2 (T B)
map (bindt g ∘ ret) = map g
    rewrite ktm_bindt0.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
A, B: Type
g: A -> G2 (T B)
map g = map g
    reflexivity.
  Qed.

  Lemma kc6_id_r: forall `(f: A -> G1 (T B)),
      kc6 (T := T) (G2 := fun A => A) (ret (T := T)) f = f.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
forall (A B : Type) (f : A -> G1 (T B)), ret ⋆6 f = f
  Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
forall (A B : Type) (f : A -> G1 (T B)), ret ⋆6 f = f
    intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
A, B: Type
f: A -> G1 (T B)
ret ⋆6 f = f
    unfold kc6.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
A, B: Type
f: A -> G1 (T B)
map (bindt ret) ∘ f = f
    rewrite ktm_bindt1.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
A, B: Type
f: A -> G1 (T B)
map id ∘ f = f
    rewrite fun_map_id.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
A, B: Type
f: A -> G1 (T B)
id ∘ f = f
    reflexivity.
  Qed.

  Lemma kc6_assoc:
    forall `(h: C -> G3 (T D))
      `(g: B -> G2 (T C))
      `(f: A -> G1 (T B)),
      kc6 (G1 := G1 ∘ G2) h (g ⋆6 f) =
        kc6 (G2 := G2 ∘ G3) (h ⋆6 g) f.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
forall (C D : Type) (h : C -> G3 (T D)) (B : Type)
  (g : B -> G2 (T C)) (A : Type) (f : A -> G1 (T B)),
h ⋆6 (g ⋆6 f) = (h ⋆6 g) ⋆6 f
  Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
forall (C D : Type) (h : C -> G3 (T D)) (B : Type)
  (g : B -> G2 (T C)) (A : Type) (f : A -> G1 (T B)),
h ⋆6 (g ⋆6 f) = (h ⋆6 g) ⋆6 f
    intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
C, D: Type
h: C -> G3 (T D)
B: Type
g: B -> G2 (T C)
A: Type
f: A -> G1 (T B)
h ⋆6 (g ⋆6 f) = (h ⋆6 g) ⋆6 f
    unfold kc6.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
C, D: Type
h: C -> G3 (T D)
B: Type
g: B -> G2 (T C)
A: Type
f: A -> G1 (T B)
map (bindt h) ∘ (map (bindt g) ∘ f) =
map (bindt (map (bindt h) ∘ g)) ∘ f
    unfold_ops @Map_compose.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
C, D: Type
h: C -> G3 (T D)
B: Type
g: B -> G2 (T C)
A: Type
f: A -> G1 (T B)
map (map (bindt h)) ∘ (map (bindt g) ∘ f) =
map (bindt (map (bindt h) ∘ g)) ∘ f
    unfold_compose_in_compose.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
C, D: Type
h: C -> G3 (T D)
B: Type
g: B -> G2 (T C)
A: Type
f: A -> G1 (T B)
map (map (bindt h)) ∘ (map (bindt g) ∘ f) =
map (bindt (map (bindt h) ∘ g)) ∘ f
    ext a.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
C, D: Type
h: C -> G3 (T D)
B: Type
g: B -> G2 (T C)
A: Type
f: A -> G1 (T B)
a: A
(map (map (bindt h)) ∘ (map (bindt g) ∘ f)) a =
(map (bindt (map (bindt h) ∘ g)) ∘ f) a
    unfold compose at 1 2.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
C, D: Type
h: C -> G3 (T D)
B: Type
g: B -> G2 (T C)
A: Type
f: A -> G1 (T B)
a: A
map (map (bindt h)) (map (bindt g) (f a)) =
(map (bindt (map (bindt h) ∘ g)) ∘ f) a
    compose near (f a) on left.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
C, D: Type
h: C -> G3 (T D)
B: Type
g: B -> G2 (T C)
A: Type
f: A -> G1 (T B)
a: A
(map (map (bindt h)) ∘ map (bindt g)) (f a) =
(map (bindt (map (bindt h) ∘ g)) ∘ f) a
    rewrite fun_map_map.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
C, D: Type
h: C -> G3 (T D)
B: Type
g: B -> G2 (T C)
A: Type
f: A -> G1 (T B)
a: A
map (map (bindt h) ∘ bindt g) (f a) =
(map (bindt (map (bindt h) ∘ g)) ∘ f) a
    rewrite ktm_bindt2.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
C, D: Type
h: C -> G3 (T D)
B: Type
g: B -> G2 (T C)
A: Type
f: A -> G1 (T B)
a: A
map (bindt (h ⋆6 g)) (f a) =
(map (bindt (map (bindt h) ∘ g)) ∘ f) a
    unfold compose at 2 3.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H2: Applicative G3
C, D: Type
h: C -> G3 (T D)
B: Type
g: B -> G2 (T C)
A: Type
f: A -> G1 (T B)
a: A
map (bindt (h ⋆6 g)) (f a) =
map (bindt (map (bindt h) ∘ g)) (f a)
    reflexivity.
  Qed.

End Kleisli_composition.

(** * Derived Structures *)
(**********************************************************************)
From Tealeaves.Classes.Kleisli Require Import
  TraversableFunctor Monad.


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

    Context
      (T U: Type -> Type)
      `{Return_T: Return T}
      `{Bindt_TU: Bindt T U}.

    #[export] Instance Map_Bindt: Map U :=
      fun (A B: Type) (f: A -> B) =>
        bindt (G := fun A => A) (ret (T := T) ∘ f).

    #[export] Instance Bind_Bindt: Bind T U
      := fun A B f =>
           bindt (T := T) (G := fun A => A) f.

    #[export] Instance Traverse_Bindt: Traverse U
      := fun G _ _ _ A B f =>
           bindt (map (F := G) (ret (T := T)) ∘ f).

  End operations.
End DerivedOperations.

Section compat_classes.

  Context
    (T U: Type -> Type)
    `{Return_T: Return T}
    `{Map_U: Map U}
    `{Traverse_U: Traverse U}
    `{Bind_TU: Bind T U}
    `{Bindt_TU: Bindt T U}.

  Class Compat_Map_Bindt: Prop :=
    compat_map_bindt:
      Map_U = @DerivedOperations.Map_Bindt T U Return_T Bindt_TU.

  Class Compat_Bind_Bindt: Prop :=
    compat_bind_bindt:
      @Bind_TU = @DerivedOperations.Bind_Bindt T U Bindt_TU.

  Class Compat_Traverse_Bindt: Prop :=
    compat_traverse_bindt:
      forall (G: Type -> Type)
        `{Map_G: Map G}
        `{Pure_G: Pure G}
        `{Mult_G: Mult G}
        `{! Applicative G},
        @Traverse_U G Map_G Pure_G Mult_G =
          @DerivedOperations.Traverse_Bindt T U Return_T
            Bindt_TU G Map_G Pure_G Mult_G.

End compat_classes.

Section compat_instances.

  Context
    `{Return_T: Return T}
    `{Bindt_TU: Bindt T U}.

  #[export] Instance Compat_Map_Bindt_Self:
    Compat_Map_Bindt T U
      (Map_U := DerivedOperations.Map_Bindt T U).
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
Compat_Map_Bindt T U
  Proof.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
Compat_Map_Bindt T U
    reflexivity.
  Qed.

  #[export] Instance Compat_Bind_Bindt_Self:
    Compat_Bind_Bindt T U
      (Bind_TU := DerivedOperations.Bind_Bindt T U).
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
Compat_Bind_Bindt T U
  Proof.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
Compat_Bind_Bindt T U
    reflexivity.
  Qed.

  #[export] Instance Compat_Traverse_Bindt_Self:
    Compat_Traverse_Bindt T U
      (Traverse_U := DerivedOperations.Traverse_Bindt T U).
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
Compat_Traverse_Bindt T U
  Proof.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
Compat_Traverse_Bindt T U
    hnf.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
DerivedOperations.Traverse_Bindt T U G Map_G Pure_G
  Mult_G =
DerivedOperations.Traverse_Bindt T U G Map_G Pure_G
  Mult_G intros.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
Applicative0: Applicative G
DerivedOperations.Traverse_Bindt T U G Map_G Pure_G
  Mult_G =
DerivedOperations.Traverse_Bindt T U G Map_G Pure_G
  Mult_G
    reflexivity.
  Qed.

  #[export] Instance Compat_Map_Bind_Bindt
    `{Map U} `{Bind T U}
    `{! Compat_Bind_Bindt T U}
    `{! Compat_Map_Bindt T U}:
    Compat_Map_Bind T U.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
H: Map U
H0: Bind T U
Compat_Bind_Bindt0: Compat_Bind_Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
Compat_Map_Bind T U
  Proof.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
H: Map U
H0: Bind T U
Compat_Bind_Bindt0: Compat_Bind_Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
Compat_Map_Bind T U
    hnf.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
H: Map U
H0: Bind T U
Compat_Bind_Bindt0: Compat_Bind_Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H = DerivedOperations.Map_Bind T U
    rewrite (compat_map_bindt T U).
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
H: Map U
H0: Bind T U
Compat_Bind_Bindt0: Compat_Bind_Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
DerivedOperations.Map_Bindt T U =
DerivedOperations.Map_Bind T U
    unfold_ops @DerivedOperations.Map_Bind.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
H: Map U
H0: Bind T U
Compat_Bind_Bindt0: Compat_Bind_Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
DerivedOperations.Map_Bindt T U =
(fun A B : Type => bind ○ compose ret)
    rewrite (compat_bind_bindt T U).
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
H: Map U
H0: Bind T U
Compat_Bind_Bindt0: Compat_Bind_Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
DerivedOperations.Map_Bindt T U =
(fun A B : Type =>
 DerivedOperations.Bind_Bindt T U A B ○ compose ret)
    reflexivity.
  Qed.

  #[export] Instance Compat_Map_Traverse_Bindt
    `{Map U} `{Traverse U}
    `{! Compat_Traverse_Bindt T U}
    `{! Compat_Map_Bindt T U}:
    Compat_Map_Traverse U.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
H: Map U
H0: Traverse U
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
Compat_Map_Traverse U
  Proof.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
H: Map U
H0: Traverse U
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
Compat_Map_Traverse U
    hnf.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
H: Map U
H0: Traverse U
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
H = DerivedOperations.Map_Traverse U
    rewrite (compat_map_bindt T U).
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
H: Map U
H0: Traverse U
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
DerivedOperations.Map_Bindt T U =
DerivedOperations.Map_Traverse U
    unfold_ops @TraversableFunctor.DerivedOperations.Map_Traverse.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
H: Map U
H0: Traverse U
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
DerivedOperations.Map_Bindt T U =
(fun (A B : Type) (f : A -> B) => traverse f)
    rewrite (compat_traverse_bindt T U (fun A => A)).
T: Type -> Type
Return_T: Return T
U: Type -> Type
Bindt_TU: Bindt T U
H: Map U
H0: Traverse U
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
DerivedOperations.Map_Bindt T U =
DerivedOperations.Traverse_Bindt T U
  (fun A : Type => A) Map_I Pure_I Mult_I
    reflexivity.
  Qed.

End compat_instances.

Section rewriting_laws.

  Context
    `{Return_T: Return T}
    `{Map_U: Map U}
    `{Traverse_U: Traverse U}
    `{Bind_TU: Bind T U}
    `{Bindt_TU: Bindt T U}.

  Lemma map_to_bindt `{! Compat_Map_Bindt T U} `(f: A -> B):
      map (F := U) f =
        bindt (G := fun A => A) (ret (T := T) ∘ f).
T: Type -> Type
Return_T: Return T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
A, B: Type
f: A -> B
map f = bindt (ret ∘ f)
  Proof.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
A, B: Type
f: A -> B
map f = bindt (ret ∘ f)
    rewrite (compat_map_bindt T U).
T: Type -> Type
Return_T: Return T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt0: Compat_Map_Bindt T U
A, B: Type
f: A -> B
DerivedOperations.Map_Bindt T U A B f =
bindt (ret ∘ f)
    reflexivity.
  Qed.

  Lemma bind_to_bindt `{! Compat_Bind_Bindt T U} `(f: A -> T B):
    bind (U := U) f = bindt (G := fun A => A) f.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Bind_Bindt0: Compat_Bind_Bindt T U
A, B: Type
f: A -> T B
bind f = bindt f
  Proof.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Bind_Bindt0: Compat_Bind_Bindt T U
A, B: Type
f: A -> T B
bind f = bindt f
    rewrite (compat_bind_bindt T U).
T: Type -> Type
Return_T: Return T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Bind_Bindt0: Compat_Bind_Bindt T U
A, B: Type
f: A -> T B
DerivedOperations.Bind_Bindt T U A B f = bindt f
    reflexivity.
  Qed.

  Lemma traverse_to_bindt `{! Compat_Traverse_Bindt T U}
    `{Applicative G} `(f: A -> G B):
    traverse (G := G) (T := U) f =
      bindt (U := U) (map (F := G) (ret (T := T)) ∘ f).
T: Type -> Type
Return_T: Return T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
traverse f = bindt (map ret ∘ f)
  Proof.
T: Type -> Type
Return_T: Return T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
traverse f = bindt (map ret ∘ f)
    rewrite (compat_traverse_bindt T U G).
T: Type -> Type
Return_T: Return T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
DerivedOperations.Traverse_Bindt T U G Map_G Pure_G
  Mult_G A B f = bindt (map ret ∘ f)
    reflexivity.
  Qed.

End rewriting_laws.

(** ** Composition with the Identity Applicative *)
(**********************************************************************)
Section traversable_monad_identity_applicative.

  Context
    `{TraversableRightModule T U}.

  Lemma bindt_app_id_l:
    forall {A B: Type} `{Applicative G} (f: A -> G (T B)),
      @bindt T U _ ((fun A => A) ∘ G)
        (Map_compose (fun A => A) G)
        (Pure_compose (fun A => A) G)
        (Mult_compose (fun A => A) G) A B f =
        bindt (G := G) f.
T, U: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
Bindt_TU: Bindt T U
H: TraversableRightModule T U
forall (A B : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall f : A -> G (T B), bindt f = bindt f
  Proof.
T, U: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
Bindt_TU: Bindt T U
H: TraversableRightModule T U
forall (A B : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall f : A -> G (T B), bindt f = bindt f
    intros.
T, U: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
Bindt_TU: Bindt T U
H: TraversableRightModule T U
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: A -> G (T B)
bindt f = bindt f fequal.
T, U: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
Bindt_TU: Bindt T U
H: TraversableRightModule T U
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: A -> G (T B)
Mult_compose (fun A : Type => A) G = Mult_G now rewrite (Mult_compose_identity2 G).
  Qed.

  Lemma bindt_app_id_r:
    forall {A B: Type} `{Applicative G} (f: A -> G (T B)),
      @bindt T U _ (G ∘ (fun A => A))
        (Map_compose G (fun A => A))
        (Pure_compose G (fun A => A))
        (Mult_compose G (fun A => A)) A B f =
        bindt (G := G) f.
T, U: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
Bindt_TU: Bindt T U
H: TraversableRightModule T U
forall (A B : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall f : A -> G (T B), bindt f = bindt f
  Proof.
T, U: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
Bindt_TU: Bindt T U
H: TraversableRightModule T U
forall (A B : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall f : A -> G (T B), bindt f = bindt f
    intros.
T, U: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
Bindt_TU: Bindt T U
H: TraversableRightModule T U
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: A -> G (T B)
bindt f = bindt f fequal.
T, U: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
Bindt_TU: Bindt T U
H: TraversableRightModule T U
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: A -> G (T B)
Mult_compose G (fun A : Type => A) = Mult_G now rewrite (Mult_compose_identity1 G).
  Qed.

End traversable_monad_identity_applicative.

(** ** Derived Kleisli Composition Laws *)
(**********************************************************************)
Section traversable_monad_derived_kleisli_composition_laws.

  Context
    `{Return_T: Return T}
    `{Map_T: Map T}
    `{Traverse_T: Traverse T}
    `{Bind_T: Bind T T}
    `{Bindt_TT: Bindt T T}
    `{! Compat_Map_Bindt T T}
    `{! Compat_Traverse_Bindt T T}
    `{! Compat_Bind_Bindt T T}
    `{! TraversableMonad T}.

  Import Kleisli.Monad.Notations.
  Import Kleisli.TraversableFunctor.Notations.

  Context
    `{Applicative G1}
    `{Applicative G2}
    `{Applicative G3}.

  Context (A B C: Type).

  (** *** Homogeneous cases *)
  (********************************************************************)
  Lemma kc6_22: forall (g: B -> G2 C) (f: A -> G1 B),
      (map ret ∘ g) ⋆6 (map ret ∘ f) =
        map (F := G1 ∘ G2) ret ∘ map (F := G1) g ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 C) (f : A -> G1 B),
map ret ∘ g ⋆6 map ret ∘ f = map ret ∘ map g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 C) (f : A -> G1 B),
map ret ∘ g ⋆6 map ret ∘ f = map ret ∘ map g ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map ret ∘ g ⋆6 map ret ∘ f = map ret ∘ map g ∘ f unfold kc6.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (bindt (map ret ∘ g)) ∘ (map ret ∘ f) =
map ret ∘ map g ∘ f
    reassociate <-.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (bindt (map ret ∘ g)) ∘ map ret ∘ f =
map ret ∘ map g ∘ f
    rewrite fun_map_map.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (bindt (map ret ∘ g) ∘ ret) ∘ f =
map ret ∘ map g ∘ f
    unfold_ops @Map_compose.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (bindt (map ret ∘ g) ∘ ret) ∘ f =
map (map ret) ∘ map g ∘ f
    unfold_compose_in_compose.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (bindt (map ret ∘ g) ∘ ret) ∘ f =
map (map ret) ∘ map g ∘ f
    rewrite fun_map_map.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (bindt (map ret ∘ g) ∘ ret) ∘ f =
map (map ret ∘ g) ∘ f
    rewrite ktm_bindt0.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (map ret ∘ g) ∘ f = map (map ret ∘ g) ∘ f
    reflexivity.
  Qed.

  Lemma kc6_44: forall (g: B -> T C) (f: A -> T B),
      kc6 (G1 := fun A => A) (G2 := fun A => A) g f = (g ⋆ f).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> T C) (f : A -> T B), g ⋆6 f = g ⋆ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> T C) (f : A -> T B), g ⋆6 f = g ⋆ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> T B
g ⋆6 f = g ⋆ f unfold kc6, kc.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> T B
map (bindt g) ∘ f = bind g ∘ f
    rewrite (bind_to_bindt (T := T)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> T B
map (bindt g) ∘ f = bindt g ∘ f
    reflexivity.
  Qed.

  Lemma kc6_00: forall (g: B -> C) (f: A -> B),
      kc6 (T := T) (G1 := fun A => A) (G2 := fun A => A)
        (ret ∘ g) (ret ∘ f) = ret ∘ g ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> C) (f : A -> B),
ret ∘ g ⋆6 ret ∘ f = ret ∘ g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> C) (f : A -> B),
ret ∘ g ⋆6 ret ∘ f = ret ∘ g ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> B
ret ∘ g ⋆6 ret ∘ f = ret ∘ g ∘ f unfold kc6.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> B
map (bindt (ret ∘ g)) ∘ (ret ∘ f) = ret ∘ g ∘ f
    reassociate <-.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> B
map (bindt (ret ∘ g)) ∘ ret ∘ f = ret ∘ g ∘ f
    change (map (F := fun A => A) ?f) with f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> B
bindt (ret ∘ g) ∘ ret ∘ f = ret ∘ g ∘ f
    rewrite (ktm_bindt0 (G := fun A => A)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> B
ret ∘ g ∘ f = ret ∘ g ∘ f
    reflexivity.
  Qed.

  (** *** Heterogeneous cases *)
  (********************************************************************)
  Lemma kc6_64: forall (g: B -> G2 (T C)) (f: A -> T B),
      kc6 (G1 := fun A => A) (G2 := G2) g f = bindt (G := G2) g ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 (T C)) (f : A -> T B),
g ⋆6 f = bindt g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 (T C)) (f : A -> T B),
g ⋆6 f = bindt g ∘ f
    reflexivity.
  Qed.

  Lemma kc6_62: forall (g: B -> G2 (T C)) (f: A -> G1 B),
      g ⋆6 map ret ∘ f = map g ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 (T C)) (f : A -> G1 B),
g ⋆6 map ret ∘ f = map g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 (T C)) (f : A -> G1 B),
g ⋆6 map ret ∘ f = map g ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 B
g ⋆6 map ret ∘ f = map g ∘ f unfold kc6.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 B
map (bindt g) ∘ (map ret ∘ f) = map g ∘ f
    reassociate <-.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 B
map (bindt g) ∘ map ret ∘ f = map g ∘ f
    rewrite fun_map_map.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 B
map (bindt g ∘ ret) ∘ f = map g ∘ f
    rewrite ktm_bindt0.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 B
map g ∘ f = map g ∘ f
    reflexivity.
  Qed.

  Lemma kc6_60: forall (g: B -> G2 (T C)) (f: A -> B),
      kc6 (T := T) (G1 := fun A => A) (G2 := G2) g (ret ∘ f) = g ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 (T C)) (f : A -> B),
g ⋆6 ret ∘ f = g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 (T C)) (f : A -> B),
g ⋆6 ret ∘ f = g ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 (T C)
f: A -> B
g ⋆6 ret ∘ f = g ∘ f unfold kc6.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 (T C)
f: A -> B
map (bindt g) ∘ (ret ∘ f) = g ∘ f reassociate <-.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 (T C)
f: A -> B
map (bindt g) ∘ ret ∘ f = g ∘ f
    change (map (F := fun A => A) ?f) with f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 (T C)
f: A -> B
bindt g ∘ ret ∘ f = g ∘ f
    rewrite ktm_bindt0.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 (T C)
f: A -> B
g ∘ f = g ∘ f
    reflexivity.
  Qed.

  Lemma kc6_46: forall (g: B -> T C) (f: A -> G1 (T B)),
      kc6 (G2 := fun A => A) g f =
        map (F := G1) (bind (T := T) g) ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> T C) (f : A -> G1 (T B)),
g ⋆6 f = map (bind g) ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> T C) (f : A -> G1 (T B)),
g ⋆6 f = map (bind g) ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> G1 (T B)
g ⋆6 f = map (bind g) ∘ f
    rewrite (bind_to_bindt (T := T)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> G1 (T B)
g ⋆6 f = map (bindt g) ∘ f
    reflexivity.
  Qed.

  Lemma kc6_26: forall (g: B -> G2 C) (f: A -> G1 (T B)),
      map ret ∘ g ⋆6 f = map (traverse g) ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 C) (f : A -> G1 (T B)),
map ret ∘ g ⋆6 f = map (traverse g) ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 C) (f : A -> G1 (T B)),
map ret ∘ g ⋆6 f = map (traverse g) ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> G1 (T B)
map ret ∘ g ⋆6 f = map (traverse g) ∘ f
    rewrite traverse_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> G1 (T B)
map ret ∘ g ⋆6 f = map (bindt (map ret ∘ g)) ∘ f
    reflexivity.
  Qed.

  Lemma kc6_06: forall (g: B -> C) (f: A -> G1 (T B)),
      kc6 (T := T) (G2 := fun A => A) (ret ∘ g) f = map (map g) ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> C) (f : A -> G1 (T B)),
ret ∘ g ⋆6 f = map (map g) ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> C) (f : A -> G1 (T B)),
ret ∘ g ⋆6 f = map (map g) ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> G1 (T B)
ret ∘ g ⋆6 f = map (map g) ∘ f
    rewrite (map_to_bindt (T := T) (U := T)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> G1 (T B)
ret ∘ g ⋆6 f = map (bindt (ret ∘ g)) ∘ f
    reflexivity.
  Qed.

  Lemma kc6_42: forall (g: B -> T C) (f: A -> G1 B),
      kc6 (T := T) (G2 := fun A => A) g (map ret ∘ f) = map g ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> T C) (f : A -> G1 B),
g ⋆6 map ret ∘ f = map g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> T C) (f : A -> G1 B),
g ⋆6 map ret ∘ f = map g ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> G1 B
g ⋆6 map ret ∘ f = map g ∘ f
    unfold kc6.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> G1 B
map (bindt g) ∘ (map ret ∘ f) = map g ∘ f
    reassociate <-.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> G1 B
map (bindt g) ∘ map ret ∘ f = map g ∘ f
    rewrite fun_map_map.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> G1 B
map (bindt g ∘ ret) ∘ f = map g ∘ f
    rewrite (ktm_bindt0 (G := fun A => A)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> G1 B
map g ∘ f = map g ∘ f
    reflexivity.
  Qed.

  Lemma kc6_24: forall (g: B -> G2 C) (f: A -> T B),
      kc6 (map ret ∘ g) f = traverse (G := G2) g ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 C) (f : A -> T B),
map ret ∘ g ⋆6 f = traverse g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 C) (f : A -> T B),
map ret ∘ g ⋆6 f = traverse g ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> T B
map ret ∘ g ⋆6 f = traverse g ∘ f
    unfold kc6.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> T B
map (bindt (map ret ∘ g)) ∘ f = traverse g ∘ f
    rewrite traverse_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> T B
map (bindt (map ret ∘ g)) ∘ f =
bindt (map ret ∘ g) ∘ f
    reflexivity.
  Qed.

  Lemma kc6_20: forall (g: B -> G2 C) (f: A -> B),
      kc6 (T := T) (G1 := fun A => A) (map ret ∘ g) (ret ∘ f) =
        map ret ∘ g ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 C) (f : A -> B),
map ret ∘ g ⋆6 ret ∘ f = map ret ∘ g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> G2 C) (f : A -> B),
map ret ∘ g ⋆6 ret ∘ f = map ret ∘ g ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> B
map ret ∘ g ⋆6 ret ∘ f = map ret ∘ g ∘ f
    unfold kc6.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> B
map (bindt (map ret ∘ g)) ∘ (ret ∘ f) =
map ret ∘ g ∘ f
    reassociate <-.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> B
map (bindt (map ret ∘ g)) ∘ ret ∘ f = map ret ∘ g ∘ f
    change (map (F := fun A => A) ?f) with f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> B
bindt (map ret ∘ g) ∘ ret ∘ f = map ret ∘ g ∘ f
    rewrite ktm_bindt0.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> G2 C
f: A -> B
map ret ∘ g ∘ f = map ret ∘ g ∘ f
    reflexivity.
  Qed.

  Lemma kc6_02: forall (g: B -> C) (f: A -> G1 B),
      kc6 (T := T) (G2 := fun A => A) (ret ∘ g) (map ret ∘ f) =
        map ret ∘ map g ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> C) (f : A -> G1 B),
ret ∘ g ⋆6 map ret ∘ f = map ret ∘ map g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> C) (f : A -> G1 B),
ret ∘ g ⋆6 map ret ∘ f = map ret ∘ map g ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> G1 B
ret ∘ g ⋆6 map ret ∘ f = map ret ∘ map g ∘ f
    unfold kc6.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> G1 B
map (bindt (ret ∘ g)) ∘ (map ret ∘ f) =
map ret ∘ map g ∘ f
    reassociate <-.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> G1 B
map (bindt (ret ∘ g)) ∘ map ret ∘ f =
map ret ∘ map g ∘ f
    rewrite fun_map_map.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> G1 B
map (bindt (ret ∘ g) ∘ ret) ∘ f = map ret ∘ map g ∘ f
    rewrite fun_map_map.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> G1 B
map (bindt (ret ∘ g) ∘ ret) ∘ f = map (ret ∘ g) ∘ f
    rewrite (ktm_bindt0 (G := fun A => A)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> G1 B
map (ret ∘ g) ∘ f = map (ret ∘ g) ∘ f
    reflexivity.
  Qed.

  Lemma kc6_04: forall (g: B -> C) (f: A -> T B),
      kc6 (T := T) (G1 := fun A => A) (G2 := fun A => A) (ret ∘ g) f =
        map g ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> C) (f : A -> T B),
ret ∘ g ⋆6 f = map g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> C) (f : A -> T B),
ret ∘ g ⋆6 f = map g ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> T B
ret ∘ g ⋆6 f = map g ∘ f
    unfold kc6.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> T B
map (bindt (ret ∘ g)) ∘ f = map g ∘ f
    rewrite (map_to_bindt (U := T) (T := T)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> C
f: A -> T B
map (bindt (ret ∘ g)) ∘ f = bindt (ret ∘ g) ∘ f
    reflexivity.
  Qed.

  Lemma kc6_40: forall (g: B -> T C) (f: A -> B),
      kc6 (T := T) (G1 := fun A => A) (G2 := fun A => A) g (ret ∘ f) =
        g ∘ f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> T C) (f : A -> B),
g ⋆6 ret ∘ f = g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
forall (g : B -> T C) (f : A -> B),
g ⋆6 ret ∘ f = g ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> B
g ⋆6 ret ∘ f = g ∘ f
    unfold kc6.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> B
map (bindt g) ∘ (ret ∘ f) = g ∘ f
    reassociate <-.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> B
map (bindt g) ∘ ret ∘ f = g ∘ f
    change (map (F := fun A => A) ?f) with f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> B
bindt g ∘ ret ∘ f = g ∘ f
    rewrite (ktm_bindt0 (G := fun A => A)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
G3: Type -> Type
Map_G1: Map G3
Pure_G1: Pure G3
Mult_G1: Mult G3
H1: Applicative G3
A, B, C: Type
g: B -> T C
f: A -> B
g ∘ f = g ∘ f
    reflexivity.
  Qed.

End traversable_monad_derived_kleisli_composition_laws.

(** ** Derived Composition Laws *)
(**********************************************************************)
Section traversable_monad_derived_composition_laws.

  Import Kleisli.Monad.Notations.
  Import Kleisli.TraversableFunctor.Notations.

  Context
    `{Return_T: Return T}
    `{Map_T: Map T}
    `{Traverse_T: Traverse T}
    `{Bind_T: Bind T T}
    `{Bindt_TT: Bindt T T}
    `{! Compat_Map_Bindt T T}
    `{! Compat_Traverse_Bindt T T}
    `{! Compat_Bind_Bindt T T}
    `{! TraversableMonad T}.

  Context
    `{Map_U: Map U}
    `{Traverse_U: Traverse U}
    `{Bind_TU: Bind T U}
    `{Bindt_TU: Bindt T U}
    `{! Compat_Map_Bindt T U}
    `{! Compat_Traverse_Bindt T U}
    `{! Compat_Bind_Bindt T U}
    `{! TraversableRightPreModule T U}.

  Context
    `{Applicative G1}
    `{Applicative G2}
    (A B C: Type).

  (** *** Composition with <<traverse>> *)
  (********************************************************************)
  Lemma traverse_bindt: forall (g: B -> G2 C) (f: A -> G1 (T B)),
      map (traverse g) ∘ bindt f =
        bindt (U := U) (G := G1 ∘ G2) (map (traverse g) ∘ f).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : A -> G1 (T B)),
map (traverse g) ∘ bindt f =
bindt (map (traverse g) ∘ f)
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : A -> G1 (T B)),
map (traverse g) ∘ bindt f =
bindt (map (traverse g) ∘ f)
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 (T B)
map (traverse g) ∘ bindt f =
bindt (map (traverse g) ∘ f)
    rewrite traverse_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 (T B)
map (bindt (map ret ∘ g)) ∘ bindt f =
bindt (map (traverse g) ∘ f)
    rewrite traverse_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 (T B)
map (bindt (map ret ∘ g)) ∘ bindt f =
bindt (map (bindt (map ret ∘ g)) ∘ f)
    rewrite ktm_bindt2.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 (T B)
bindt (map ret ∘ g ⋆6 f) =
bindt (map (bindt (map ret ∘ g)) ∘ f)
    reflexivity.
  Qed.

  Lemma bindt_traverse: forall (g: B -> G2 (T C)) (f: A -> G1 B),
      map (bindt g) ∘ traverse f =
        bindt (U := U) (G := G1 ∘ G2) (map g ∘ f).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 (T C)) (f : A -> G1 B),
map (bindt g) ∘ traverse f = bindt (map g ∘ f)
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 (T C)) (f : A -> G1 B),
map (bindt g) ∘ traverse f = bindt (map g ∘ f)
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 B
map (bindt g) ∘ traverse f = bindt (map g ∘ f)
    rewrite traverse_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 B
map (bindt g) ∘ bindt (map ret ∘ f) =
bindt (map g ∘ f)
    rewrite ktm_bindt2.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 B
bindt (g ⋆6 map ret ∘ f) = bindt (map g ∘ f)
    rewrite kc6_62.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 B
bindt (map g ∘ f) = bindt (map g ∘ f)
    reflexivity.
  Qed.

  (** *** Composition with <<bind>> *)
  (********************************************************************)
  Lemma bind_bindt: forall (g: B -> T C) (f: A -> G1 (T B)),
      map (bind g) ∘ bindt f = bindt (U := U) (map (bind g) ∘ f).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> T C) (f : A -> G1 (T B)),
map (bind g) ∘ bindt f = bindt (map (bind g) ∘ f)
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> T C) (f : A -> G1 (T B)),
map (bind g) ∘ bindt f = bindt (map (bind g) ∘ f)
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> G1 (T B)
map (bind g) ∘ bindt f = bindt (map (bind g) ∘ f)
    rewrite (bind_to_bindt (U := T)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> G1 (T B)
map (bind g) ∘ bindt f = bindt (map (bindt g) ∘ f)
    rewrite (bind_to_bindt (U := U)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> G1 (T B)
map (bindt g) ∘ bindt f = bindt (map (bindt g) ∘ f)
    rewrite (ktm_bindt2 (G2 := fun A => A)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> G1 (T B)
bindt (g ⋆6 f) = bindt (map (bindt g) ∘ f)
    rewrite bindt_app_id_r.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> G1 (T B)
bindt (g ⋆6 f) = bindt (map (bindt g) ∘ f)
    reflexivity.
  Qed.

  Lemma bindt_bind: forall (g: B -> G2 (T C)) (f: A -> T B),
      bindt g ∘ bind f = bindt (U := U) (bindt g ∘ f).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 (T C)) (f : A -> T B),
bindt g ∘ bind f = bindt (bindt g ∘ f)
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 (T C)) (f : A -> T B),
bindt g ∘ bind f = bindt (bindt g ∘ f)
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> T B
bindt g ∘ bind f = bindt (bindt g ∘ f)
    rewrite bind_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> T B
bindt g ∘ bindt f = bindt (bindt g ∘ f)
    change (bindt (U := U) g) with
      (map (F := fun A => A) (bindt (U := U) g)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> T B
map (bindt g) ∘ bindt f = bindt (bindt g ∘ f)
    rewrite (ktm_bindt2 (G1 := fun A => A)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> T B
bindt (g ⋆6 f) = bindt (bindt g ∘ f)
    rewrite bindt_app_id_l.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> T B
bindt (g ⋆6 f) = bindt (bindt g ∘ f)
    reflexivity.
  Qed.

  (** *** Composition with <<map>> *)
  (********************************************************************)
  Lemma map_bindt: forall (g: B -> C) (f: A -> G1 (T B)),
      map (map g) ∘ bindt f = bindt (map (map g) ∘ f).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> C) (f : A -> G1 (T B)),
map (map g) ∘ bindt f = bindt (map (map g) ∘ f)
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> C) (f : A -> G1 (T B)),
map (map g) ∘ bindt f = bindt (map (map g) ∘ f)
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: A -> G1 (T B)
map (map g) ∘ bindt f = bindt (map (map g) ∘ f)
    rewrite (map_to_bindt (U := T)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: A -> G1 (T B)
map (map g) ∘ bindt f =
bindt (map (bindt (ret ∘ g)) ∘ f)
    rewrite (map_to_bindt (U := U)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: A -> G1 (T B)
map (bindt (ret ∘ g)) ∘ bindt f =
bindt (map (bindt (ret ∘ g)) ∘ f)
    rewrite (ktm_bindt2 (G2 := fun A => A)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: A -> G1 (T B)
bindt (ret ∘ g ⋆6 f) =
bindt (map (bindt (ret ∘ g)) ∘ f)
    rewrite bindt_app_id_r.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: A -> G1 (T B)
bindt (ret ∘ g ⋆6 f) =
bindt (map (bindt (ret ∘ g)) ∘ f)
    reflexivity.
  Qed.

  Lemma bindt_map: forall (g: B -> G2 (T C)) (f: A -> B),
      bindt g ∘ map f = bindt (U := U) (g ∘ f).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 (T C)) (f : A -> B),
bindt g ∘ map f = bindt (g ∘ f)
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 (T C)) (f : A -> B),
bindt g ∘ map f = bindt (g ∘ f)
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> B
bindt g ∘ map f = bindt (g ∘ f)
    rewrite (map_to_bindt (T := T) (U := U)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> B
bindt g ∘ bindt (ret ∘ f) = bindt (g ∘ f)
    change (bindt g) with (map (F := fun A => A) (bindt g)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> B
map (bindt g) ∘ bindt (ret ∘ f) = bindt (g ∘ f)
    rewrite (ktm_bindt2 (G1 := fun A => A)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> B
bindt (g ⋆6 ret ∘ f) = bindt (g ∘ f)
    rewrite bindt_app_id_l.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> B
bindt (g ⋆6 ret ∘ f) = bindt (g ∘ f)
    rewrite kc6_60.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> B
bindt (g ∘ f) = bindt (g ∘ f)
    reflexivity.
  Qed.

  (** *** Composition between <<traverse>> and <<bind>> *)
  (********************************************************************)
  Lemma traverse_bind: forall (g: B -> G2 C) (f: A -> T B),
      traverse g ∘ bind f = bindt (traverse g ∘ f).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : A -> T B),
traverse g ∘ bind f = bindt (traverse g ∘ f)
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : A -> T B),
traverse g ∘ bind f = bindt (traverse g ∘ f)
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> T B
traverse g ∘ bind f = bindt (traverse g ∘ f)
    rewrite traverse_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> T B
bindt (map ret ∘ g) ∘ bind f = bindt (traverse g ∘ f)
    rewrite (bind_to_bindt (U := U)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> T B
bindt (map ret ∘ g) ∘ bindt f = bindt (traverse g ∘ f)
    change (bindt ?g) with (map (F := fun A => A) (bindt g)) at 1.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> T B
map (bindt (map ret ∘ g)) ∘ bindt f =
bindt (traverse g ∘ f)
    rewrite (ktm_bindt2 (G1 := fun A => A)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> T B
bindt (map ret ∘ g ⋆6 f) = bindt (traverse g ∘ f)
    rewrite bindt_app_id_l.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> T B
bindt (map ret ∘ g ⋆6 f) = bindt (traverse g ∘ f)
    rewrite kc6_24.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> T B
bindt (traverse g ∘ f) = bindt (traverse g ∘ f)
    rewrite traverse_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> T B
bindt (bindt (map ret ∘ g) ∘ f) =
bindt (bindt (map ret ∘ g) ∘ f)
    reflexivity.
  Qed.

  Lemma bind_traverse: forall (g: B -> T C) (f: A -> G1 B),
      map (bind g) ∘ traverse f = bindt (map g ∘ f).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> T C) (f : A -> G1 B),
map (bind g) ∘ traverse f = bindt (map g ∘ f)
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> T C) (f : A -> G1 B),
map (bind g) ∘ traverse f = bindt (map g ∘ f)
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> G1 B
map (bind g) ∘ traverse f = bindt (map g ∘ f)
    rewrite traverse_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> G1 B
map (bind g) ∘ bindt (map ret ∘ f) = bindt (map g ∘ f)
    rewrite (bind_to_bindt (U := U)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> G1 B
map (bindt g) ∘ bindt (map ret ∘ f) =
bindt (map g ∘ f)
    rewrite (ktm_bindt2 (G2 := fun A => A)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> G1 B
bindt (g ⋆6 map ret ∘ f) = bindt (map g ∘ f)
    rewrite bindt_app_id_r.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> G1 B
bindt (g ⋆6 map ret ∘ f) = bindt (map g ∘ f)
    rewrite kc6_42.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> G1 B
bindt (map g ∘ f) = bindt (map g ∘ f)
    reflexivity.
  Qed.

  (** ** Monad Laws *)
  (********************************************************************)
  Lemma bind_ret: forall (A B: Type) (f: A -> T B),
      bind f ∘ ret = f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (A B : Type) (f : A -> T B), bind f ∘ ret = f
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (A B : Type) (f : A -> T B), bind f ∘ ret = f
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0, B0: Type
f: A0 -> T B0
bind f ∘ ret = f
    rewrite bind_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0, B0: Type
f: A0 -> T B0
bindt f ∘ ret = f
    rewrite (ktm_bindt0 (G := fun A => A)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0, B0: Type
f: A0 -> T B0
f = f
    reflexivity.
  Qed.

  Lemma bind_id: forall (A: Type),
      bind ret = @id (U A).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall A : Type, bind ret = id
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall A : Type, bind ret = id
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
bind ret = id
    rewrite bind_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
bindt ret = id
    rewrite ktm_bindt1.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
id = id
    reflexivity.
  Qed.

  Lemma bind_bind: forall (g: B -> T C) (f: A -> T B),
      bind g ∘ bind f = bind (U := U) (g ⋆ f).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> T C) (f : A -> T B),
bind g ∘ bind f = bind (g ⋆ f)
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> T C) (f : A -> T B),
bind g ∘ bind f = bind (g ⋆ f)
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> T B
bind g ∘ bind f = bind (g ⋆ f)
    do 2 rewrite bind_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> T B
bindt g ∘ bindt f = bind (g ⋆ f)
    change (bindt g) with (map (F := fun A => A) (bindt g)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> T B
map (bindt g) ∘ bindt f = bind (g ⋆ f)
    change ((fun A => A) ?x) with x.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> T B
map (bindt g) ∘ bindt f = bind (g ⋆ f)
    rewrite (ktm_bindt2 (G1 := fun A => A) (G2 := fun A => A)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> T B
bindt (g ⋆6 f) = bind (g ⋆ f)
    rewrite bindt_app_id_r.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> T B
bindt (g ⋆6 f) = bind (g ⋆ f)
    rewrite kc6_44.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> T B
bindt (g ⋆ f) = bind (g ⋆ f)
    rewrite bind_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> T C
f: A -> T B
bindt (g ⋆ f) = bindt (g ⋆ f)
    reflexivity.
  Qed.

  (** ** Traversable Laws *)
  (********************************************************************)
  Lemma traverse_id: forall (A: Type),
      traverse (G := fun A => A) (@id A) = @id (U A).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall A : Type, traverse id = id
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall A : Type, traverse id = id
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
traverse id = id
    rewrite (traverse_to_bindt (G := fun A => A)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
bindt (map ret ∘ id) = id
    change (?g ∘ id) with g.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
bindt (map ret) = id
    change (map (F := fun A => A) ?f) with f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
bindt ret = id
    rewrite ktm_bindt1.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
id = id
    reflexivity.
  Qed.

  Lemma traverse_traverse:
    forall (g: B -> G2 C) (f: A -> G1 B),
      map (traverse g) ∘ traverse f =
        traverse (T := U) (G := G1 ∘ G2) (map g ∘ f).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : A -> G1 B),
map (traverse g) ∘ traverse f = traverse (map g ∘ f)
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : A -> G1 B),
map (traverse g) ∘ traverse f = traverse (map g ∘ f)
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (traverse g) ∘ traverse f = traverse (map g ∘ f)
    rewrite traverse_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (bindt (map ret ∘ g)) ∘ traverse f =
traverse (map g ∘ f)
    rewrite traverse_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (bindt (map ret ∘ g)) ∘ bindt (map ret ∘ f) =
traverse (map g ∘ f)
    rewrite ktm_bindt2.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
bindt (map ret ∘ g ⋆6 map ret ∘ f) =
traverse (map g ∘ f)
    rewrite kc6_22.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
bindt (map ret ∘ map g ∘ f) = traverse (map g ∘ f)
    rewrite traverse_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
bindt (map ret ∘ map g ∘ f) =
bindt (map ret ∘ (map g ∘ f))
    reflexivity.
  Qed.

  Lemma traverse_morphism:
    forall `{! ApplicativeMorphism G1 G2 ϕ} (A B: Type) (f: A -> G1 B),
      ϕ (U B) ∘ traverse f = traverse (ϕ B ∘ f).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall ϕ : forall A : Type, G1 A -> G2 A,
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : A -> G1 B),
ϕ (U B) ∘ traverse f = traverse (ϕ B ∘ f)
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall ϕ : forall A : Type, G1 A -> G2 A,
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : A -> G1 B),
ϕ (U B) ∘ traverse f = traverse (ϕ B ∘ f)
    intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
ϕ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ϕ
A0, B0: Type
f: A0 -> G1 B0
ϕ (U B0) ∘ traverse f = traverse (ϕ B0 ∘ f)
    infer_applicative_instances.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
ϕ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ϕ
A0, B0: Type
f: A0 -> G1 B0
app1: Applicative G1
app2: Applicative G2
ϕ (U B0) ∘ traverse f = traverse (ϕ B0 ∘ f)
    rewrite traverse_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
ϕ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ϕ
A0, B0: Type
f: A0 -> G1 B0
app1: Applicative G1
app2: Applicative G2
ϕ (U B0) ∘ bindt (map ret ∘ f) = traverse (ϕ B0 ∘ f)
    rewrite traverse_to_bindt.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
ϕ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ϕ
A0, B0: Type
f: A0 -> G1 B0
app1: Applicative G1
app2: Applicative G2
ϕ (U B0) ∘ bindt (map ret ∘ f) =
bindt (map ret ∘ (ϕ B0 ∘ f))
    rewrite ktm_morph.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
ϕ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ϕ
A0, B0: Type
f: A0 -> G1 B0
app1: Applicative G1
app2: Applicative G2
bindt (ϕ (T B0) ∘ (map ret ∘ f)) =
bindt (map ret ∘ (ϕ B0 ∘ f))
    reassociate <-.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
ϕ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ϕ
A0, B0: Type
f: A0 -> G1 B0
app1: Applicative G1
app2: Applicative G2
bindt (ϕ (T B0) ∘ map ret ∘ f) =
bindt (map ret ∘ (ϕ B0 ∘ f))
    rewrite appmor_natural_pf.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_T: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U: Map U
Traverse_U: Traverse U
Bind_TU: Bind T U
Bindt_TU: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
ϕ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ϕ
A0, B0: Type
f: A0 -> G1 B0
app1: Applicative G1
app2: Applicative G2
bindt (map ret ∘ ϕ B0 ∘ f) =
bindt (map ret ∘ (ϕ B0 ∘ f))
    reflexivity.
  Qed.

End traversable_monad_derived_composition_laws.

(** ** Derived Typeclass Instances *)
(**********************************************************************)
Module DerivedInstances.

  Section instances.

    Context
      `{Return_T: Return T}
      `{Map_T: Map T}
      `{Traverse_T: Traverse T}
      `{Bind_TT: Bind T T}
      `{Bindt_TT: Bindt T T}
      `{! Compat_Map_Bindt T T}
      `{! Compat_Traverse_Bindt T T}
      `{! Compat_Bind_Bindt T T}
      `{! TraversableMonad T}.

    #[export] Instance TraversableFunctor_TraversableMonad:
      TraversableFunctor T.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
TraversableFunctor T
    Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
TraversableFunctor T
      constructor; intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
A: Type
traverse id = id
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (traverse g) ∘ traverse f = traverse (kc2 g f)
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f)
      -
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
A: Type
traverse id = id apply traverse_id.
      -
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (traverse g) ∘ traverse f = traverse (kc2 g f) apply traverse_traverse.
      -
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f) apply traverse_morphism.
    Qed.

    #[export] Instance RightPreModule_TraversableMonad:
      RightPreModule T T :=
      {| kmod_bind1 := bind_id;
         kmod_bind2 := bind_bind;
      |}.

    #[export] Instance Monad_TraversableMonad: Monad T :=
      {| kmon_bind0 := bind_ret;
      |}.

    #[local] Instance TraversableRightModule_TraversableMonad:
      TraversableRightModule T T :=
      {| ktmod_monad := _;
      |}.

    (*
      #[export] Instance Functor_TraversableMonad: Functor T
      := DerivedInstances.Functor_TraversableFunctor.
     (* or DerivedInstances.Functor_Monad. *)
     *)

    Context
      `{Map_U_inst: Map U}
      `{Traverse_U_inst: Traverse U}
      `{Bind_U_inst: Bind T U}
      `{Bindt_U_inst: Bindt T U}
      `{! Compat_Map_Bindt T U}
      `{! Compat_Traverse_Bindt T U}
      `{! Compat_Bind_Bindt T U}
      `{! TraversableRightPreModule T U}.

    #[export] Instance TraversableFunctor_TraversableRightPreModule:
      TraversableFunctor U.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
TraversableFunctor U
    Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
TraversableFunctor U
      constructor; intros.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
A: Type
traverse id = id
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (traverse g) ∘ traverse f = traverse (kc2 g f)
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (U B) ∘ traverse f = traverse (ϕ B ∘ f)
      -
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
A: Type
traverse id = id apply traverse_id.
      -
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (traverse g) ∘ traverse f = traverse (kc2 g f) apply traverse_traverse.
      -
T: Type -> Type
Return_T: Return T
Map_T: Map T
Traverse_T: Traverse T
Bind_TT: Bind T T
Bindt_TT: Bindt T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
TraversableMonad0: TraversableMonad T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
TraversableRightPreModule0: TraversableRightPreModule
  T U
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (U B) ∘ traverse f = traverse (ϕ B ∘ f) apply traverse_morphism.
    Qed.

    #[export] Instance RightPreModule_TraversableRightPreModule:
      RightPreModule T U :=
      {| kmod_bind1 := bind_id;
         kmod_bind2 := bind_bind;
      |}.

    #[export] Instance RightModule_TraversableRightModule:
      RightModule T U :=
      {| kmod_premod := _
      |}.

  End instances.

End DerivedInstances.

(** * Notations *)
(**********************************************************************)
Module Notations.
  Infix "⋆6" := (kc6) (at level 60): tealeaves_scope.
End Notations.