From Tealeaves Require Import
  Classes.Categorical.TraversableMonad
  Classes.Kleisli.TraversableMonad
  Classes.Kleisli.Monad.

Import Kleisli.Monad.Notations.
Import Kleisli.TraversableMonad.Notations.

#[local] Generalizable Variables T G ϕ.

(** * Categorical Traversable Monads from Kleisli Traversable Monads *)
(**********************************************************************)

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

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

    #[export] Instance Dist_Bindt: ApplicativeDist T :=
      fun G _ _ _ A => bindt (G := G) (map (F := G) ret).
    #[export] Instance Join_Bindt: Join T :=
      fun A => bindt (G := fun A => A) id.
  End operations.
End DerivedOperations.

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

  Section with_monad.

    Context
      `{Kleisli.TraversableMonad.TraversableMonad T}.

    Import DerivedOperations.
    Import Kleisli.TraversableMonad.DerivedOperations.
    Import Kleisli.TraversableMonad.DerivedInstances.
    Import Kleisli.TraversableFunctor.DerivedInstances.

    (** ** Monad Instance *)
    (******************************************************************)
    #[export] Instance Natural_Return: Natural (@ret T _).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
Natural (@ret T Return_T)
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
Natural (@ret T Return_T)
      constructor.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
Functor (fun A : Type => A)
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
Functor T
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (A B : Type) (f : A -> B),
map f ∘ ret = ret ∘ map f
      -
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
Functor (fun A : Type => A) typeclasses eauto.
      -
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
Functor T inversion H.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
ktm_bindt0: forall (G : Type -> Type) 
  (Map_G : Map G) (Pure_G : Pure G)
  (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> G (T B)),
bindt f ∘ ret = f
ktm_premod: TraversableRightPreModule T T
Functor T
        typeclasses eauto.
      -
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (A B : Type) (f : A -> B),
map f ∘ ret = ret ∘ map f intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A, B: Type
f: A -> B
map f ∘ ret = ret ∘ map f
        rewrite map_to_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A, B: Type
f: A -> B
bindt (ret ∘ f) ∘ ret = ret ∘ map f
        rewrite (ktm_bindt0 (T := T) (G := fun A => A)).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A, B: Type
f: A -> B
ret ∘ f = ret ∘ map f
        reflexivity.
    Qed.

    #[export] Instance Natural_Join: Natural (@join T _).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
Natural (@join T (Join_Bindt T))
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
Natural (@join T (Join_Bindt T))
      constructor.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
Functor (T ∘ T)
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
Functor T
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (A B : Type) (f : A -> B),
map f ∘ join = join ∘ map f
      -
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
Functor (T ∘ T) typeclasses eauto.
      -
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
Functor T typeclasses eauto.
      -
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (A B : Type) (f : A -> B),
map f ∘ join = join ∘ map f intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A, B: Type
f: A -> B
map f ∘ join = join ∘ map f
        unfold_ops @Map_compose @Join_Bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A, B: Type
f: A -> B
map f ∘ bindt id = bindt id ∘ map (map f)
        rewrite <- bind_to_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A, B: Type
f: A -> B
map f ∘ bind id = bindt id ∘ map (map f)
        rewrite <- bind_to_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A, B: Type
f: A -> B
map f ∘ bind id = bind id ∘ map (map f)
        unfold_compose_in_compose.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A, B: Type
f: A -> B
map f ∘ bind id = bind id ∘ map (map f)
        rewrite map_bind.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A, B: Type
f: A -> B
bind (map f ∘ id) = bind id ∘ map (map f)
        rewrite bind_map.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A, B: Type
f: A -> B
bind (map f ∘ id) = bind (id ∘ map f)
        reflexivity.
    Qed.

    Lemma mon_join_ret_T: forall A: Type,
        join ∘ ret (T := T) (A := T A) = @id (T A).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall A : Type, join ∘ ret = id
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall A : Type, join ∘ ret = id
      intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
join ∘ ret = id unfold_ops @Join_Bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bindt id ∘ ret = id
      unfold_compose_in_compose.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bindt id ∘ ret = id
      rewrite <- bind_to_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bind id ∘ ret = id
      rewrite kmon_bind0.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
id = id
      reflexivity.
    Qed.

    Lemma mon_join_map_ret_T: forall A: Type,
        join (T := T) ∘ map (F := T) ret = @id (T A).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall A : Type, join ∘ map ret = id
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall A : Type, join ∘ map ret = id
      intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
join ∘ map ret = id
      unfold_ops @Join_Bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bindt id ∘ map ret = id
      rewrite <- bind_to_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bind id ∘ map ret = id
      unfold_compose_in_compose.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bind id ∘ map ret = id
      rewrite bind_map.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bind (id ∘ ret) = id
      change (id ∘ ?g) with g.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bind ret = id
      rewrite kmod_bind1.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
id = id
      reflexivity.
    Qed.

    Lemma mon_join_join_T: forall A: Type,
        join (T := T) (A := A) ∘ join (T := T) =
          join ∘ map (F := T) (join (T := T)).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall A : Type, join ∘ join = join ∘ map join
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall A : Type, join ∘ join = join ∘ map join
      intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
join ∘ join = join ∘ map join
      unfold_ops @Join_Bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bindt id ∘ bindt id = bindt id ∘ map (bindt id)
      rewrite <- bind_to_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bind id ∘ bindt id = bind id ∘ map (bind id)
      rewrite <- bind_to_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bind id ∘ bind id = bind id ∘ map (bind id)
      unfold_compose_in_compose.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bind id ∘ bind id = bind id ∘ map (bind id)
      rewrite kmon_bind2.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bind (id ⋆ id) = bind id ∘ map (bind id)
      rewrite bind_map.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bind (id ⋆ id) = bind (id ∘ bind id)
      reflexivity.
    Qed.

    #[export] Instance CategoricalMonad_KleisliTraversableMonad:
      Categorical.Monad.Monad T :=
      {| mon_join_ret := mon_join_ret_T;
         mon_join_map_ret := mon_join_map_ret_T;
         mon_join_join := mon_join_join_T;
      |}.

    (** ** Traversable Functor Instance *)
    (******************************************************************)
    Lemma dist_natural_T:
      forall (G: Type -> Type)
        (mapG: Map G) (pureG: Pure G) (multG: Mult G),
        Applicative G -> Natural (@dist T _ G mapG pureG multG).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (G : Type -> Type) (mapG : Map G)
  (pureG : Pure G) (multG : Mult G),
Applicative G ->
Natural (@dist T (Dist_Bindt T) G mapG pureG multG)
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (G : Type -> Type) (mapG : Map G)
  (pureG : Pure G) (multG : Mult G),
Applicative G ->
Natural (@dist T (Dist_Bindt T) G mapG pureG multG)
      intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
Natural (@dist T (Dist_Bindt T) G mapG pureG multG) constructor.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
Functor (T ○ G)
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
Functor (G ○ T)
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
forall (A B : Type) (f : A -> B),
map f ∘ dist T G = dist T G ∘ map f
      -
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
Functor (T ○ G) typeclasses eauto.
      -
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
Functor (G ○ T) typeclasses eauto.
      -
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
forall (A B : Type) (f : A -> B),
map f ∘ dist T G = dist T G ∘ map f intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
A, B: Type
f: A -> B
map f ∘ dist T G = dist T G ∘ map f
        unfold_ops @Map_compose @Dist_Bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
A, B: Type
f: A -> B
map (map f) ∘ bindt (map ret) =
bindt (map ret) ∘ map (map f)
        rewrite map_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
A, B: Type
f: A -> B
bindt (map (map f) ∘ map ret) =
bindt (map ret) ∘ map (map f)
        rewrite bindt_map.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
A, B: Type
f: A -> B
bindt (map (map f) ∘ map ret) =
bindt (map ret ∘ map f)
        rewrite fun_map_map.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
A, B: Type
f: A -> B
bindt (map (map f ∘ ret)) = bindt (map ret ∘ map f)
        rewrite fun_map_map.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
A, B: Type
f: A -> B
bindt (map (map f ∘ ret)) = bindt (map (ret ∘ f))
        rewrite (natural (ϕ := @ret T _)).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: Applicative G
A, B: Type
f: A -> B
bindt (map (ret ∘ map f)) = bindt (map (ret ∘ f))
        reflexivity.
    Qed.

    Lemma dist_morph_T: forall `{morphism: ApplicativeMorphism G1 G2 ϕ},
      forall A: Type,
        dist T G2 ∘ map (F := T) (ϕ A) = ϕ (T A) ∘ dist T G1.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (G1 G2 : Type -> Type) (H0 : Map G1)
  (H1 : Mult G1) (H2 : Pure G1) (H3 : Map G2)
  (H4 : Mult G2) (H5 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist T G2 ∘ map (ϕ A) = ϕ (T A) ∘ dist T G1
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (G1 G2 : Type -> Type) (H0 : Map G1)
  (H1 : Mult G1) (H2 : Pure G1) (H3 : Map G2)
  (H4 : Mult G2) (H5 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist T G2 ∘ map (ϕ A) = ϕ (T A) ∘ dist T G1
      intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A: Type
dist T G2 ∘ map (ϕ A) = ϕ (T A) ∘ dist T G1
      assert (Applicative G1) by now inversion morphism.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A: Type
H6: Applicative G1
dist T G2 ∘ map (ϕ A) = ϕ (T A) ∘ dist T G1
      assert (Applicative G2) by now inversion morphism.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A: Type
H6: Applicative G1
H7: Applicative G2
dist T G2 ∘ map (ϕ A) = ϕ (T A) ∘ dist T G1
      unfold_ops @Dist_Bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A: Type
H6: Applicative G1
H7: Applicative G2
bindt (map ret) ∘ map (ϕ A) =
ϕ (T A) ∘ bindt (map ret)
      rewrite bindt_map.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A: Type
H6: Applicative G1
H7: Applicative G2
bindt (map ret ∘ ϕ A) = ϕ (T A) ∘ bindt (map ret)
      rewrite ktm_morph.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A: Type
H6: Applicative G1
H7: Applicative G2
bindt (map ret ∘ ϕ A) = bindt (ϕ (T A) ∘ map ret)
      inversion morphism.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A: Type
H6: Applicative G1
H7: Applicative G2
appmor_app_F: Applicative G1
appmor_app_G: Applicative G2
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : G1 A),
ϕ B (map f x) = map f (ϕ A x)
appmor_pure: forall (A : Type) (a : A),
ϕ A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : G1 A)
  (y : G1 B),
ϕ (A * B) (mult (x, y)) =
mult (ϕ A x, ϕ B y)
bindt (map ret ∘ ϕ A) = bindt (ϕ (T A) ∘ map ret)
      rewrite (natural (ϕ := ϕ)).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A: Type
H6: Applicative G1
H7: Applicative G2
appmor_app_F: Applicative G1
appmor_app_G: Applicative G2
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : G1 A),
ϕ B (map f x) = map f (ϕ A x)
appmor_pure: forall (A : Type) (a : A),
ϕ A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : G1 A)
  (y : G1 B),
ϕ (A * B) (mult (x, y)) =
mult (ϕ A x, ϕ B y)
bindt (ϕ (T A) ∘ map ret) = bindt (ϕ (T A) ∘ map ret)
      reflexivity.
    Qed.

    Lemma dist_unit_T: forall A: Type,
        dist T (fun A0: Type => A0) = @id (T A).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall A : Type, dist T (fun A0 : Type => A0) = id
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall A : Type, dist T (fun A0 : Type => A0) = id
      intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
dist T (fun A0 : Type => A0) = id
      unfold_ops @Dist_Bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bindt (map ret) = id
      unfold_ops @Map_I.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
bindt ret = id
      rewrite ktm_bindt1.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
A: Type
id = id
      reflexivity.
    Qed.

    Lemma dist_linear_T: forall `{Applicative G1} `{Applicative G2},
      forall (A: Type),
        dist T (G1 ∘ G2) (A := A) =
          map (F := G1) (dist T G2) ∘ dist T G1.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall A : Type,
dist T (G1 ∘ G2) = map (dist T G2) ∘ dist T G1
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall A : Type,
dist T (G1 ∘ G2) = map (dist T G2) ∘ dist T G1
      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
A: Type
dist T (G1 ∘ G2) = map (dist T G2) ∘ dist T G1
      unfold_ops @Dist_Bindt @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
A: Type
bindt (map (map ret)) =
map (bindt (map ret)) ∘ bindt (map ret)
      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
A: Type
bindt (map (map ret)) = bindt (map ret ⋆6 map ret)
      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
A: Type
bindt (map (map ret)) =
bindt (map (bindt (map ret)) ∘ map ret)
      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
A: Type
bindt (map (map ret)) =
bindt (map (bindt (map ret) ∘ ret))
      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
A: Type
bindt (map (map ret)) = bindt (map (map ret))
      reflexivity.
    Qed.

    #[export] Instance TraversableFunctor_Categorical_TraversableMonad_Kleisli:
      Categorical.TraversableFunctor.TraversableFunctor T :=
      {| dist_natural := dist_natural_T;
         dist_morph := @dist_morph_T;
         dist_unit := dist_unit_T;
         dist_linear := @dist_linear_T;
      |}.

    (** ** Traversable Monad Instance *)
    (******************************************************************)
    Lemma trvmon_ret_T:
      forall (G: Type -> Type) (H3: Map G) (H4: Pure G) (H5: Mult G),
        Applicative G ->
        forall (A: Type), dist T G ∘ ret (T := T) (A := G A) =
                          map (F := G) (ret (T := T)).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (G : Type -> Type) (H3 : Map G) (H4 : Pure G)
  (H5 : Mult G),
Applicative G ->
forall A : Type, dist T G ∘ ret = map ret
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (G : Type -> Type) (H3 : Map G) (H4 : Pure G)
  (H5 : Mult G),
Applicative G ->
forall A : Type, dist T G ∘ ret = map ret
      intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
dist T G ∘ ret = map ret unfold_ops @Dist_Bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
bindt (map ret) ∘ ret = map ret
      rewrite (ktm_bindt0 (T := T)); auto.
    Qed.

    Lemma trvmon_join_T:
      forall (G: Type -> Type) (H3: Map G) (H4: Pure G) (H5: Mult G),
        Applicative G -> forall (A: Type),
          dist T G ∘ join (T := T) (A := G A) =
            map (F := G) join ∘ dist T G ∘ map (F := T) (dist T G).
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (G : Type -> Type) (H3 : Map G) (H4 : Pure G)
  (H5 : Mult G),
Applicative G ->
forall A : Type,
dist T G ∘ join = map join ∘ dist T G ∘ map (dist T G)
    Proof.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
forall (G : Type -> Type) (H3 : Map G) (H4 : Pure G)
  (H5 : Mult G),
Applicative G ->
forall A : Type,
dist T G ∘ join = map join ∘ dist T G ∘ map (dist T G)
      intros.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
dist T G ∘ join = map join ∘ dist T G ∘ map (dist T G) unfold_ops @Dist_Bindt @Join_Bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
bindt (map ret) ∘ bindt id =
map (bindt id) ∘ bindt (map ret)
∘ map (bindt (map ret))
      do 2 rewrite <- bind_to_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
bindt (map ret) ∘ bind id =
map (bind id) ∘ bindt (map ret)
∘ map (bindt (map ret))
      unfold_compose_in_compose.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
bindt (map ret) ∘ bind id =
map (bind id) ∘ bindt (map ret)
∘ map (bindt (map ret))
      rewrite bindt_bind.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
bindt (bindt (map ret) ∘ id) =
map (bind id) ∘ bindt (map ret)
∘ map (bindt (map ret))
      unfold compose at 5.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
bindt (bindt (map ret) ∘ id) =
map (bind id) ∘ bindt (map ret)
∘ map (bindt (map ret))
      rewrite bind_bindt.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
bindt (bindt (map ret) ∘ id) =
bindt (map (bind id) ∘ map ret)
∘ map (bindt (map ret))
      rewrite fun_map_map.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
bindt (bindt (map ret) ∘ id) =
bindt (map (bind id ∘ ret)) ∘ map (bindt (map ret))
      rewrite bindt_map.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
bindt (bindt (map ret) ∘ id) =
bindt (map (bind id ∘ ret) ∘ bindt (map ret))
      rewrite bind_ret.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
bindt (bindt (map ret) ∘ id) =
bindt (map id ∘ bindt (map ret))
      rewrite fun_map_id.
T: Type -> Type
Return_T: Return T
Bindt_TT: Bindt T T
H: TraversableMonad T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
bindt (bindt (map ret) ∘ id) =
bindt (id ∘ bindt (map ret))
      reflexivity.
    Qed.

    #[export] Instance TraversableMonad_Categorical_Kleisli:
      Categorical.TraversableMonad.TraversableMonad T :=
      {| trvmon_ret := trvmon_ret_T;
         trvmon_join := trvmon_join_T;
      |}.

  End with_monad.

End DerivedInstances.