From Tealeaves Require Export
  Classes.Kleisli.DecoratedTraversableMonad
  Classes.Monoid
  Functors.Writer.

Import Applicative.Notations.
Import Monoid.Notations.
Import Product.Notations.

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

Section dtm_to_dtm.

  Context
    {T: Type -> Type}
    `{DecoratedTraversableMonad W1 T}
    `{Monoid W2}
    (ϕ: W1 -> W2)
    `{! Monoid_Morphism W1 W2 ϕ}.

  #[export] Instance Binddt_Morphism: Binddt W2 T T :=
    fun G Gmap Gpure Gmult V1 V2 σ =>
      binddt (G := G) (T := T) (σ ∘ map_fst ϕ).

  #[export] Instance DTM_of_DTM: DecoratedTraversableMonad W2 T.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
DecoratedTraversableMonad W2 T
  Proof.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
DecoratedTraversableMonad W2 T
    constructor.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
Monoid W2
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
forall (G : Type -> Type) 
  (Map_G : Map G) (Pure_G : Pure G) 
  (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : W2 * A -> G (T B)),
binddt f ∘ ret = f ∘ ret
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
DecoratedTraversableRightPreModule W2 T T
    -
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
Monoid W2 typeclasses eauto.
    -
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : W2 * A -> G (T B)),
binddt f ∘ ret = f ∘ ret intros.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A, B: Type
f: W2 * A -> G (T B)
binddt f ∘ ret = f ∘ ret
      unfold_ops @Binddt_Morphism.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A, B: Type
f: W2 * A -> G (T B)
binddt (f ∘ map_fst ϕ) ∘ ret = f ∘ ret
      rewrite kdtm_binddt0.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A, B: Type
f: W2 * A -> G (T B)
f ∘ map_fst ϕ ∘ ret = f ∘ ret
      reassociate -> on left.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A, B: Type
f: W2 * A -> G (T B)
f ∘ (map_fst ϕ ∘ ret) = f ∘ ret
      fequal.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A, B: Type
f: W2 * A -> G (T B)
map_fst ϕ ∘ ret = ret
      unfold_ops @Return_Writer.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A, B: Type
f: W2 * A -> G (T B)
map_fst ϕ ∘ (fun a : A => (Ƶ, a)) =
(fun a : A => (Ƶ, a))
      unfold map_fst, compose.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A, B: Type
f: W2 * A -> G (T B)
map_tensor ϕ id ○ pair Ƶ = (fun a : A => (Ƶ, a))
      ext a.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A, B: Type
f: W2 * A -> G (T B)
a: A
map_tensor ϕ id (Ƶ, a) = (Ƶ, a)
      cbn.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A, B: Type
f: W2 * A -> G (T B)
a: A
(ϕ Ƶ, id a) = (Ƶ, a)
      fequal.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A, B: Type
f: W2 * A -> G (T B)
a: A
ϕ Ƶ = Ƶ
      apply monmor_unit.
    -
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
DecoratedTraversableRightPreModule W2 T T constructor.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
forall A : Type, binddt (ret ∘ extract) = id
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
forall (G1 : Type -> Type) 
  (Map_G : Map G1) (Pure_G : Pure G1)
  (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) 
  (Map_G0 : Map G2) (Pure_G0 : Pure G2)
  (Mult_G0 : Mult G2),
Applicative G2 ->
forall (B C : Type) (g : W2 * B -> G2 (T C))
  (A : Type) (f : W2 * A -> G1 (T B)),
map (binddt g) ∘ binddt f = binddt (kc7 G1 G2 g f)
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
forall (G1 G2 : Type -> Type) 
  (H : Map G1) (H0 : Mult G1) 
  (H1 : Pure G1) (H2 : Map G2) 
  (H3 : Mult G2) (H4 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : W2 * A -> G1 (T B)),
ϕ (T B) ∘ binddt f = binddt (ϕ (T B) ∘ f)
      +
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
forall A : Type, binddt (ret ∘ extract) = id intros.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
A: Type
binddt (ret ∘ extract) = id
        unfold_ops @Binddt_Morphism.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
A: Type
binddt (ret ∘ extract ∘ map_fst ϕ) = id
        reassociate -> on left.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
A: Type
binddt (ret ∘ (extract ∘ map_fst ϕ)) = id
        assert (Heq: extract (A := A) ∘ map_fst ϕ = extract (W := prod W1)).
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
A: Type
extract ∘ map_fst ϕ = extract
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
A: Type
Heq: extract ∘ map_fst ϕ = extract
binddt (ret ∘ (extract ∘ map_fst ϕ)) = id
        now ext [w a].
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
A: Type
Heq: extract ∘ map_fst ϕ = extract
binddt (ret ∘ (extract ∘ map_fst ϕ)) = id
        rewrite Heq.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
A: Type
Heq: extract ∘ map_fst ϕ = extract
binddt (ret ∘ extract) = id
        apply kdtm_binddt1.
      +
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall (B C : Type) (g : W2 * B -> G2 (T C))
  (A : Type) (f : W2 * A -> G1 (T B)),
map (binddt g) ∘ binddt f = binddt (kc7 G1 G2 g f) intros.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
map (binddt g) ∘ binddt f = binddt (kc7 G1 G2 g f)
        unfold_ops @Binddt_Morphism.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
map (binddt (g ∘ map_fst ϕ)) ∘ binddt (f ∘ map_fst ϕ) =
binddt (kc7 G1 G2 g f ∘ map_fst ϕ)
        rewrite kdtm_binddt2.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
binddt (kc7 G1 G2 (g ∘ map_fst ϕ) (f ∘ map_fst ϕ)) =
binddt (kc7 G1 G2 g f ∘ map_fst ϕ)
        fequal.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
kc7 G1 G2 (g ∘ map_fst ϕ) (f ∘ map_fst ϕ) =
kc7 G1 G2 g f ∘ map_fst ϕ
        unfold kc7.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
(fun '(w, a) =>
 map (binddt ((g ∘ map_fst ϕ) ⦿ w))
   ((f ∘ map_fst ϕ) (w, a))) =
(fun '(w, a) => map (binddt (g ⦿ w)) (f (w, a)))
∘ map_fst ϕ
        ext [w a].
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
w: W1
a: A
map (binddt ((g ∘ map_fst ϕ) ⦿ w))
  ((f ∘ map_fst ϕ) (w, a)) =
((fun '(w, a) => map (binddt (g ⦿ w)) (f (w, a)))
 ∘ map_fst ϕ) (w, a)
        unfold compose.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
w: W1
a: A
map (binddt ((g ○ map_fst ϕ) ⦿ w))
  (f (map_fst ϕ (w, a))) =
(let
 '(w, a) := map_fst ϕ (w, a) in
  map (binddt (g ⦿ w)) (f (w, a))) cbn.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
w: W1
a: A
map (binddt ((g ○ map_fst ϕ) ⦿ w)) (f (ϕ w, id a)) =
map (binddt (g ⦿ ϕ w)) (f (ϕ w, id a))
        fequal.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
w: W1
a: A
binddt ((g ○ map_fst ϕ) ⦿ w) = binddt (g ⦿ ϕ w)
        fequal.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
w: W1
a: A
binddt ((g ○ map_fst ϕ) ⦿ w) = binddt (g ⦿ ϕ w)
        unfold binddt at 2.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
w: W1
a: A
binddt ((g ○ map_fst ϕ) ⦿ w) =
binddt (g ⦿ ϕ w ○ map_fst ϕ)
        fequal.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
w: W1
a: A
(g ○ map_fst ϕ) ⦿ w = g ⦿ ϕ w ○ map_fst ϕ
        unfold preincr, compose, incr.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
w: W1
a: A
(fun a : W1 * B =>
 g (map_fst ϕ (let '(w1, a0) := a in (w ● w1, a0)))) =
(fun a : W1 * B =>
 g (let '(w1, a0) := map_fst ϕ a in (ϕ w ● w1, a0)))
        ext [w2 b].
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
w: W1
a: A
w2: W1
b: B
g (map_fst ϕ (w ● w2, b)) =
g (let '(w1, a) := map_fst ϕ (w2, b) in (ϕ w ● w1, a))
        fequal.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
w: W1
a: A
w2: W1
b: B
map_fst ϕ (w ● w2, b) =
(let '(w1, a) := map_fst ϕ (w2, b) in (ϕ w ● w1, a))
        cbn.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
w: W1
a: A
w2: W1
b: B
(ϕ (w ● w2), id b) = (ϕ w ● ϕ w2, id b)
        fequal.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
B, C: Type
g: W2 * B -> G2 (T C)
A: Type
f: W2 * A -> G1 (T B)
w: W1
a: A
w2: W1
b: B
ϕ (w ● w2) = ϕ w ● ϕ w2
        apply monmor_op.
      +
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
forall (G1 G2 : Type -> Type) (H : Map G1)
  (H0 : Mult G1) (H1 : Pure G1) (H2 : Map G2)
  (H3 : Mult G2) (H4 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : W2 * A -> G1 (T B)),
ϕ (T B) ∘ binddt f = binddt (ϕ (T B) ∘ f) intros.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ0: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ0
A, B: Type
f: W2 * A -> G1 (T B)
ϕ0 (T B) ∘ binddt f = binddt (ϕ0 (T B) ∘ f)
        unfold_ops @Binddt_Morphism.
T: Type -> Type
W1: Type
op: Monoid_op W1
unit0: Monoid_unit W1
Return_inst: Return T
Bindd_T_inst: Binddt W1 T T
H: DecoratedTraversableMonad W1 T
W2: Type
op0: Monoid_op W2
unit1: Monoid_unit W2
H0: Monoid W2
ϕ: W1 -> W2
Monoid_Morphism0: Monoid_Morphism W1 W2 ϕ
G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ0: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ0
A, B: Type
f: W2 * A -> G1 (T B)
ϕ0 (T B) ∘ binddt (f ∘ map_fst ϕ) =
binddt (ϕ0 (T B) ∘ f ∘ map_fst ϕ)
        apply kdtm_morph; auto.
  Qed.

End dtm_to_dtm.