From Tealeaves Require Import
  Classes.Categorical.DecoratedTraversableMonad
  Classes.Kleisli.DecoratedTraversableMonad
  Classes.Categorical.Bimonad (bimonad_baton).

Import Kleisli.DecoratedTraversableMonad.Notations.
Import Kleisli.DecoratedMonad.Notations.
Import Kleisli.TraversableMonad.Notations.
Import Kleisli.Comonad.Notations.
Import Product.Notations.
Import Monoid.Notations.
Import Functor.Notations.

#[local] Generalizable Variables T A B C.

#[local] Arguments ret (T)%function_scope {Return}
  (A)%type_scope _.
#[local] Arguments join T%function_scope {Join}
  {A}%type_scope _.
#[local] Arguments map F%function_scope {Map}
  {A B}%type_scope f%function_scope _.
#[local] Arguments extract (W)%function_scope {Extract}
  (A)%type_scope _.
#[local] Arguments cojoin W%function_scope {Cojoin}
  {A}%type_scope _.
#[local] Arguments mapd {E}%type_scope T%function_scope {Mapd}
  {A B}%type_scope _%function_scope _.
#[local] Arguments mapdt {E}%type_scope T%function_scope {Mapdt}
  G%function_scope {H H0 H1} {A B}%type_scope _%function_scope.
#[local] Arguments bindd {W}%type_scope {T} (U)%function_scope {Bindd}
  {A B}%type_scope _ _.
#[local] Arguments traverse T%function_scope {Traverse}
  G%function_scope {Map_G Pure_G Mult_G}
  {A B}%type_scope _%function_scope _.

(** * Categorical DTMs from Kleisli DTMs *)
(**********************************************************************)

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

    Context
      (W: Type)
      (T: Type -> Type)
      `{Binddt W T T}
      `{Return T}.

    #[export] Instance Join_Binddt: Join T :=
      fun A => binddt (G := fun A => A) (A := T A) (extract (W ×) (T A)).
    #[export] Instance Decorate_Binddt: Decorate W T :=
      fun A => binddt (G := fun A => A) (ret T (W * A)).
    #[export] Instance Dist_Binddt: ApplicativeDist T :=
      fun G _ _ _ A =>
        binddt (T := T) (map G (ret T A) ∘ extract (W ×) (G A)).

  End operations.
End DerivedOperations.

Module DerivedInstances.

  Section with_monad.

    Context
      (W: Type)
      (T: Type -> Type)
      `{Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad W T}.

    (* Alectryon doesn't like this
       Import KleisliToCategorical.DecoratedTraversableMonad.DerivedOperations.
     *)
    Import DerivedOperations.
    Import Kleisli.DecoratedTraversableMonad.DerivedOperations.
    Import Kleisli.DecoratedTraversableMonad.DerivedInstances.

    #[local] Tactic Notation "unfold_everything" :=
      unfold_ops @Map_compose;
      unfold_ops @Decorate_Binddt;
      unfold_ops @Map_Binddt;
      unfold_ops @Dist_Binddt;
      unfold_ops @Join_Binddt.

    #[local] Tactic Notation "binddt_to_bindd" :=
      rewrite <- bindd_to_binddt.

    #[local] Tactic Notation "mapdt_to_mapd" :=
      rewrite <- mapd_to_mapdt.

    #[local] Tactic Notation "mapd_to_map" :=
      rewrite <- map_to_mapd.

    (** ** Monad Instance *)
    (******************************************************************)
    Lemma ret_natural: Natural (@ret T _).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Natural (ret T)
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Natural (ret T)
      constructor.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Functor (fun A : Type => A)
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Functor T
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (A B : Type) (f : A -> B),
map T f ∘ ret T A =
ret T B ∘ map (fun A0 : Type => A0) f
      -
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Functor (fun A : Type => A) typeclasses eauto.
      -
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Functor T typeclasses eauto.
      -
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (A B : Type) (f : A -> B),
map T f ∘ ret T A =
ret T B ∘ map (fun A0 : Type => A0) f intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
map T f ∘ ret T A =
ret T B ∘ map (fun A : Type => A) f
        rewrite map_to_binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
binddt (ret T B ∘ f ∘ extract (prod W) A) ∘ ret T A =
ret T B ∘ map (fun A : Type => A) f
        rewrite (kdtm_binddt0 (G := fun A => A)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
ret T B ∘ f ∘ extract (prod W) A ∘ ret (prod W) A =
ret T B ∘ map (fun A : Type => A) f
        reflexivity.
    Qed.

    Lemma join_natural: Natural (@join T _).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Natural (@join T (Join_Binddt W T))
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Natural (@join T (Join_Binddt W T))
      constructor.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Functor (T ∘ T)
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Functor T
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (A B : Type) (f : A -> B),
map T f ∘ join T = join T ∘ map (T ∘ T) f
      -
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Functor (T ∘ T) typeclasses eauto.
      -
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Functor T typeclasses eauto.
      -
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (A B : Type) (f : A -> B),
map T f ∘ join T = join T ∘ map (T ∘ T) f intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
map T f ∘ join T = join T ∘ map (T ∘ T) f
        unfold join.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
map T f ∘ Join_Binddt W T A =
Join_Binddt W T B ∘ map (T ∘ T) f
        unfold Join_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
map T f ∘ binddt (extract (prod W) (T A)) =
binddt (extract (prod W) (T B)) ∘ map (T ∘ T) f
        change (map T f) with (map (fun A => A) (map T f)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
map (fun A : Type => A) (map T f)
∘ binddt (extract (prod W) (T A)) =
binddt (extract (prod W) (T B)) ∘ map (T ∘ T) f
        unfold_compose_in_compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
map (fun A : Type => A) (map T f)
∘ binddt (extract (prod W) (T A)) =
binddt (extract (prod W) (T B)) ∘ map (T ∘ T) f
        rewrite (map_binddt (W := W) (T := T) (U := T)
                   (G1 := fun A => A)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
binddt
  (map (fun A : Type => A) (map T f)
   ∘ extract (prod W) (T A)) =
binddt (extract (prod W) (T B)) ∘ map (T ∘ T) f
        unfold_ops @Map_I.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
binddt (map T f ∘ extract (prod W) (T A)) =
binddt (extract (prod W) (T B)) ∘ map (T ∘ T) f
        change (map (T ∘ T) f) with (map T (map T f)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
binddt (map T f ∘ extract (prod W) (T A)) =
binddt (extract (prod W) (T B)) ∘ map T (map T f)
        rewrite (binddt_map (G2 := fun A => A) (T := T) (U := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
binddt (map T f ∘ extract (prod W) (T A)) =
binddt
  (extract (prod W) (T B) ∘ map (prod W) (map T f))
        rewrite <- (natural (Natural := Natural_extract_reader W)
                     (ϕ := @extract (W ×) _) (map T f)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
binddt (map T f ∘ extract (prod W) (T A)) =
binddt
  (map (fun A : Type => A) (map T f)
   ∘ extract (prod W) (T A))
        reflexivity.
    Qed.

    Lemma join_ret: `(join T ∘ ret T (T A) = @id (T A)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type, join T ∘ ret T (T A) = id
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type, join T ∘ ret T (T A) = id
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
join T ∘ ret T (T A) = id
      unfold_ops @Join_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
binddt (extract (prod W) (T A)) ∘ ret T (T A) = id
      unfold_compose_in_compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
binddt (extract (prod W) (T A)) ∘ ret T (T A) = id
      rewrite (kdtm_binddt0 (G := fun A => A)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
extract (prod W) (T A) ∘ ret (prod W) (T A) = id
      rewrite (bimonad_baton (prod W)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
id = id
      reflexivity.
    Qed.

    Lemma join_map_ret: `(join T ∘ map T (ret T A) = @id (T A)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type, join T ∘ map T (ret T A) = id
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type, join T ∘ map T (ret T A) = id
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
join T ∘ map T (ret T A) = id
      unfold join.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
Join_Binddt W T A ∘ map T (ret T A) = id
      unfold Join_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
binddt (extract (prod W) (T A)) ∘ map T (ret T A) = id
      binddt_to_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (extract (prod W) (T A)) ∘ map T (ret T A) =
id
      unfold_compose_in_compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (extract (prod W) (T A)) ∘ map T (ret T A) =
id
      rewrite bindd_map.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T
  (extract (prod W) (T A) ∘ map (prod W) (ret T A)) =
id
      rewrite <- (natural (Natural := Natural_extract_reader W)
                   (ϕ := @extract (W ×) _)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T
  (map (fun A : Type => A) (ret T A)
   ∘ extract (prod W) A) = id
      unfold_ops @Map_I.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T A ∘ extract (prod W) A) = id
      rewrite kdm_bindd1.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
id = id
      reflexivity.
    Qed.

    Lemma join_join:
      `(join T ∘ join T (A := T A) = join T ∘ map T (join T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type,
join T ∘ join T = join T ∘ map T (join T)
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type,
join T ∘ join T = join T ∘ map T (join T)
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
join T ∘ join T = join T ∘ map T (join T)
      unfold join.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
Join_Binddt W T A ∘ Join_Binddt W T (T A) =
Join_Binddt W T A ∘ map T (Join_Binddt W T A)
      unfold Join_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
binddt (extract (prod W) (T A))
∘ binddt (extract (prod W) (T (T A))) =
binddt (extract (prod W) (T A))
∘ map T (binddt (extract (prod W) (T A)))
      repeat binddt_to_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (extract (prod W) (T A))
∘ bindd T (extract (prod W) (T (T A))) =
bindd T (extract (prod W) (T A))
∘ map T (bindd T (extract (prod W) (T A)))
      unfold_compose_in_compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (extract (prod W) (T A))
∘ bindd T (extract (prod W) (T (T A))) =
bindd T (extract (prod W) (T A))
∘ map T (bindd T (extract (prod W) (T A)))
      (* Merge LHS *)
      rewrite (kdm_bindd2 (T := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T
  (extract (prod W) (T A)
   ⋆5 extract (prod W) (T (T A))) =
bindd T (extract (prod W) (T A))
∘ map T (bindd T (extract (prod W) (T A)))
      (* Merge RHS *)
      rewrite (bindd_map).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T
  (extract (prod W) (T A)
   ⋆5 extract (prod W) (T (T A))) =
bindd T
  (extract (prod W) (T A)
   ∘ map (prod W) (bindd T (extract (prod W) (T A))))
      rewrite <- (natural (Natural := Natural_extract_reader W)
                   (ϕ := @extract (W ×) _)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T
  (extract (prod W) (T A)
   ⋆5 extract (prod W) (T (T A))) =
bindd T
  (map (fun A : Type => A)
     (bindd T (extract (prod W) (T A)))
   ∘ extract (prod W) ((T ∘ T) A))
      unfold_ops @Map_I.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T
  (extract (prod W) (T A)
   ⋆5 extract (prod W) (T (T A))) =
bindd T
  (bindd T (extract (prod W) (T A))
   ∘ extract (prod W) ((T ∘ T) A))
      change (extract ?W ?A) with (id ∘ extract W A) at 1.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T
  (id ∘ extract (prod W) (T A)
   ⋆5 extract (prod W) (T (T A))) =
bindd T
  (bindd T (extract (prod W) (T A))
   ∘ extract (prod W) ((T ∘ T) A))
      change (extract ?W ?A) with (id ∘ extract W A) at 2.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T
  (id ∘ extract (prod W) (T A)
   ⋆5 id ∘ extract (prod W) (T (T A))) =
bindd T
  (bindd T (extract (prod W) (T A))
   ∘ extract (prod W) ((T ∘ T) A))
      rewrite kc5_44.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (kc id id ∘ extract (prod W) (T (T A))) =
bindd T
  (bindd T (extract (prod W) (T A))
   ∘ extract (prod W) ((T ∘ T) A))
      reflexivity.
    Qed.

    #[export] Instance: Categorical.Monad.Monad T :=
      {| mon_ret_natural := ret_natural;
         mon_join_natural := join_natural;
         mon_join_ret := join_ret;
         mon_join_map_ret := join_map_ret;
         mon_join_join := join_join;
      |}.

    (** ** Decorated Functor Instance *)
    (******************************************************************)
    Lemma dec_dec: forall (A: Type),
        dec T ∘ dec T = map T (cojoin (W ×)) ∘ dec T (A := A).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type,
dec T ∘ dec T = map T (cojoin (prod W)) ∘ dec T
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type,
dec T ∘ dec T = map T (cojoin (prod W)) ∘ dec T
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
dec T ∘ dec T = map T (cojoin (prod W)) ∘ dec T
      (* LHS *)
      unfold dec at 1 2.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
Decorate_Binddt W T (W * A) ∘ Decorate_Binddt W T A =
map T (cojoin (prod W)) ∘ dec T
      unfold Decorate_Binddt at 1 2.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
binddt (ret T (W * (W * A))) ∘ binddt (ret T (W * A)) =
map T (cojoin (prod W)) ∘ dec T
      do 2 binddt_to_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * (W * A)))
∘ bindd T (ret T (W * A)) =
map T (cojoin (prod W)) ∘ dec T
      unfold_compose_in_compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * (W * A)))
∘ bindd T (ret T (W * A)) =
map T (cojoin (prod W)) ∘ dec T
      rewrite (kdm_bindd2 (T := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * (W * A)) ⋆5 ret T (W * A)) =
map T (cojoin (prod W)) ∘ dec T
      change (ret ?T ?A) with (ret T A ∘ id) at 1.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * (W * A)) ∘ id ⋆5 ret T (W * A)) =
map T (cojoin (prod W)) ∘ dec T
      change (ret ?T ?A) with (ret T A ∘ id) at 2.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T
  (ret T (W * (W * A)) ∘ id ⋆5 ret T (W * A) ∘ id) =
map T (cojoin (prod W)) ∘ dec T
      rewrite kc5_11.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * (W * A)) ∘ (id ⋆1 id)) =
map T (cojoin (prod W)) ∘ dec T
      (* RHS *)
      unfold dec at 1.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * (W * A)) ∘ (id ⋆1 id)) =
map T (cojoin (prod W)) ∘ Decorate_Binddt W T A
      unfold Decorate_Binddt at 1.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * (W * A)) ∘ (id ⋆1 id)) =
map T (cojoin (prod W)) ∘ binddt (ret T (W * A))
      binddt_to_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * (W * A)) ∘ (id ⋆1 id)) =
map T (cojoin (prod W)) ∘ bindd T (ret T (W * A))
      rewrite map_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * (W * A)) ∘ (id ⋆1 id)) =
bindd T (map T (cojoin (prod W)) ∘ ret T (W * A))
      rewrite (natural (ϕ := ret T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * (W * A)) ∘ (id ⋆1 id)) =
bindd T
  (ret T ((prod W ∘ prod W) A)
   ∘ map (fun A : Type => A) (cojoin (prod W)))
      reflexivity.
    Qed.

    Lemma dec_extract: forall (A: Type),
        map T (extract (W ×) A) ∘ dec T = @id (T A).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type,
map T (extract (prod W) A) ∘ dec T = id
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type,
map T (extract (prod W) A) ∘ dec T = id
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
map T (extract (prod W) A) ∘ dec T = id
      unfold dec.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
map T (extract (prod W) A) ∘ Decorate_Binddt W T A =
id
      unfold Decorate_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
map T (extract (prod W) A) ∘ binddt (ret T (W * A)) =
id
      binddt_to_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
map T (extract (prod W) A) ∘ bindd T (ret T (W * A)) =
id
      rewrite map_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (map T (extract (prod W) A) ∘ ret T (W * A)) =
id
      rewrite (natural (ϕ := ret T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T
  (ret T A
   ∘ map (fun A : Type => A) (extract (prod W) A)) =
id
      unfold_ops @Map_I.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T A ∘ extract (prod W) A) = id
      rewrite kdm_bindd1.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
id = id
      reflexivity.
    Qed.

    Lemma dec_natural: Natural (@dec W T _).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Natural (@dec W T (Decorate_Binddt W T))
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Natural (@dec W T (Decorate_Binddt W T))
      constructor.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Functor T
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Functor (T ○ prod W)
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (A B : Type) (f : A -> B),
map (T ○ prod W) f ∘ dec T = dec T ∘ map T f
      -
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Functor T typeclasses eauto.
      -
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Functor (T ○ prod W) typeclasses eauto.
      -
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (A B : Type) (f : A -> B),
map (T ○ prod W) f ∘ dec T = dec T ∘ map T f intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
map (T ○ prod W) f ∘ dec T = dec T ∘ map T f
        unfold dec.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
map (T ○ prod W) f ∘ Decorate_Binddt W T A =
Decorate_Binddt W T B ∘ map T f
        unfold Decorate_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
map (T ○ prod W) f ∘ binddt (ret T (W * A)) =
binddt (ret T (W * B)) ∘ map T f
        do 2 binddt_to_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
map (T ○ prod W) f ∘ bindd T (ret T (W * A)) =
bindd T (ret T (W * B)) ∘ map T f
        change (map (T ○ prod W) f) with (map T (map (prod W) f)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
map T (map (prod W) f) ∘ bindd T (ret T (W * A)) =
bindd T (ret T (W * B)) ∘ map T f
        rewrite map_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
bindd T (map T (map (prod W) f) ∘ ret T (W * A)) =
bindd T (ret T (W * B)) ∘ map T f
        rewrite (natural (ϕ := ret T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
bindd T
  (ret T (W * B)
   ∘ map (fun A : Type => A) (map (prod W) f)) =
bindd T (ret T (W * B)) ∘ map T f
        rewrite bindd_map.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A, B: Type
f: A -> B
bindd T
  (ret T (W * B)
   ∘ map (fun A : Type => A) (map (prod W) f)) =
bindd T (ret T (W * B) ∘ map (prod W) f)
        reflexivity.
    Qed.

    #[export] Instance:
      Categorical.DecoratedFunctor.DecoratedFunctor W T :=
      {| dfun_dec_natural := dec_natural;
         dfun_dec_dec := dec_dec;
         dfun_dec_extract := dec_extract;
      |}.

    (** ** Decorated Monad Instance *)
    (******************************************************************)
    Lemma dmon_ret_: forall (A: Type),
        dec T ∘ ret T A = ret T (W * A) ∘ pair Ƶ (B:=A).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type,
dec T ∘ ret T A = ret T (W * A) ∘ pair Ƶ
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type,
dec T ∘ ret T A = ret T (W * A) ∘ pair Ƶ
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
dec T ∘ ret T A = ret T (W * A) ∘ pair Ƶ
      unfold_everything.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
binddt (ret T (W * A)) ∘ ret T A =
ret T (W * A) ∘ pair Ƶ
      binddt_to_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * A)) ∘ ret T A =
ret T (W * A) ∘ pair Ƶ
      now rewrite (kdm_bindd0 (T := T)).
    Qed.

    Lemma dmon_join_: forall (A: Type),
        dec T ∘ join T (A:=A) =
          join T ∘ map T (shift T) ∘ dec T ∘ map T (dec T).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type,
dec T ∘ join T =
join T ∘ map T (shift T) ∘ dec T ∘ map T (dec T)
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type,
dec T ∘ join T =
join T ∘ map T (shift T) ∘ dec T ∘ map T (dec T)
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
dec T ∘ join T =
join T ∘ map T (shift T) ∘ dec T ∘ map T (dec T)
      unfold shift.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
dec T ∘ join T =
join T ∘ map T (map T (uncurry incr) ∘ strength)
∘ dec T ∘ map T (dec T)
      unfold strength.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
dec T ∘ join T =
join T
∘ map T
    (map T (uncurry incr)
     ∘ (fun '(a, t) => map T (pair a) t)) ∘ dec T
∘ map T (dec T)
      unfold join, Join_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
dec T ∘ binddt (extract (prod W) (T A)) =
binddt (extract (prod W) (T (W * A)))
∘ map T
    (map T (uncurry incr)
     ∘ (fun '(a, t) => map T (pair a) t)) ∘ dec T
∘ map T (dec T)
      repeat binddt_to_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
dec T ∘ bindd T (extract (prod W) (T A)) =
bindd T (extract (prod W) (T (W * A)))
∘ map T
    (map T (uncurry incr)
     ∘ (fun '(a, t) => map T (pair a) t)) ∘ dec T
∘ map T (dec T)
      unfold dec, Decorate_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
binddt (ret T (W * A))
∘ bindd T (extract (prod W) (T A)) =
bindd T (extract (prod W) (T (W * A)))
∘ map T
    (map T (uncurry incr)
     ∘ (fun '(a, t) => map T (pair a) t))
∘ binddt (ret T (W * T (W * A)))
∘ map T (binddt (ret T (W * A)))
      repeat binddt_to_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * A))
∘ bindd T (extract (prod W) (T A)) =
bindd T (extract (prod W) (T (W * A)))
∘ map T
    (map T (uncurry incr)
     ∘ (fun '(a, t) => map T (pair a) t))
∘ bindd T (ret T (W * T (W * A)))
∘ map T (bindd T (ret T (W * A)))
      unfold_compose_in_compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * A))
∘ bindd T (extract (prod W) (T A)) =
bindd T (extract (prod W) (T (W * A)))
∘ map T
    (map T (uncurry incr)
     ∘ (fun '(a, t) => map T (pair a) t))
∘ bindd T (ret T (W * T (W * A)))
∘ map T (bindd T (ret T (W * A)))
      (* Fuse LHS *)
      rewrite (kdm_bindd2 (T := T)) at 1.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * A) ⋆5 extract (prod W) (T A)) =
bindd T (extract (prod W) (T (W * A)))
∘ map T
    (map T (uncurry incr)
     ∘ (fun '(a, t) => map T (pair a) t))
∘ bindd T (ret T (W * T (W * A)))
∘ map T (bindd T (ret T (W * A)))
      change (extract (W ×) (T A))
        with (id ∘ extract (W ×) (T A)) at 1.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (ret T (W * A) ⋆5 id ∘ extract (prod W) (T A)) =
bindd T (extract (prod W) (T (W * A)))
∘ map T
    (map T (uncurry incr)
     ∘ (fun '(a, t) => map T (pair a) t))
∘ bindd T (ret T (W * T (W * A)))
∘ map T (bindd T (ret T (W * A)))
      rewrite kc5_54.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T
  ((fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t)
   ∘ map (prod W) id) =
bindd T (extract (prod W) (T (W * A)))
∘ map T
    (map T (uncurry incr)
     ∘ (fun '(a, t) => map T (pair a) t))
∘ bindd T (ret T (W * T (W * A)))
∘ map T (bindd T (ret T (W * A)))
      rewrite (fun_map_id (F := (W ×))).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T
  ((fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) ∘ id) =
bindd T (extract (prod W) (T (W * A)))
∘ map T
    (map T (uncurry incr)
     ∘ (fun '(a, t) => map T (pair a) t))
∘ bindd T (ret T (W * T (W * A)))
∘ map T (bindd T (ret T (W * A)))
      change (?f ∘ id) with f.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) =
bindd T (extract (prod W) (T (W * A)))
∘ map T
    (map T (uncurry incr)
     ∘ (fun '(a, t) => map T (pair a) t))
∘ bindd T (ret T (W * T (W * A)))
∘ map T (bindd T (ret T (W * A)))
      (* Fuse RHS *)
      rewrite map_to_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) =
bindd T (extract (prod W) (T (W * A)))
∘ bindd T
    (ret T (T (W * A))
     ∘ (map T (uncurry incr)
        ∘ (fun '(a, t) => map T (pair a) t))
     ∘ extract (prod W) (W * T (W * A)))
∘ bindd T (ret T (W * T (W * A)))
∘ map T (bindd T (ret T (W * A)))
      rewrite (kdm_bindd2 (T := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) =
bindd T
  (extract (prod W) (T (W * A))
   ⋆5 ret T (T (W * A))
      ∘ (map T (uncurry incr)
         ∘ (fun '(a, t) => map T (pair a) t))
      ∘ extract (prod W) (W * T (W * A)))
∘ bindd T (ret T (W * T (W * A)))
∘ map T (bindd T (ret T (W * A)))
      reassociate -> near (extract (W ×) _).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) =
bindd T
  (extract (prod W) (T (W * A))
   ⋆5 ret T (T (W * A))
      ∘ (map T (uncurry incr)
         ∘ (fun '(a, t) => map T (pair a) t)
         ∘ extract (prod W) (W * T (W * A))))
∘ bindd T (ret T (W * T (W * A)))
∘ map T (bindd T (ret T (W * A)))
      rewrite (kc5_51).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) =
bindd T
  (extract (prod W) (T (W * A))
   ⋆1 map T (uncurry incr)
      ∘ (fun '(a, t) => map T (pair a) t)
      ∘ extract (prod W) (W * T (W * A)))
∘ bindd T (ret T (W * T (W * A)))
∘ map T (bindd T (ret T (W * A)))
      rewrite (kc1_id_l).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) =
bindd T
  (map T (uncurry incr)
   ∘ (fun '(a, t) => map T (pair a) t)
   ∘ extract (prod W) (W * T (W * A)))
∘ bindd T (ret T (W * T (W * A)))
∘ map T (bindd T (ret T (W * A)))
      rewrite (kdm_bindd2 (T := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) =
bindd T
  (map T (uncurry incr)
   ∘ (fun '(a, t) => map T (pair a) t)
   ∘ extract (prod W) (W * T (W * A))
   ⋆5 ret T (W * T (W * A)))
∘ map T (bindd T (ret T (W * A)))
      change (ret T ((W × ) (T ((W × ) A))))
        with ((ret T ((W × ) (T ((W × ) A)))) ∘ id).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) =
bindd T
  (map T (uncurry incr)
   ∘ (fun '(a, t) => map T (pair a) t)
   ∘ extract (prod W) (W * T (W * A))
   ⋆5 ret T (W * T (W * A)) ∘ id)
∘ map T (bindd T (ret T (W * A)))
      rewrite (kc5_51).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) =
bindd T
  (map T (uncurry incr)
   ∘ (fun '(a, t) => map T (pair a) t)
   ∘ extract (prod W) (W * T (W * A)) ⋆1 id)
∘ map T (bindd T (ret T (W * A)))
      rewrite (kc1_01).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) =
bindd T
  (map T (uncurry incr)
   ∘ (fun '(a, t) => map T (pair a) t) ∘ id)
∘ map T (bindd T (ret T (W * A)))
      change (?f ∘ id) with f.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) =
bindd T
  (map T (uncurry incr)
   ∘ (fun '(a, t) => map T (pair a) t))
∘ map T (bindd T (ret T (W * A)))
      rewrite bindd_map.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
bindd T (fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) =
bindd T
  (map T (uncurry incr)
   ∘ (fun '(a, t) => map T (pair a) t)
   ∘ map (prod W) (bindd T (ret T (W * A))))
      (* Now compare inner functions *)
      fequal.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
(fun '(w, t) => bindd T (ret T (W * A) ⦿ w) t) =
map T (uncurry incr)
∘ (fun '(a, t) => map T (pair a) t)
∘ map (prod W) (bindd T (ret T (W * A)))
      ext [w t].
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
w: W
t: T A
bindd T (ret T (W * A) ⦿ w) t =
(map T (uncurry incr)
 ∘ (fun '(a, t) => map T (pair a) t)
 ∘ map (prod W) (bindd T (ret T (W * A)))) (w, t)
      do 2 (unfold compose; cbn).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
w: W
t: T A
bindd T (ret T (W * A) ⦿ w) t =
map T (uncurry incr)
  (map T (pair (id w)) (bindd T (ret T (W * A)) t))
      compose near (bindd T (ret T (W * A)) t).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
w: W
t: T A
bindd T (ret T (W * A) ⦿ w) t =
(map T (uncurry incr) ∘ map T (pair (id w)))
  (bindd T (ret T (W * A)) t)
      rewrite (fun_map_map (F := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
w: W
t: T A
bindd T (ret T (W * A) ⦿ w) t =
map T (uncurry incr ∘ pair (id w))
  (bindd T (ret T (W * A)) t)
      compose near t on right.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
w: W
t: T A
bindd T (ret T (W * A) ⦿ w) t =
(map T (uncurry incr ∘ pair (id w))
 ∘ bindd T (ret T (W * A))) t
      rewrite map_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
w: W
t: T A
bindd T (ret T (W * A) ⦿ w) t =
bindd T
  (map T (uncurry incr ∘ pair (id w)) ∘ ret T (W * A))
  t
      rewrite (natural (ϕ := ret T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
w: W
t: T A
bindd T (ret T (W * A) ⦿ w) t =
bindd T
  (ret T (W * A)
   ∘ map (fun A : Type => A)
       (uncurry incr ∘ pair (id w))) t
      reflexivity.
    Qed.

    #[export] Instance:
      Categorical.DecoratedMonad.DecoratedMonad W T :=
      {| dmon_ret := dmon_ret_;
         dmon_join := dmon_join_;
      |}.

    (** ** Traversable Functor instance *)
    (******************************************************************)
    Lemma dist_natural_T:
      forall (G: Type -> Type) (H2: Map G) (H3: Pure G) (H4: Mult G)
        (Happ: Applicative G),
        Natural (@dist T _ G H2 H3 H4).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G : Type -> Type) (H2 : Map G) (H3 : Pure G)
  (H4 : Mult G),
Applicative G ->
Natural (@dist T (Dist_Binddt W T) G H2 H3 H4)
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G : Type -> Type) (H2 : Map G) (H3 : Pure G)
  (H4 : Mult G),
Applicative G ->
Natural (@dist T (Dist_Binddt W T) G H2 H3 H4)
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
Natural (@dist T (Dist_Binddt W T) G H2 H3 H4) inversion Happ.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
Natural (@dist T (Dist_Binddt W T) G H2 H3 H4) constructor.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
Functor (T ○ G)
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
Functor (G ○ T)
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
forall (A B : Type) (f : A -> B),
map (G ○ T) f ∘ dist T G = dist T G ∘ map (T ○ G) f
      -
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
Functor (T ○ G) typeclasses eauto.
      -
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
Functor (G ○ T) typeclasses eauto.
      -
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
forall (A B : Type) (f : A -> B),
map (G ○ T) f ∘ dist T G = dist T G ∘ map (T ○ G) f intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
map (G ○ T) f ∘ dist T G = dist T G ∘ map (T ○ G) f
        unfold dist, Dist_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
map (G ○ T) f
∘ binddt (map G (ret T A) ∘ extract (prod W) (G A)) =
binddt (map G (ret T B) ∘ extract (prod W) (G B))
∘ map (T ○ G) f
        change (map (G ○ T) f) with (map G (map T f)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
map G (map T f)
∘ binddt (map G (ret T A) ∘ extract (prod W) (G A)) =
binddt (map G (ret T B) ∘ extract (prod W) (G B))
∘ map (T ○ G) f
        rewrite map_binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
binddt
  (map G (map T f)
   ∘ (map G (ret T A) ∘ extract (prod W) (G A))) =
binddt (map G (ret T B) ∘ extract (prod W) (G B))
∘ map (T ○ G) f
        reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
binddt
  (map G (map T f) ∘ map G (ret T A)
   ∘ extract (prod W) (G A)) =
binddt (map G (ret T B) ∘ extract (prod W) (G B))
∘ map (T ○ G) f
        rewrite (fun_map_map (F := G)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
binddt
  (map G (map T f ∘ ret T A) ∘ extract (prod W) (G A)) =
binddt (map G (ret T B) ∘ extract (prod W) (G B))
∘ map (T ○ G) f
        rewrite (natural (ϕ := ret T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
binddt
  (map G (ret T B ∘ map (fun A : Type => A) f)
   ∘ extract (prod W) (G A)) =
binddt (map G (ret T B) ∘ extract (prod W) (G B))
∘ map (T ○ G) f
        (* RHS *)
        change (map (T ○ G) f) with (map T (map G f)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
binddt
  (map G (ret T B ∘ map (fun A : Type => A) f)
   ∘ extract (prod W) (G A)) =
binddt (map G (ret T B) ∘ extract (prod W) (G B))
∘ map T (map G f)
        rewrite binddt_map.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
binddt
  (map G (ret T B ∘ map (fun A : Type => A) f)
   ∘ extract (prod W) (G A)) =
binddt
  (map G (ret T B) ∘ extract (prod W) (G B)
   ∘ map (prod W) (map G f))
        reassociate -> on right.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
binddt
  (map G (ret T B ∘ map (fun A : Type => A) f)
   ∘ extract (prod W) (G A)) =
binddt
  (map G (ret T B)
   ∘ (extract (prod W) (G B) ∘ map (prod W) (map G f)))
        rewrite <- (natural (Natural := Natural_extract_reader W)
                     (ϕ := @extract (W ×) _)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
binddt
  (map G (ret T B ∘ map (fun A : Type => A) f)
   ∘ extract (prod W) (G A)) =
binddt
  (map G (ret T B)
   ∘ (map (fun A : Type => A) (map G f)
      ∘ extract (prod W) (G A)))
        unfold_ops Map_I.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
binddt (map G (ret T B ∘ f) ∘ extract (prod W) (G A)) =
binddt
  (map G (ret T B)
   ∘ (map G f ∘ extract (prod W) (G A)))
        reassociate <- on right.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
binddt (map G (ret T B ∘ f) ∘ extract (prod W) (G A)) =
binddt
  (map G (ret T B) ∘ map G f ∘ extract (prod W) (G A))
        rewrite (fun_map_map (F := G)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
A, B: Type
f: A -> B
binddt (map G (ret T B ∘ f) ∘ extract (prod W) (G A)) =
binddt (map G (ret T B ∘ f) ∘ extract (prod W) (G A))

        reflexivity.
    Qed.

    Lemma dist_morph_T:
      forall (G1 G2: Type -> Type)
        (H2: Map G1) (H4: Mult G1) (H3: Pure G1) (H5: Map G2)
        (H7: Mult G2) (H6: Pure G2) (ϕ: forall A: Type, G1 A -> G2 A),
        ApplicativeMorphism G1 G2 ϕ ->
        forall A: Type, dist T G2 ∘ map T (ϕ A) = ϕ (T A) ∘ dist T G1.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G1 G2 : Type -> Type) (H2 : Map G1)
  (H4 : Mult G1) (H3 : Pure G1) (H5 : Map G2)
  (H7 : Mult G2) (H6 : Pure G2) (ϕ : G1 ⇒ G2),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist T G2 ∘ map T (ϕ A) = ϕ (T A) ∘ dist T G1
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G1 G2 : Type -> Type) (H2 : Map G1)
  (H4 : Mult G1) (H3 : Pure G1) (H5 : Map G2)
  (H7 : Mult G2) (H6 : Pure G2) (ϕ : G1 ⇒ G2),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist T G2 ∘ map T (ϕ A) = ϕ (T A) ∘ dist T G1
      introv morph; inversion morph; intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H2: Map G1
H4: Mult G1
H3: Pure G1
H5: Map G2
H7: Mult G2
H6: Pure G2
ϕ: G1 ⇒ G2
morph: ApplicativeMorphism G1 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 G1 f x) = map G2 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)
A: Type
dist T G2 ∘ map T (ϕ A) = ϕ (T A) ∘ dist T G1
      unfold_ops @Dist_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H2: Map G1
H4: Mult G1
H3: Pure G1
H5: Map G2
H7: Mult G2
H6: Pure G2
ϕ: G1 ⇒ G2
morph: ApplicativeMorphism G1 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 G1 f x) = map G2 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)
A: Type
binddt (map G2 (ret T A) ∘ extract (prod W) (G2 A))
∘ map T (ϕ A) =
ϕ (T A)
∘ binddt (map G1 (ret T A) ∘ extract (prod W) (G1 A))
      rewrite binddt_map.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H2: Map G1
H4: Mult G1
H3: Pure G1
H5: Map G2
H7: Mult G2
H6: Pure G2
ϕ: G1 ⇒ G2
morph: ApplicativeMorphism G1 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 G1 f x) = map G2 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)
A: Type
binddt
  (map G2 (ret T A) ∘ extract (prod W) (G2 A)
   ∘ map (prod W) (ϕ A)) =
ϕ (T A)
∘ binddt (map G1 (ret T A) ∘ extract (prod W) (G1 A))
      rewrite (kdtm_morph G1 G2 (ϕ := ϕ)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H2: Map G1
H4: Mult G1
H3: Pure G1
H5: Map G2
H7: Mult G2
H6: Pure G2
ϕ: G1 ⇒ G2
morph: ApplicativeMorphism G1 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 G1 f x) = map G2 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)
A: Type
binddt
  (map G2 (ret T A) ∘ extract (prod W) (G2 A)
   ∘ map (prod W) (ϕ A)) =
binddt
  (ϕ (T A)
   ∘ (map G1 (ret T A) ∘ extract (prod W) (G1 A)))
      reassociate -> on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H2: Map G1
H4: Mult G1
H3: Pure G1
H5: Map G2
H7: Mult G2
H6: Pure G2
ϕ: G1 ⇒ G2
morph: ApplicativeMorphism G1 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 G1 f x) = map G2 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)
A: Type
binddt
  (map G2 (ret T A)
   ∘ (extract (prod W) (G2 A) ∘ map (prod W) (ϕ A))) =
binddt
  (ϕ (T A)
   ∘ (map G1 (ret T A) ∘ extract (prod W) (G1 A)))
      rewrite <- (natural (Natural := Natural_extract_reader W)
                   (ϕ := @extract (W ×) _)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H2: Map G1
H4: Mult G1
H3: Pure G1
H5: Map G2
H7: Mult G2
H6: Pure G2
ϕ: G1 ⇒ G2
morph: ApplicativeMorphism G1 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 G1 f x) = map G2 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)
A: Type
binddt
  (map G2 (ret T A)
   ∘ (map (fun A : Type => A) (ϕ A)
      ∘ extract (prod W) (G1 A))) =
binddt
  (ϕ (T A)
   ∘ (map G1 (ret T A) ∘ extract (prod W) (G1 A)))
      unfold_ops Map_I.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H2: Map G1
H4: Mult G1
H3: Pure G1
H5: Map G2
H7: Mult G2
H6: Pure G2
ϕ: G1 ⇒ G2
morph: ApplicativeMorphism G1 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 G1 f x) = map G2 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)
A: Type
binddt
  (map G2 (ret T A) ∘ (ϕ A ∘ extract (prod W) (G1 A))) =
binddt
  (ϕ (T A)
   ∘ (map G1 (ret T A) ∘ extract (prod W) (G1 A)))
      reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H2: Map G1
H4: Mult G1
H3: Pure G1
H5: Map G2
H7: Mult G2
H6: Pure G2
ϕ: G1 ⇒ G2
morph: ApplicativeMorphism G1 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 G1 f x) = map G2 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)
A: Type
binddt
  (map G2 (ret T A) ∘ ϕ A ∘ extract (prod W) (G1 A)) =
binddt
  (ϕ (T A)
   ∘ (map G1 (ret T A) ∘ extract (prod W) (G1 A)))
      rewrite (natural (ϕ := ϕ)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1, G2: Type -> Type
H2: Map G1
H4: Mult G1
H3: Pure G1
H5: Map G2
H7: Mult G2
H6: Pure G2
ϕ: G1 ⇒ G2
morph: ApplicativeMorphism G1 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 G1 f x) = map G2 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)
A: Type
binddt
  (ϕ (T A) ∘ map G1 (ret T A)
   ∘ extract (prod W) (G1 A)) =
binddt
  (ϕ (T A)
   ∘ (map G1 (ret T A) ∘ extract (prod W) (G1 A)))
      reflexivity.
    Qed.

    Lemma dist_unit_T: forall A: Type,
        dist T (fun A0: Type => A0) = @id (T A).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type, dist T (fun A0 : Type => A0) = id
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall A : Type, dist T (fun A0 : Type => A0) = id
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
dist T (fun A0 : Type => A0) = id unfold_ops @Dist_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
A: Type
binddt
  (map (fun A0 : Type => A0) (ret T A)
   ∘ extract (prod W) A) = id
      apply (kdtm_binddt1).
    Qed.

    Lemma dist_linear_T:
      forall (G1: Type -> Type)
        (H2: Map G1) (H3: Pure G1) (H4: Mult G1),
        Applicative G1 ->
        forall (G2: Type -> Type)
          (H6: Map G2) (H7: Pure G2) (H8: Mult G2),
          Applicative G2 ->
          forall (A: Type),
            dist T (G1 ∘ G2) (A := A) = map G1 (dist T G2) ∘ dist T G1.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G1 : Type -> Type) (H2 : Map G1)
  (H3 : Pure G1) (H4 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H6 : Map G2)
  (H7 : Pure G2) (H8 : Mult G2),
Applicative G2 ->
forall A : Type,
dist T (G1 ∘ G2) = map G1 (dist T G2) ∘ dist T G1
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G1 : Type -> Type) (H2 : Map G1)
  (H3 : Pure G1) (H4 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H6 : Map G2)
  (H7 : Pure G2) (H8 : Mult G2),
Applicative G2 ->
forall A : Type,
dist T (G1 ∘ G2) = map G1 (dist T G2) ∘ dist T G1
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H0: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H1: Applicative G2
A: Type
dist T (G1 ∘ G2) = map G1 (dist T G2) ∘ dist T G1 unfold_ops @Dist_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H0: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H1: Applicative G2
A: Type
binddt
  (map (G1 ∘ G2) (ret T A)
   ∘ extract (prod W) ((G1 ∘ G2) A)) =
map G1
  (binddt (map G2 (ret T A) ∘ extract (prod W) (G2 A)))
∘ binddt
    (map G1 (ret T (G2 A))
     ∘ extract (prod W) (G1 (G2 A)))
      rewrite (kdtm_binddt2); try typeclasses eauto.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H0: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H1: Applicative G2
A: Type
binddt
  (map (G1 ∘ G2) (ret T A)
   ∘ extract (prod W) ((G1 ∘ G2) A)) =
binddt
  (map G2 (ret T A) ∘ extract (prod W) (G2 A)
   ⋆7 map G1 (ret T (G2 A))
      ∘ extract (prod W) (G1 (G2 A)))
      change (map G2 (ret T A)) with (map G2 (ret T A) ∘ id).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H0: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H1: Applicative G2
A: Type
binddt
  (map (G1 ∘ G2) (ret T A)
   ∘ extract (prod W) ((G1 ∘ G2) A)) =
binddt
  (map G2 (ret T A) ∘ id ∘ extract (prod W) (G2 A)
   ⋆7 map G1 (ret T (G2 A))
      ∘ extract (prod W) (G1 (G2 A)))
      rewrite kc7_27.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H0: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H1: Applicative G2
A: Type
binddt
  (map (G1 ∘ G2) (ret T A)
   ∘ extract (prod W) ((G1 ∘ G2) A)) =
binddt
  (map G1 (traverse T G2 id)
   ∘ (map G1 (ret T (G2 A))
      ∘ extract (prod W) (G1 (G2 A))))
      reassociate <- on right.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H0: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H1: Applicative G2
A: Type
binddt
  (map (G1 ∘ G2) (ret T A)
   ∘ extract (prod W) ((G1 ∘ G2) A)) =
binddt
  (map G1 (traverse T G2 id) ∘ map G1 (ret T (G2 A))
   ∘ extract (prod W) (G1 (G2 A)))
      rewrite (fun_map_map).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H0: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H1: Applicative G2
A: Type
binddt
  (map (G1 ∘ G2) (ret T A)
   ∘ extract (prod W) ((G1 ∘ G2) A)) =
binddt
  (map G1 (traverse T G2 id ∘ ret T (G2 A))
   ∘ extract (prod W) (G1 (G2 A)))
      rewrite (traverse_ret G2).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H0: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H1: Applicative G2
A: Type
binddt
  (map (G1 ∘ G2) (ret T A)
   ∘ extract (prod W) ((G1 ∘ G2) A)) =
binddt
  (map G1 (map G2 (ret T A) ∘ id)
   ∘ extract (prod W) (G1 (G2 A)))
      reflexivity.
    Qed.

    #[export] Instance:
      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 (G A) = map G (ret T A).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G : Type -> Type) (H3 : Map G) (H4 : Pure G)
  (H5 : Mult G),
Applicative G ->
forall A : Type,
dist T G ∘ ret T (G A) = map G (ret T A)
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G : Type -> Type) (H3 : Map G) (H4 : Pure G)
  (H5 : Mult G),
Applicative G ->
forall A : Type,
dist T G ∘ ret T (G A) = map G (ret T A)
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
dist T G ∘ ret T (G A) = map G (ret T A) unfold_ops @Dist_Binddt @Map_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
binddt (map G (ret T A) ∘ extract (prod W) (G A))
∘ ret T (G A) = map G (ret T A)
      rewrite (kdtm_binddt0).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
H0: Applicative G
A: Type
map G (ret T A) ∘ extract (prod W) (G A)
∘ ret (prod W) (G A) = map G (ret T A)
      reflexivity.
    Qed.

    Lemma trvmon_join_T:
      forall (G: Type -> Type) (H3: Map G)
        (H4: Pure G) (H5: Mult G)
        (Happ: Applicative G),
      forall (A: Type),
        dist T G ∘ join T =
          map G (join T) ∘ dist T G ∘ map T (dist T G (A := A)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G : Type -> Type) (H3 : Map G) (H4 : Pure G)
  (H5 : Mult G),
Applicative G ->
forall A : Type,
dist T G ∘ join T =
map G (join T) ∘ dist T G ∘ map T (dist T G)
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G : Type -> Type) (H3 : Map G) (H4 : Pure G)
  (H5 : Mult G),
Applicative G ->
forall A : Type,
dist T G ∘ join T =
map G (join T) ∘ dist T G ∘ map T (dist T G)
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
dist T G ∘ join T =
map G (join T) ∘ dist T G ∘ map T (dist T G)
      unfold_ops @Dist_Binddt @Join_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
binddt (map G (ret T A) ∘ extract (prod W) (G A))
∘ binddt (extract (prod W) (T (G A))) =
map G (binddt (extract (prod W) (T A)))
∘ binddt
    (map G (ret T (T A)) ∘ extract (prod W) (G (T A)))
∘ map T
    (binddt (map G (ret T A) ∘ extract (prod W) (G A)))
      repeat rewrite <- mapdt_to_binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
mapdt T G (extract (prod W) (G A))
∘ binddt (extract (prod W) (T (G A))) =
map G (binddt (extract (prod W) (T A)))
∘ mapdt T G (extract (prod W) (G (T A)))
∘ map T (mapdt T G (extract (prod W) (G A)))
      repeat binddt_to_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
mapdt T G (extract (prod W) (G A))
∘ bindd T (extract (prod W) (T (G A))) =
map G (bindd T (extract (prod W) (T A)))
∘ mapdt T G (extract (prod W) (G (T A)))
∘ map T (mapdt T G (extract (prod W) (G A)))
      unfold_compose_in_compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
mapdt T G (extract (prod W) (G A))
∘ bindd T (extract (prod W) (T (G A))) =
map G (bindd T (extract (prod W) (T A)))
∘ mapdt T G (extract (prod W) (G (T A)))
∘ map T (mapdt T G (extract (prod W) (G A)))
      rewrite mapdt_bindd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
binddt
  (fun '(w, a) =>
   mapdt T G (extract (prod W) (G A) ⦿ w)
     (extract (prod W) (T (G A)) (w, a))) =
map G (bindd T (extract (prod W) (T A)))
∘ mapdt T G (extract (prod W) (G (T A)))
∘ map T (mapdt T G (extract (prod W) (G A)))
      unfold compose at 4.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
binddt
  (fun '(w, a) =>
   mapdt T G (extract (prod W) (G A) ⦿ w)
     (extract (prod W) (T (G A)) (w, a))) =
map G (bindd T (extract (prod W) (T A)))
∘ mapdt T G (extract (prod W) (G (T A)))
∘ map T (mapdt T G (extract (prod W) (G A)))
      rewrite bindd_mapdt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
binddt
  (fun '(w, a) =>
   mapdt T G (extract (prod W) (G A) ⦿ w)
     (extract (prod W) (T (G A)) (w, a))) =
binddt
  (fun '(w, a) =>
   map G (extract (prod W) (T A) ∘ pair w)
     (extract (prod W) (G (T A)) (w, a)))
∘ map T (mapdt T G (extract (prod W) (G A)))
      rewrite binddt_map.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
binddt
  (fun '(w, a) =>
   mapdt T G (extract (prod W) (G A) ⦿ w)
     (extract (prod W) (T (G A)) (w, a))) =
binddt
  ((fun '(w, a) =>
    map G (extract (prod W) (T A) ∘ pair w)
      (extract (prod W) (G (T A)) (w, a)))
   ∘ map (prod W) (mapdt T G (extract (prod W) (G A))))
      fequal.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
(fun '(w, a) =>
 mapdt T G (extract (prod W) (G A) ⦿ w)
   (extract (prod W) (T (G A)) (w, a))) =
(fun '(w, a) =>
 map G (extract (prod W) (T A) ∘ pair w)
   (extract (prod W) (G (T A)) (w, a)))
∘ map (prod W) (mapdt T G (extract (prod W) (G A)))
      ext [w a].
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
w: W
a: T (G A)
mapdt T G (extract (prod W) (G A) ⦿ w)
  (extract (prod W) (T (G A)) (w, a)) =
((fun '(w, a) =>
  map G (extract (prod W) (T A) ∘ pair w)
    (extract (prod W) (G (T A)) (w, a)))
 ∘ map (prod W) (mapdt T G (extract (prod W) (G A))))
  (w, a)
      unfold compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
w: W
a: T (G A)
mapdt T G (extract (prod W) (G A) ⦿ w)
  (extract (prod W) (T (G A)) (w, a)) =
(let
 '(w, a) :=
  map (prod W) (mapdt T G (extract (prod W) (G A)))
    (w, a) in
  map G (extract (prod W) (T A) ○ pair w)
    (extract (prod W) (G (T A)) (w, a))) cbn.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
w: W
a: T (G A)
mapdt T G (extract (prod W) (G A) ⦿ w) a =
map G (fun a : T A => a)
  (mapdt T G (extract (prod W) (G A)) a)
      change (fun a0 => a0) with (@id (T A)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
w: W
a: T (G A)
mapdt T G (extract (prod W) (G A) ⦿ w) a =
map G id (mapdt T G (extract (prod W) (G A)) a)
      unfold compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
w: W
a: T (G A)
mapdt T G (extract (prod W) (G A) ⦿ w) a =
map G id (mapdt T G (extract (prod W) (G A)) a) cbn.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
w: W
a: T (G A)
mapdt T G (extract (prod W) (G A) ⦿ w) a =
map G id (mapdt T G (extract (prod W) (G A)) a)
      inversion Happ.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
w: W
a: T (G A)
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
mapdt T G (extract (prod W) (G A) ⦿ w) a =
map G id (mapdt T G (extract (prod W) (G A)) a)
      rewrite (fun_map_id (F := G)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
w: W
a: T (G A)
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
mapdt T G (extract (prod W) (G A) ⦿ w) a =
id (mapdt T G (extract (prod W) (G A)) a)
      rewrite extract_preincr.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H3: Map G
H4: Pure G
H5: Mult G
Happ: Applicative G
A: Type
w: W
a: T (G A)
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
mapdt T G (extract (prod W) (G A)) a =
id (mapdt T G (extract (prod W) (G A)) a)
      reflexivity.
    Qed.

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

    (** ** Decorated Traversable Functor instance *)
    (******************************************************************)
    Lemma dtfun_compat_T:
      forall (G: Type -> Type) (H2: Map G) (H3: Pure G) (H4: Mult G)
             (Happ: Applicative G),
      forall (A: Type),
        dist T G ∘ map T (strength) ∘ dec (A := G A) T =
          map G (dec T) ∘ dist T G.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G : Type -> Type) (H2 : Map G) (H3 : Pure G)
  (H4 : Mult G),
Applicative G ->
forall A : Type,
dist T G ∘ map T strength ∘ dec T =
map G (dec T) ∘ dist T G
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G : Type -> Type) (H2 : Map G) (H3 : Pure G)
  (H4 : Mult G),
Applicative G ->
forall A : Type,
dist T G ∘ map T strength ∘ dec T =
map G (dec T) ∘ dist T G
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
dist T G ∘ map T strength ∘ dec T =
map G (dec T) ∘ dist T G unfold_ops @Dist_Binddt @Decorate_Binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
binddt
  (map G (ret T (W * A))
   ∘ extract (prod W) (G (W * A))) ∘ map T strength
∘ binddt (ret T (W * G A)) =
map G (binddt (ret T (W * A)))
∘ binddt (map G (ret T A) ∘ extract (prod W) (G A))
      change (ret T (W * G A)) with (ret T (W * G A) ∘ id).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
binddt
  (map G (ret T (W * A))
   ∘ extract (prod W) (G (W * A))) ∘ map T strength
∘ binddt (ret T (W * G A) ∘ id) =
map G (binddt (ret T (W * A)))
∘ binddt (map G (ret T A) ∘ extract (prod W) (G A))
      rewrite <- mapd_to_binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
binddt
  (map G (ret T (W * A))
   ∘ extract (prod W) (G (W * A))) ∘ map T strength
∘ mapd T id =
map G (binddt (ret T (W * A)))
∘ binddt (map G (ret T A) ∘ extract (prod W) (G A))
      rewrite <- bindd_to_binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
binddt
  (map G (ret T (W * A))
   ∘ extract (prod W) (G (W * A))) ∘ map T strength
∘ mapd T id =
map G (bindd T (ret T (W * A)))
∘ binddt (map G (ret T A) ∘ extract (prod W) (G A))
      reassociate -> on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
binddt
  (map G (ret T (W * A))
   ∘ extract (prod W) (G (W * A)))
∘ (map T strength ∘ mapd T id) =
map G (bindd T (ret T (W * A)))
∘ binddt (map G (ret T A) ∘ extract (prod W) (G A))
      rewrite map_mapd.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
binddt
  (map G (ret T (W * A))
   ∘ extract (prod W) (G (W * A)))
∘ mapd T (strength ∘ id) =
map G (bindd T (ret T (W * A)))
∘ binddt (map G (ret T A) ∘ extract (prod W) (G A))
      do 2 rewrite <- mapdt_to_binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
mapdt T G (extract (prod W) (G (W * A)))
∘ mapd T (strength ∘ id) =
map G (bindd T (ret T (W * A)))
∘ mapdt T G (extract (prod W) (G A))
      change (extract (prod W) ?A) with (id ∘ extract (prod W) A).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
mapdt T G (id ∘ extract (prod W) (G (W * A)))
∘ mapd T (strength ∘ id) =
map G (bindd T (ret T (W * A)))
∘ mapdt T G (id ∘ extract (prod W) (G A))
      rewrite (mapdt_mapd).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
mapdt T G
  (id ∘ extract (prod W) (G (W * A)) ⋆1 strength ∘ id) =
map G (bindd T (ret T (W * A)))
∘ mapdt T G (id ∘ extract (prod W) (G A))
      rewrite (bindd_mapdt).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
mapdt T G
  (id ∘ extract (prod W) (G (W * A)) ⋆1 strength ∘ id) =
binddt
  (fun '(w, a) =>
   map G (ret T (W * A) ∘ pair w)
     ((id ∘ extract (prod W) (G A)) (w, a)))
      rewrite mapdt_to_binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
binddt
  (map G (ret T (W * A))
   ∘ (id ∘ extract (prod W) (G (W * A))
      ⋆1 strength ∘ id)) =
binddt
  (fun '(w, a) =>
   map G (ret T (W * A) ∘ pair w)
     ((id ∘ extract (prod W) (G A)) (w, a)))
      rewrite kc1_01.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
binddt
  (map G (ret T (W * A)) ∘ (id ∘ (strength ∘ id))) =
binddt
  (fun '(w, a) =>
   map G (ret T (W * A) ∘ pair w)
     ((id ∘ extract (prod W) (G A)) (w, a)))
      fequal.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
map G (ret T (W * A)) ∘ (id ∘ (strength ∘ id)) =
(fun '(w, a) =>
 map G (ret T (W * A) ∘ pair w)
   ((id ∘ extract (prod W) (G A)) (w, a)))
      ext [w a].
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
w: W
a: G A
(map G (ret T (W * A)) ∘ (id ∘ (strength ∘ id)))
  (w, a) =
map G (ret T (W * A) ∘ pair w)
  ((id ∘ extract (prod W) (G A)) (w, a))
      unfold compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
w: W
a: G A
map G (ret T (W * A)) (id (strength (id (w, a)))) =
map G (ret T (W * A) ○ pair w)
  (id (extract (prod W) (G A) (w, a))) cbn.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
w: W
a: G A
map G (ret T (W * A)) (map G (pair w) a) =
map G (ret T (W * A) ○ pair w) a
      compose near a on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
w: W
a: G A
(map G (ret T (W * A)) ∘ map G (pair w)) a =
map G (ret T (W * A) ○ pair w) a
      inversion Happ.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
w: W
a: G A
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
(map G (ret T (W * A)) ∘ map G (pair w)) a =
map G (ret T (W * A) ○ pair w) a
      rewrite (fun_map_map (F := G)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
Happ: Applicative G
A: Type
w: W
a: G A
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map G f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map G f x, map G g y) =
map G (map_tensor f g)
  (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map G α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map G left_unitor (mult (pure tt, x)) =
x
app_unital_r: forall (A : Type) (x : G A),
map G right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
map G (ret T (W * A) ∘ pair w) a =
map G (ret T (W * A) ○ pair w) a
      reflexivity.
    Qed.

    #[export] Instance:
      Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor W T :=
      {| dtfun_compat := dtfun_compat_T;
      |}.

    (** *** Decorated Traversable monad instance *)
    (******************************************************************)
    #[export] Instance:
      Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad W T :=
      ltac:(constructor; typeclasses eauto).

  End with_monad.
End DerivedInstances.