From Tealeaves Require Import
  Classes.Categorical.DecoratedTraversableMonad
  Classes.Kleisli.DecoratedTraversableMonad
  CategoricalToKleisli.DecoratedMonad
  CategoricalToKleisli.DecoratedFunctor (cobind_dec).

Import Product.Notations.
Import Kleisli.Monad.Notations.
Import Kleisli.DecoratedTraversableMonad.Notations.
Import Categorical.Monad.Notations.
Import Categorical.TraversableFunctor.Notations.
Import Strength.Notations.

#[local] Generalizable Variables W T G ϕ A B C.

#[local] Tactic Notation "bring" constr(x) "and" constr(y) "together" :=
  change (?f ∘ x ∘ y ∘ ?g) with (f ∘ (x ∘ y) ∘ g).

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

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

  #[export] Instance Binddt_Categorical
    (W: Type)
    (T: Type -> Type)
    `{Map T}
    `{Decorate W T}
    `{ApplicativeDist T}
    `{Join T}: Binddt W T T :=
  fun (G: Type -> Type) `{Map G} `{Pure G} `{Mult G} (A B: Type)
    (f: W * A -> G (T B)) =>
    map (F := G) join ∘ dist T G ∘ map f ∘ dec T.

End DerivedOperations.

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

  Import DerivedOperations.

  Section adapter.

    Context
      `{Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad W T}.

    Context
      (G1: Type -> Type)
      `{Map G1} `{Pure G1} `{Mult G1} `{! Applicative G1}
      (G2: Type -> Type)
      `{Map G2} `{Pure G2} `{Mult G2} `{! Applicative G2}.

    Definition kcompose_dtm_alt {A B C} :=
      fun `(g: W * B -> G2 (T C))
        `(f: W * A -> G1 (T B))
      => (map (F := G1) ((map (F := G2) (μ))
                          ∘ δ T G2
                          ∘ map (F := T) (g ∘ μ (T := (W ×)))
                          ∘ σ
                          ∘ map (F := (W ×)) (dec T)))
          ∘ σ
          ∘ cobind (W := (W ×)) f.

    Lemma equiv' {A B C}:
      forall  `(g: W * B -> G2 (T C))
         `(f: W * A -> G1 (T B)),
        g ⋆7 f =
          kcompose_dtm_alt g f.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
forall (g : W * B -> G2 (T C)) (f : W * A -> G1 (T B)),
g ⋆7 f = kcompose_dtm_alt g f
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
forall (g : W * B -> G2 (T C)) (f : W * A -> G1 (T B)),
g ⋆7 f = kcompose_dtm_alt g f
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
g ⋆7 f = kcompose_dtm_alt g f unfold kc7.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
(fun '(w, a) => map (binddt (preincr g w)) (f (w, a))) =
kcompose_dtm_alt g f
      unfold_ops @Binddt_Categorical.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
(fun '(w, a) =>
 map (map (μ) ∘ δ T G2 ∘ map (preincr g w) ∘ dec T)
   (f (w, a))) = kcompose_dtm_alt g f
      ext [w a].
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
map (map (μ) ∘ δ T G2 ∘ map (preincr g w) ∘ dec T)
  (f (w, a)) = kcompose_dtm_alt g f (w, a)
      unfold kcompose_dtm_alt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
map (map (μ) ∘ δ T G2 ∘ map (preincr g w) ∘ dec T)
  (f (w, a)) =
(map
   (map (μ) ∘ δ T G2 ∘ map (g ∘ μ) ∘ σ ∘ map (dec T))
 ∘ σ ∘ cobind f) (w, a)
      unfold compose at 6.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
map (map (μ) ∘ δ T G2 ∘ map (preincr g w) ∘ dec T)
  (f (w, a)) =
(map
   (map (μ) ∘ δ T G2 ∘ map (g ∘ μ) ∘ σ ∘ map (dec T))
 ∘ σ) (cobind f (w, a)) cbn.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
map (map (μ) ∘ δ T G2 ∘ map (preincr g w) ∘ dec T)
  (f (w, a)) =
(map
   (map (μ) ∘ δ T G2 ∘ map (g ∘ μ) ∘ σ ∘ map (dec T))
 ∘ σ) (w, f (w, a))
      unfold compose at 6.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
map (map (μ) ∘ δ T G2 ∘ map (preincr g w) ∘ dec T)
  (f (w, a)) =
map (map (μ) ∘ δ T G2 ∘ map (g ∘ μ) ∘ σ ∘ map (dec T))
  (σ (w, f (w, a)))
      cbn.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
map (map (μ) ∘ δ T G2 ∘ map (preincr g w) ∘ dec T)
  (f (w, a)) =
map (map (μ) ∘ δ T G2 ∘ map (g ∘ μ) ∘ σ ∘ map (dec T))
  (map (pair w) (f (w, a))) compose near (f (w, a)) on right.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
map (map (μ) ∘ δ T G2 ∘ map (preincr g w) ∘ dec T)
  (f (w, a)) =
(map
   (map (μ) ∘ δ T G2 ∘ map (g ∘ μ) ∘ σ ∘ map (dec T))
 ∘ map (pair w)) (f (w, a))
      rewrite (fun_map_map (F := G1) (Functor := app_functor)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
map (map (μ) ∘ δ T G2 ∘ map (preincr g w) ∘ dec T)
  (f (w, a)) =
map
  (map (μ) ∘ δ T G2 ∘ map (g ∘ μ) ∘ σ ∘ map (dec T)
   ∘ pair w) (f (w, a))
      repeat fequal.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
map (μ) ∘ δ T G2 ∘ map (preincr g w) ∘ dec T =
map (μ) ∘ δ T G2 ∘ map (g ∘ μ) ∘ σ ∘ map (dec T)
∘ pair w
      ext t.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
t: T B
(map (μ) ∘ δ T G2 ∘ map (preincr g w) ∘ dec T) t =
(map (μ) ∘ δ T G2 ∘ map (g ∘ μ) ∘ σ ∘ map (dec T)
 ∘ pair w) t
      unfold compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
t: T B
map (μ) (δ T G2 (map (preincr g w) (dec T t))) =
map (μ)
  (δ T G2 (map (g ○ μ) (σ (map (dec T) (w, t))))) cbn.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
t: T B
map (μ) (δ T G2 (map (preincr g w) (dec T t))) =
map (μ)
  (δ T G2 (map (g ○ μ) (map (pair (id w)) (dec T t))))
      compose near (dec T t).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
t: T B
map (μ) ((δ T G2 ∘ map (preincr g w)) (dec T t)) =
map (μ)
  (δ T G2
     ((map (g ○ μ) ∘ map (pair (id w))) (dec T t)))
      unfold compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
t: T B
map (μ) (δ T G2 (map (preincr g w) (dec T t))) =
map (μ)
  (δ T G2 (map (g ○ μ) (map (pair (id w)) (dec T t)))) cbn.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
t: T B
map (μ) (δ T G2 (map (preincr g w) (dec T t))) =
map (μ)
  (δ T G2 (map (g ○ μ) (map (pair (id w)) (dec T t))))
      compose near (dec T t) on right.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
t: T B
map (μ) (δ T G2 (map (preincr g w) (dec T t))) =
map (μ)
  (δ T G2
     ((map (g ○ μ) ∘ map (pair (id w))) (dec T t)))
      rewrite (fun_map_map (F := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
t: T B
map (μ) (δ T G2 (map (preincr g w) (dec T t))) =
map (μ) (δ T G2 (map (g ○ μ ∘ pair (id w)) (dec T t)))
      unfold compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
t: T B
map (μ) (δ T G2 (map (preincr g w) (dec T t))) =
map (μ)
  (δ T G2
     (map (fun a : W * B => g (μ (id w, a))) (dec T t)))
      repeat fequal.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
A, B, C: Type
g: W * B -> G2 (T C)
f: W * A -> G1 (T B)
w: W
a: A
t: T B
preincr g w = (fun a : W * B => g (μ (id w, a)))
      now ext [w' b].
    Qed.

  End adapter.

  Section with_monad.

    Context
      `{Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad W T}.

    Theorem kdtm_binddt1_T {A}:
      binddt (G := fun A => A) (η (T := T) ∘ extract) = @id (T A).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
A: Type
binddt (η ∘ extract) = id
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
A: Type
binddt (η ∘ extract) = id
      unfold_ops @Binddt_Categorical.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
A: Type
map (μ) ∘ δ T (fun A : Type => A) ∘ map (η ∘ extract)
∘ dec T = id
      change (map (F := fun A => A) ?f) with f.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
A: Type
μ ∘ δ T (fun A : Type => A) ∘ map (η ∘ extract)
∘ dec T = id
      rewrite (dist_unit (F := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
A: Type
μ ∘ id ∘ map (η ∘ extract) ∘ dec T = id
      change (?mu ∘ id) with mu.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
A: Type
μ ∘ map (η ∘ extract) ∘ dec T = id
      rewrite <- fun_map_map.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
A: Type
μ ∘ (map (η) ∘ map extract) ∘ dec T = id
      do 2 reassociate -> on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
A: Type
μ ∘ (map (η) ∘ (map extract ∘ dec T)) = id
      rewrite dfun_dec_extract.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
A: Type
μ ∘ (map (η) ∘ id) = id
      reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
A: Type
μ ∘ map (η) ∘ id = id
      rewrite (mon_join_map_ret (T := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
A: Type
id ∘ id = id
      reflexivity.
    Qed.

    Theorem kdtm_binddt0_T: forall
        (G: Type -> Type) `{Map G} `{Pure G} `{Mult G} `{! Applicative G}
        (A B: Type)
        (f: W * A -> G (T B)),
        binddt f ∘ η (T := T) = f ∘ η (T := (W ×)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
forall (G : Type -> Type) (H5 : Map G) (H6 : Pure G)
  (H7 : Mult G),
Applicative G ->
forall (A B : Type) (f : W * A -> G (T B)),
binddt f ∘ η = f ∘ η
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
forall (G : Type -> Type) (H5 : Map G) (H6 : Pure G)
  (H7 : Mult G),
Applicative G ->
forall (A B : Type) (f : W * A -> G (T B)),
binddt f ∘ η = f ∘ η
      intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f ∘ η = f ∘ η
      unfold_ops @Binddt_Categorical.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
map (μ) ∘ δ T G ∘ map f ∘ dec T ∘ η = f ∘ η
      reassociate -> on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
map (μ) ∘ δ T G ∘ map f ∘ (dec T ∘ η) = f ∘ η
      rewrite (dmon_ret (W := W) (T := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
map (μ) ∘ δ T G ∘ map f ∘ (η ∘ pair (monoid_unit W)) =
f ∘ η
      reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
map (μ) ∘ δ T G ∘ map f ∘ η ∘ pair (monoid_unit W) =
f ∘ η
      reassociate -> near (η (A := W * A)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
map (μ) ∘ δ T G ∘ (map f ∘ η) ∘ pair (monoid_unit W) =
f ∘ η
      rewrite (natural (ϕ := @ret T _)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
map (μ) ∘ δ T G ∘ (η ∘ map f) ∘ pair (monoid_unit W) =
f ∘ η
      unfold_ops @Map_I.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
map (μ) ∘ δ T G ∘ (η ∘ f) ∘ pair (monoid_unit W) =
f ∘ η
      reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
map (μ) ∘ δ T G ∘ η ∘ f ∘ pair (monoid_unit W) = f ∘ η
      reassociate -> near (η (A := G (T B))).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
map (μ) ∘ (δ T G ∘ η) ∘ f ∘ pair (monoid_unit W) =
f ∘ η
      rewrite (trvmon_ret (T := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
map (μ) ∘ map (η) ∘ f ∘ pair (monoid_unit W) = f ∘ η
      rewrite (fun_map_map (F := G) (Functor := app_functor)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
map (μ ∘ η) ∘ f ∘ pair (monoid_unit W) = f ∘ η
      rewrite (mon_join_ret (T := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
map id ∘ f ∘ pair (monoid_unit W) = f ∘ η
      rewrite (fun_map_id (F := G) (Functor := app_functor)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G: Type -> Type
H5: Map G
H6: Pure G
H7: Mult G
Applicative0: Applicative G
A, B: Type
f: W * A -> G (T B)
id ∘ f ∘ pair (monoid_unit W) = f ∘ η
      reflexivity.
    Qed.

    Section binddt_binddt.

      Context
        (G1: Type -> Type)
        `{Map G1} `{Pure G1} `{Mult G1} `{! Applicative G1}
        (G2: Type -> Type)
        `{Map G2} `{Pure G2} `{Mult G2} `{! Applicative G2}
        `(g: W * B -> G2 (T C)) `(f: W * A -> G1 (T B)).

      #[local] Arguments map (F)%function_scope {Map}
        {A B}%type_scope f%function_scope _.
      #[local] Arguments dist F%function_scope {ApplicativeDist}
        G%function_scope {H H0 H1} (A)%type_scope _.
      #[local] Arguments dec {E}%type_scope F%function_scope
        {Decorate} (A)%type_scope _.
      #[local] Arguments join {T}%function_scope
        {Join} (A)%type_scope _.

      Theorem kdtm_binddt2_T:
        map G1 (binddt (G := G2) g) ∘ binddt (G := G1) f =
          binddt (G := G1 ∘ G2) (g ⋆7 f).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
map G1 (binddt g) ∘ binddt f = binddt (g ⋆7 f)
      Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
map G1 (binddt g) ∘ binddt f = binddt (g ⋆7 f)
        rewrite (equiv' _ _ g f).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
map G1 (binddt g) ∘ binddt f =
binddt (kcompose_dtm_alt G1 G2 g f)
        unfold kcompose_dtm_alt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
map G1 (binddt g) ∘ binddt f =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        (* ********** *)
        unfold binddt at 1 2; unfold Binddt_Categorical.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
map G1
  (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g ∘ dec T B)
∘ (map G1 (μ B) ∘ δ T G1 (T B) ∘ map T f ∘ dec T A) =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        assert (Functor G1) by now inversion Applicative0.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
map G1
  (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g ∘ dec T B)
∘ (map G1 (μ B) ∘ δ T G1 (T B) ∘ map T f ∘ dec T A) =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        assert (Functor G2) by now inversion Applicative1.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1
  (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g ∘ dec T B)
∘ (map G1 (μ B) ∘ δ T G1 (T B) ∘ map T f ∘ dec T A) =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        (* Normalize associativity *)
        do 3 reassociate <-.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1
  (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g ∘ dec T B)
∘ map G1 (μ B) ∘ δ T G1 (T B) ∘ map T f ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        (* Bring together <<map G1 (dec T B)>> and <<map G1 (μ B)>> *)
        rewrite <- (fun_map_map (F := G1) (Functor := app_functor)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1 (dec T B) ∘ map G1 (μ B) ∘ δ T G1 (T B)
∘ map T f ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        bring (map G1 (dec T B)) and (map G1 (μ B)) together.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ (map G1 (dec T B) ∘ map G1 (μ B)) ∘ δ T G1 (T B)
∘ map T f ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (fun_map_map (F := G1) (Functor := app_functor)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1 (dec T B ∘ μ B) ∘ δ T G1 (T B) ∘ map T f
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite dmon_join.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T) ∘ dec T (T (W * B))
     ∘ map T (dec T B)) ∘ δ T G1 (T B) ∘ map T f
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        (* Move <<dec T (T (W * B))>> towards <<dec T A>> *)
        reassociate -> near (map T (dec T B)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ (dec T (T (W * B)) ∘ map T (dec T B)))
∘ δ T G1 (T B) ∘ map T f ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite <- (natural (ϕ := @dec W T _)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ (map (T ○ prod W) (dec T B) ∘ dec T (T B)))
∘ δ T G1 (T B) ∘ map T f ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ map (T ○ prod W) (dec T B) ∘ dec T (T B))
∘ δ T G1 (T B) ∘ map T f ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite <- (fun_map_map
                      (F := G1)
                      _ _ _
                      (dec T (T B))).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ (map G1
     (μ (W * B) ∘ map T (shift T)
      ∘ map (T ○ prod W) (dec T B))
   ∘ map G1 (dec T (T B))) ∘ δ T G1 (T B) ∘ map T f
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ map (T ○ prod W) (dec T B))
∘ map G1 (dec T (T B)) ∘ δ T G1 (T B) ∘ map T f
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        bring (map G1 (dec T (T B))) and (δ T G1 (T B)) together.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ map (T ○ prod W) (dec T B))
∘ (map G1 (dec T (T B)) ∘ δ T G1 (T B)) ∘ map T f
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite <- (dtfun_compat (F := T) (G := G1)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ map (T ○ prod W) (dec T B))
∘ (δ T G1 (W * T B) ∘ map T (σ) ∘ dec T (G1 (T B)))
∘ map T f ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        do 2 reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ dec T (G1 (T B)) ∘ map T f ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        bring (dec T (G1 (T B))) and (map T f) together.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ (dec T (G1 (T B)) ∘ map T f) ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite <- (natural (ϕ := @dec W T _)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ (map (T ○ prod W) f ∘ dec T (W * A))
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        change (map (T ○ prod W) f) with (map (T ∘ prod W) f).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ (map (T ∘ prod W) f ∘ dec T (W * A))
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ dec T (W * A)
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate -> near (dec T A).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f
∘ (dec T (W * A) ∘ dec T A) =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        (* Change decorate-then-decorate into decorate-then-duplicate *)
        rewrite dfun_dec_dec.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f
∘ (map T cojoin ∘ dec T A) =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (shift T)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        (* Now move <<μ B>> towards <<μ C>> *)
        unfold shift.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (map T (uncurry incr) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite incr_spec.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B) ∘ map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        change (μ (W * B) ∘ map T (map T (μ B) ∘ σ) ∘ map (T ○ prod W) (dec T B)) with
          (μ (W * B) ∘ (map T (map T (μ B) ∘ σ) ∘ map (T ○ prod W) (dec T B))).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1
    (μ (W * B)
     ∘ (map T (map T (μ B) ∘ σ)
        ∘ map (T ○ prod W) (dec T B)))
∘ δ T G1 (W * T B) ∘ map T (σ) ∘ map (T ∘ prod W) f
∘ map T cojoin ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite <- (fun_map_map (F := G1) (Functor := app_functor) _ _ _ _ (μ (W * B))).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ (map G1 (μ (W * B))
   ∘ map G1
       (map T (map T (μ B) ∘ σ)
        ∘ map (T ○ prod W) (dec T B)))
∘ δ T G1 (W * T B) ∘ map T (σ) ∘ map (T ∘ prod W) f
∘ map T cojoin ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map G1 (μ (W * B))
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (fun_map_map (F := G1) _ _ _ (μ (W * B))).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1
  (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g ∘ μ (W * B))
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate -> near (μ (W * B)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1
  (map G2 (μ C) ∘ δ T G2 (T C) ∘ (map T g ∘ μ (W * B)))
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (natural (ϕ := join)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1
  (map G2 (μ C) ∘ δ T G2 (T C)
   ∘ (μ (G2 (T C)) ∘ map (T ∘ T) g))
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1
  (map G2 (μ C) ∘ δ T G2 (T C) ∘ μ (G2 (T C))
   ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        bring (δ T G2 (T C)) and (μ (G2 (T C))) together.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1
  (map G2 (μ C) ∘ (δ T G2 (T C) ∘ μ (G2 (T C)))
   ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite trvmon_join.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1
  (map G2 (μ C)
   ∘ (map G2 (μ (T C)) ∘ δ T G2 (T (T C))
      ∘ map T (δ T G2 (T C))) ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        do 2 reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1
  (map G2 (μ C) ∘ map G2 (μ (T C)) ∘ δ T G2 (T (T C))
   ∘ map T (δ T G2 (T C)) ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (fun_map_map (F := G2)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1
  (map G2 (μ C ∘ μ (T C)) ∘ δ T G2 (T (T C))
   ∘ map T (δ T G2 (T C)) ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        (* Change map-join-then-join into join-then-join *)
        rewrite (mon_join_join (T := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1
  (map G2 (μ C ∘ map T (μ C)) ∘ δ T G2 (T (T C))
   ∘ map T (δ T G2 (T C)) ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        (* Now rearrange to match RHS *)
        rewrite <- (fun_map_map (F := G2)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1
  (map G2 (μ C) ∘ map G2 (map T (μ C))
   ∘ δ T G2 (T (T C)) ∘ map T (δ T G2 (T C))
   ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        change (map G2 (μ C) ∘ map G2 (map T (μ C)) ∘ δ T G2 (T (T C)) ∘ map T (δ T G2 (T C)) ∘ map (T ∘ T) g)
          with (map G2 (μ C) ∘ (map G2 (map T (μ C)) ∘ δ T G2 (T (T C)) ∘ map T (δ T G2 (T C)) ∘ map (T ∘ T) g)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1
  (map G2 (μ C)
   ∘ (map G2 (map T (μ C)) ∘ δ T G2 (T (T C))
      ∘ map T (δ T G2 (T C)) ∘ map (T ∘ T) g))
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite <- (fun_map_map (F := G1)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map G1 (map G2 (μ C))
∘ map G1
    (map G2 (map T (μ C)) ∘ δ T G2 (T (T C))
     ∘ map T (δ T G2 (T C)) ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        change (map G1 (map G2 ?f)) with (map (G1 ∘ G2) f).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (map G2 (map T (μ C)) ∘ δ T G2 (T (T C))
     ∘ map T (δ T G2 (T C)) ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        change (map G2 (map T ?mu)) with (map (G2 ∘ T) mu).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (map (G2 ∘ T) (μ C) ∘ δ T G2 (T (T C))
     ∘ map T (δ T G2 (T C)) ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (natural (ϕ := dist T G2)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (δ T G2 (T C) ∘ map (T ○ G2) (μ C)
     ∘ map T (δ T G2 (T C)) ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        change (map (T ○ G2) ?f) with (map T (map G2 f)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (δ T G2 (T C) ∘ map T (map G2 (μ C))
     ∘ map T (δ T G2 (T C)) ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate -> near (map T (δ T G2 (T C))).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (δ T G2 (T C)
     ∘ (map T (map G2 (μ C)) ∘ map T (δ T G2 (T C)))
     ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (fun_map_map (F := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (δ T G2 (T C)
     ∘ map T (map G2 (μ C) ∘ δ T G2 (T C))
     ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map (T ○ prod W) (dec T B)) ∘ δ T G1 (W * T B)
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        change (map (T ○ prod W) ?f) with (map T (map (W ×) f)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (δ T G2 (T C)
     ∘ map T (map G2 (μ C) ∘ δ T G2 (T C))
     ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ)
     ∘ map T (map (prod W) (dec T B)))
∘ δ T G1 (W * T B) ∘ map T (σ) ∘ map (T ∘ prod W) f
∘ map T cojoin ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (fun_map_map (F := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (δ T G2 (T C)
     ∘ map T (map G2 (μ C) ∘ δ T G2 (T C))
     ∘ map (T ∘ T) g)
∘ map G1
    (map T (map T (μ B) ∘ σ ∘ map (prod W) (dec T B)))
∘ δ T G1 (W * T B) ∘ map T (σ) ∘ map (T ∘ prod W) f
∘ map T cojoin ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate -> near (δ T G1 (W * T B)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (δ T G2 (T C)
     ∘ map T (map G2 (μ C) ∘ δ T G2 (T C))
     ∘ map (T ∘ T) g)
∘ (map G1
     (map T (map T (μ B) ∘ σ ∘ map (prod W) (dec T B)))
   ∘ δ T G1 (W * T B)) ∘ map T (σ)
∘ map (T ∘ prod W) f ∘ map T cojoin ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        change (map G1 (map T ?f)) with (map (G1 ○ T) f).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (δ T G2 (T C)
     ∘ map T (map G2 (μ C) ∘ δ T G2 (T C))
     ∘ map (T ∘ T) g)
∘ (map (G1 ○ T)
     (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))
   ∘ δ T G1 (W * T B)) ∘ map T (σ)
∘ map (T ∘ prod W) f ∘ map T cojoin ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (natural (ϕ := dist T G1) (A := (W * T B)) (B := (T (W * B)))).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (δ T G2 (T C)
     ∘ map T (map G2 (μ C) ∘ δ T G2 (T C))
     ∘ map (T ∘ T) g)
∘ (δ T G1 (T (W * B))
   ∘ map (T ○ G1)
       (map T (μ B) ∘ σ ∘ map (prod W) (dec T B)))
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (δ T G2 (T C)
     ∘ map T (map G2 (μ C) ∘ δ T G2 (T C))
     ∘ map (T ∘ T) g) ∘ δ T G1 (T (W * B))
∘ map (T ○ G1)
    (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        change (map (T ∘ T) ?g) with (map T (map T g)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (δ T G2 (T C)
     ∘ map T (map G2 (μ C) ∘ δ T G2 (T C))
     ∘ map T (map T g)) ∘ δ T G1 (T (W * B))
∘ map (T ○ G1)
    (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate -> near (map T (map T g)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (δ T G2 (T C)
     ∘ (map T (map G2 (μ C) ∘ δ T G2 (T C))
        ∘ map T (map T g))) ∘ δ T G1 (T (W * B))
∘ map (T ○ G1)
    (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (fun_map_map (F := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ map G1
    (δ T G2 (T C)
     ∘ map T (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g))
∘ δ T G1 (T (W * B))
∘ map (T ○ G1)
    (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite <- (fun_map_map (F := G1)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C)
∘ (map G1 (δ T G2 (T C))
   ∘ map G1
       (map T (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)))
∘ δ T G1 (T (W * B))
∘ map (T ○ G1)
    (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ map G1
    (map T (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g))
∘ δ T G1 (T (W * B))
∘ map (T ○ G1)
    (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        change (map G1 (map T ?f)) with (map (G1 ○ T) f).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ map (G1 ○ T) (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ δ T G1 (T (W * B))
∘ map (T ○ G1)
    (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate -> near (δ T G1 (T (W * B))).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ (map (G1 ○ T)
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
   ∘ δ T G1 (T (W * B)))
∘ map (T ○ G1)
    (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (natural (ϕ := δ T G1)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ (δ T G1 (G2 (T C))
   ∘ map (T ○ G1)
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g))
∘ map (T ○ G1)
    (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map (T ○ G1) (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
∘ map (T ○ G1)
    (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate -> near (map (T ○ G1) (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ (map (T ○ G1)
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g)
   ∘ map (T ○ G1)
       (map T (μ B) ∘ σ ∘ map (prod W) (dec T B)))
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (fun_map_map (F := T ○ G1)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map (T ○ G1)
    (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g
     ∘ (map T (μ B) ∘ σ ∘ map (prod W) (dec T B)))
∘ map T (σ) ∘ map (T ∘ prod W) f ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind 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
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map (T ○ G1)
    (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g
     ∘ (map T (μ B) ∘ σ ∘ map (prod W) (dec T B)))
∘ map T (σ) ∘ map T (map (prod W) f) ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        change (map (T ○ G1) ?f) with (map T (map G1 f)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g
        ∘ (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))))
∘ map T (σ) ∘ map T (map (prod W) f) ∘ map T cojoin
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate -> near (map T cojoin).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g
        ∘ (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))))
∘ map T (σ) ∘ (map T (map (prod W) f) ∘ map T cojoin)
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (fun_map_map (F := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g
        ∘ (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))))
∘ map T (σ) ∘ map T (map (prod W) f ∘ cojoin)
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate -> near (map T (map (prod W) f ∘ cojoin)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g
        ∘ (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))))
∘ (map T (σ) ∘ map T (map (prod W) f ∘ cojoin))
∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (fun_map_map (F := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g
        ∘ (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))))
∘ map T (σ ∘ (map (prod W) f ∘ cojoin)) ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        reassociate -> near (map T (σ ∘ (map (prod W) f ∘ cojoin))).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ (map T
     (map G1
        (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g
         ∘ (map T (μ B) ∘ σ ∘ map (prod W) (dec T B))))
   ∘ map T (σ ∘ (map (prod W) f ∘ cojoin))) ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        rewrite (fun_map_map (F := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g
        ∘ (map T (μ B) ∘ σ ∘ map (prod W) (dec T B)))
     ∘ (σ ∘ (map (prod W) f ∘ cojoin))) ∘ dec T A =
binddt
  (map G1
     (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
      ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
        (* ********** *)
        unfold binddt, kc7, binddt.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g
        ∘ (map T (μ B) ∘ σ ∘ map (prod W) (dec T B)))
     ∘ (σ ∘ (map (prod W) f ∘ cojoin))) ∘ dec T A =
map (G1 ∘ G2) (μ C) ∘ δ T (G1 ∘ G2) (T C)
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
        ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
∘ dec T A
        rewrite dist_linear.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g
        ∘ (map T (μ B) ∘ σ ∘ map (prod W) (dec T B)))
     ∘ (σ ∘ (map (prod W) f ∘ cojoin))) ∘ dec T A =
map (G1 ∘ G2) (μ C)
∘ (map G1 (δ T G2 (T C)) ∘ δ T G1 (G2 (T C)))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
        ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
∘ dec T A
        do 4 reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T g
        ∘ map T (μ B) ∘ σ ∘ map (prod W) (dec T B))
     ∘ σ ∘ map (prod W) f ∘ cojoin) ∘ dec T A =
map (G1 ∘ G2) (μ C)
∘ (map G1 (δ T G2 (T C)) ∘ δ T G1 (G2 (T C)))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
        ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
∘ dec T A
        reassociate -> near (map T (μ B)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C)
        ∘ (map T g ∘ map T (μ B)) ∘ σ
        ∘ map (prod W) (dec T B)) ∘ σ ∘ map (prod W) f
     ∘ cojoin) ∘ dec T A =
map (G1 ∘ G2) (μ C)
∘ (map G1 (δ T G2 (T C)) ∘ δ T G1 (G2 (T C)))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
        ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
∘ dec T A
        rewrite (fun_map_map (F := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
        ∘ σ ∘ map (prod W) (dec T B)) ∘ σ
     ∘ map (prod W) f ∘ cojoin) ∘ dec T A =
map (G1 ∘ G2) (μ C)
∘ (map G1 (δ T G2 (T C)) ∘ δ T G1 (G2 (T C)))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
        ∘ σ ∘ map (prod W) (dec T B)) ∘ σ ∘ cobind f)
∘ dec T A
        replace (cobind f) with (map (prod W) f ∘ cojoin).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (G1 ∘ G2) (μ C) ∘ map G1 (δ T G2 (T C))
∘ δ T G1 (G2 (T C))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
        ∘ σ ∘ map (prod W) (dec T B)) ∘ σ
     ∘ map (prod W) f ∘ cojoin) ∘ dec T A =
map (G1 ∘ G2) (μ C)
∘ (map G1 (δ T G2 (T C)) ∘ δ T G1 (G2 (T C)))
∘ map T
    (map G1
       (map G2 (μ C) ∘ δ T G2 (T C) ∘ map T (g ∘ μ B)
        ∘ σ ∘ map (prod W) (dec T B)) ∘ σ
     ∘ (map (prod W) f ∘ cojoin)) ∘ dec T A
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (prod W) f ∘ cojoin = cobind f
        reflexivity.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
map (prod W) f ∘ cojoin = cobind f
        ext [w a].
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1: Type -> Type
H5: Map G1
H6: Pure G1
H7: Mult G1
Applicative0: Applicative G1
G2: Type -> Type
H8: Map G2
H9: Pure G2
H10: Mult G2
Applicative1: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
H11: Functor G1
H12: Functor G2
w: W
a: A
(map (prod W) f ∘ cojoin) (w, a) = cobind f (w, a)
        reflexivity.
      Qed.

    End binddt_binddt.

    Lemma kdtm_morph_T:
      forall `{ApplicativeMorphism G1 G2 ϕ},
      forall (A B: Type) (f: W * A -> G1 (T B)),
        ϕ (T B) ∘ binddt (G := G1) f = binddt (G := G2) (ϕ (T B) ∘ f).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
forall (G1 G2 : Type -> Type) (H5 : Map G1)
  (H6 : Mult G1) (H7 : Pure G1) (H8 : Map G2)
  (H9 : Mult G2) (H10 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : W * A -> G1 (T B)),
ϕ (T B) ∘ binddt f = binddt (ϕ (T B) ∘ f)
    Proof.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
forall (G1 G2 : Type -> Type) (H5 : Map G1)
  (H6 : Mult G1) (H7 : Pure G1) (H8 : Map G2)
  (H9 : Mult G2) (H10 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : W * A -> G1 (T B)),
ϕ (T B) ∘ binddt f = binddt (ϕ (T B) ∘ f)
      introv morph.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
forall (A B : Type) (f : W * A -> G1 (T B)),
ϕ (T B) ∘ binddt f = binddt (ϕ (T B) ∘ f) intros.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
ϕ (T B) ∘ binddt f = binddt (ϕ (T B) ∘ f)
      unfold_ops @Binddt_Categorical.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
ϕ (T B) ∘ (map (μ) ∘ δ T G1 ∘ map f ∘ dec T) =
map (μ) ∘ δ T G2 ∘ map (ϕ (T B) ∘ f) ∘ dec T
      do 3 reassociate <- on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
ϕ (T B) ∘ map (μ) ∘ δ T G1 ∘ map f ∘ dec T =
map (μ) ∘ δ T G2 ∘ map (ϕ (T B) ∘ f) ∘ dec T
      fequal.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
ϕ (T B) ∘ map (μ) ∘ δ T G1 ∘ map f =
map (μ) ∘ δ T G2 ∘ map (ϕ (T B) ∘ f)
      unfold compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
(fun a : T (W * A) =>
 ϕ (T B) (map (μ) (δ T G1 (map f a)))) =
(fun a : T (W * A) =>
 map (μ) (δ T G2 (map (ϕ (T B) ○ f) a))) ext t.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
t: T (W * A)
ϕ (T B) (map (μ) (δ T G1 (map f t))) =
map (μ) (δ T G2 (map (ϕ (T B) ○ f) t))
      rewrite appmor_natural.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
t: T (W * A)
map (μ) (ϕ (T (T B)) (δ T G1 (map f t))) =
map (μ) (δ T G2 (map (ϕ (T B) ○ f) t))
      fequal.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
t: T (W * A)
ϕ (T (T B)) (δ T G1 (map f t)) =
δ T G2 (map (ϕ (T B) ○ f) t)
      compose near (map f t).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
t: T (W * A)
(ϕ (T (T B)) ∘ δ T G1) (map f t) =
δ T G2 (map (ϕ (T B) ○ f) t)
      rewrite <- (dist_morph (F := T)).
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
t: T (W * A)
(δ T G2 ∘ map (ϕ (T B))) (map f t) =
δ T G2 (map (ϕ (T B) ○ f) t)
      unfold compose.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
t: T (W * A)
δ T G2 (map (ϕ (T B)) (map f t)) =
δ T G2 (map (ϕ (T B) ○ f) t) compose near t on left.
W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: ApplicativeDist T
H4: Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad
  W T
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
t: T (W * A)
δ T G2 ((map (ϕ (T B)) ∘ map f) t) =
δ T G2 (map (ϕ (T B) ○ f) t)
      now rewrite (fun_map_map (F := T)).
    Qed.

    (** ** Typeclass Instances *)
    (******************************************************************)
    #[export] Instance: Kleisli.DecoratedTraversableMonad.DecoratedTraversableRightPreModule W T T :=
      {|
        kdtm_binddt1 := @kdtm_binddt1_T;
        kdtm_binddt2 := @kdtm_binddt2_T;
        kdtm_morph := @kdtm_morph_T;
      |}.

    #[export] Instance: Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad W T :=
      {| kdtm_binddt0 := @kdtm_binddt0_T;
         kdtm_monoid := dmon_monoid;
      |}.

  End with_monad.

End DerivedInstances.