From Tealeaves Require Import
  Classes.Kleisli.DecoratedTraversableFunctor
  Classes.Kleisli.DecoratedTraversableMonad.

#[local] Generalizable Variables F T U W.

Import Monoid.Notations.
Import Product.Notations.
Import DecoratedTraversableFunctor.Notations.

(** * Composition of Two <<DTF>> Instances *)
(******************************************************************************)

(** ** Composition of <<mapdt>> Operations *)
(******************************************************************************)
#[export] Instance Mapdt_compose `{op: Monoid_op W}
  `{Mapdt W F1} `{Mapdt W F2}: Mapdt W (F1 ○ F2) :=
  fun G map pure mult A B f =>
    mapdt (T := F1) (G := G) (fun '(w1, t) => mapdt (T := F2) (f ⦿ w1) t).

(** ** <<DecoratedTraversableFunctor>> Laws *)
(******************************************************************************)
Section compose_functors.

  Context
    `{Monoid W}.

  Context
    `{Mapdt W F1} `{Mapdt W F2}
    `{! DecoratedTraversableFunctor W F1}
    `{! DecoratedTraversableFunctor W F2}.

  Lemma kdtf_comp_mapdt1 : forall A : Type,
      mapdt (T := F1 ○ F2) (@extract (W ×) _ A) = id.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
forall A : Type, mapdt extract = id
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
forall A : Type, mapdt extract = id
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
A: Type
mapdt extract = id
    unfold_ops @Mapdt_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
A: Type
mapdt (fun '(w1, t) => mapdt (extract ⦿ w1) t) = id
    rewrite <- kdtf_mapdt1.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
A: Type
mapdt (fun '(w1, t) => mapdt (extract ⦿ w1) t) =
mapdt extract
    fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
A: Type
(fun '(w1, t) => mapdt (extract ⦿ w1) t) = extract
    ext [w t].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
A: Type
w: W
t: F2 A
mapdt (extract ⦿ w) t = extract (w, t)
    rewrite extract_preincr.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
A: Type
w: W
t: F2 A
mapdt extract t = extract (w, t)
    rewrite kdtf_mapdt1.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
A: Type
w: W
t: F2 A
id t = extract (w, t)
    reflexivity.
  Qed.

  Lemma kdtf_comp_mapdt2 :
    forall (G1 : Type -> Type) (H1 : Map G1)
      (H2 : Pure G1) (H3 : Mult G1),
      Applicative G1 ->
      forall (G2 : Type -> Type) (H5 : Map G2)
        (H6 : Pure G2) (H7 : Mult G2),
        Applicative G2 ->
        forall (A B C : Type) (g : W * B -> G2 C) (f : W * A -> G1 B),
          map (F := G1) (mapdt (G := G2) (T := F1 ○ F2) g)
              ∘ mapdt (G := G1) (T := F1 ○ F2) f =
            mapdt (G := G1 ∘ G2) (T := F1 ○ F2) (kc3 g f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
forall (G1 : Type -> Type) (H2 : Map G1)
  (H3 : Pure G1) (H4 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H5 : Map G2)
  (H6 : Pure G2) (H7 : Mult G2),
Applicative G2 ->
forall (A B C : Type) (g : W * B -> G2 C)
  (f : W * A -> G1 B),
map (mapdt g) ∘ mapdt f = mapdt (g ⋆3 f)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
forall (G1 : Type -> Type) (H2 : Map G1)
  (H3 : Pure G1) (H4 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H5 : Map G2)
  (H6 : Pure G2) (H7 : Mult G2),
Applicative G2 ->
forall (A B C : Type) (g : W * B -> G2 C)
  (f : W * A -> G1 B),
map (mapdt g) ∘ mapdt f = mapdt (g ⋆3 f)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
map (mapdt g) ∘ mapdt f = mapdt (g ⋆3 f)
    unfold_ops @Mapdt_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
map (mapdt (fun '(w1, t) => mapdt (g ⦿ w1) t))
∘ mapdt (fun '(w1, t) => mapdt (f ⦿ w1) t) =
mapdt (fun '(w1, t) => mapdt ((g ⋆3 f) ⦿ w1) t)
    rewrite (kdtf_mapdt2
               (A := F2 A) (B := F2 B) (C := F2 C)
               (E := W) (G1 := G1) (G2 := G2) (T := F1)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
mapdt
  ((fun '(w1, t) => mapdt (g ⦿ w1) t)
   ⋆3 (fun '(w1, t) => mapdt (f ⦿ w1) t)) =
mapdt (fun '(w1, t) => mapdt ((g ⋆3 f) ⦿ w1) t)
    fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
(fun '(w1, t) => mapdt (g ⦿ w1) t)
⋆3 (fun '(w1, t) => mapdt (f ⦿ w1) t) =
(fun '(w1, t) => mapdt ((g ⋆3 f) ⦿ w1) t)
    ext [w1 t].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
w1: W
t: F2 A
((fun '(w1, t) => mapdt (g ⦿ w1) t)
 ⋆3 (fun '(w1, t) => mapdt (f ⦿ w1) t)) (w1, t) =
mapdt ((g ⋆3 f) ⦿ w1) t
    rewrite (kc3_preincr _ _ _ f g w1).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
w1: W
t: F2 A
((fun '(w1, t) => mapdt (g ⦿ w1) t)
 ⋆3 (fun '(w1, t) => mapdt (f ⦿ w1) t)) (w1, t) =
mapdt (g ⦿ w1 ⋆3 f ⦿ w1) t
    rewrite <- (kdtf_mapdt2
               (A := A) (B := B) (C := C)
               (E := W) (G1 := G1) (G2 := G2) (T := F2)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
w1: W
t: F2 A
((fun '(w1, t) => mapdt (g ⦿ w1) t)
 ⋆3 (fun '(w1, t) => mapdt (f ⦿ w1) t)) (w1, t) =
(map (mapdt (g ⦿ w1)) ∘ mapdt (f ⦿ w1)) t
    unfold kc3, compose; cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
w1: W
t: F2 A
map (fun '(w1, t) => mapdt (g ⦿ w1) t)
  (map (pair w1) (mapdt (f ⦿ w1) t)) =
map (mapdt (g ⦿ w1)) (mapdt (f ⦿ w1) t)
    compose near (mapdt (f ⦿ w1) t) on left.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
w1: W
t: F2 A
(map (fun '(w1, t) => mapdt (g ⦿ w1) t)
 ∘ map (pair w1)) (mapdt (f ⦿ w1) t) =
map (mapdt (g ⦿ w1)) (mapdt (f ⦿ w1) t)
    assert (Functor G1).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
w1: W
t: F2 A
Functor G1
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
w1: W
t: F2 A
H10: Functor G1
(map (fun '(w1, t) => mapdt (g ⦿ w1) t)
 ∘ map (pair w1)) (mapdt (f ⦿ w1) t) =
map (mapdt (g ⦿ w1)) (mapdt (f ⦿ w1) t) {
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
w1: W
t: F2 A
Functor G1 now inversion H5. }
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
w1: W
t: F2 A
H10: Functor G1
(map (fun '(w1, t) => mapdt (g ⦿ w1) t)
 ∘ map (pair w1)) (mapdt (f ⦿ w1) t) =
map (mapdt (g ⦿ w1)) (mapdt (f ⦿ w1) t)
    rewrite (fun_map_map (F := G1)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H5: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H9: Applicative G2
A, B, C: Type
g: W * B -> G2 C
f: W * A -> G1 B
w1: W
t: F2 A
H10: Functor G1
map ((fun '(w1, t) => mapdt (g ⦿ w1) t) ∘ pair w1)
  (mapdt (f ⦿ w1) t) =
map (mapdt (g ⦿ w1)) (mapdt (f ⦿ w1) t)
    reflexivity.
  Qed.

  Lemma kdtf_comp_morph :
    forall (G1 G2 : Type -> Type) (H1 : Map G1)
      (H2 : Mult G1) (H3 : Pure G1) (H4 : Map G2)
      (H5 : Mult G2) (H6 : Pure G2)
      (ϕ : forall A : Type, G1 A -> G2 A),
      ApplicativeMorphism G1 G2 ϕ ->
      forall (A B : Type) (f : W * A -> G1 B),
        ϕ (F1 (F2 B)) ∘ (mapdt (T := F1 ○ F2) (G := G1) f)
          = mapdt (ϕ B ∘ f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
forall (G1 G2 : Type -> Type) (H2 : Map G1)
  (H3 : Mult G1) (H4 : Pure G1) (H5 : Map G2)
  (H6 : Mult G2) (H7 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : W * A -> G1 B),
ϕ (F1 (F2 B)) ∘ mapdt f = mapdt (ϕ B ∘ f)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
forall (G1 G2 : Type -> Type) (H2 : Map G1)
  (H3 : Mult G1) (H4 : Pure G1) (H5 : Map G2)
  (H6 : Mult G2) (H7 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : W * A -> G1 B),
ϕ (F1 (F2 B)) ∘ mapdt f = mapdt (ϕ B ∘ f)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H8: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 B
ϕ (F1 (F2 B)) ∘ mapdt f = mapdt (ϕ B ∘ f)
    unfold_ops @Mapdt_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H8: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 B
ϕ (F1 (F2 B))
∘ mapdt (fun '(w1, t) => mapdt (f ⦿ w1) t) =
mapdt (fun '(w1, t) => mapdt ((ϕ B ∘ f) ⦿ w1) t)
    rewrite kdtf_morph.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H8: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 B
mapdt (ϕ (F2 B) ∘ (fun '(w1, t) => mapdt (f ⦿ w1) t)) =
mapdt (fun '(w1, t) => mapdt ((ϕ B ∘ f) ⦿ w1) t)
    fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H8: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 B
ϕ (F2 B) ∘ (fun '(w1, t) => mapdt (f ⦿ w1) t) =
(fun '(w1, t) => mapdt ((ϕ B ∘ f) ⦿ w1) t)
    ext [w t].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H8: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 B
w: W
t: F2 A
(ϕ (F2 B) ∘ (fun '(w1, t) => mapdt (f ⦿ w1) t)) (w, t) =
mapdt ((ϕ B ∘ f) ⦿ w) t
    unfold compose; cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H8: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 B
w: W
t: F2 A
ϕ (F2 B) (mapdt (f ⦿ w) t) = mapdt ((ϕ B ○ f) ⦿ w) t
    compose near t on left.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H8: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 B
w: W
t: F2 A
(ϕ (F2 B) ∘ mapdt (f ⦿ w)) t = mapdt ((ϕ B ○ f) ⦿ w) t
    rewrite kdtf_morph.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F1: Type -> Type
H0: Mapdt W F1
F2: Type -> Type
H1: Mapdt W F2
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F1
DecoratedTraversableFunctor1: DecoratedTraversableFunctor
  W F2
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H8: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 B
w: W
t: F2 A
mapdt (ϕ B ∘ f ⦿ w) t = mapdt ((ϕ B ○ f) ⦿ w) t
    reflexivity.
  Qed.

  (** ** <<DecoratedTraversableFunctor>> Instance *)
  (******************************************************************************)
  #[export] Instance DecoratedTraversableFunctor_compose:
    DecoratedTraversableFunctor W (F1 ○ F2) :=
    {| kdtf_mapdt1 := kdtf_comp_mapdt1;
      kdtf_mapdt2 := kdtf_comp_mapdt2;
      kdtf_morph := kdtf_comp_morph;
    |}.

End compose_functors.

(** * Composition of a <<DTF>> with a <<DTM>> Right Module *)
(******************************************************************************)

(** ** Composition of <<mapdt>> with <<binddt>> *)
(******************************************************************************)
#[export] Instance Mapdt_Binddt_compose
 `{op: Monoid_op W}
 `{Mapdt_F: Mapdt W F}
 `{Binddt_U: Binddt W T U}:
  Binddt W T (F ∘ U) :=
  fun G map pure mult A B f =>
    mapdt (T := F) (G := G)
      (fun '(w1, t) => binddt (U := U) (f ⦿ w1) t).

(** ** <<DecoratedTraversableRightModule>> Laws *)
(******************************************************************************)
Section compose_functor_module.

  Context
    `{Monoid W}.

  Context
    `{Mapdt_WF: Mapdt W F}
    `{Return_T: Return T}
    `{Binddt_WTU: Binddt W T U}
    `{Binddt_WTT: Binddt W T T}
    `{! DecoratedTraversableFunctor W F}
    `{! DecoratedTraversableRightPreModule W T U}.

  Lemma kdtm_binddt1_compose :
    forall A : Type,
      binddt (T := T) (U := F ∘ U) (ret (T := T) ∘ extract) = @id (F (U A)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
forall A : Type, binddt (ret ∘ extract) = id
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
forall A : Type, binddt (ret ∘ extract) = id
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
A: Type
binddt (ret ∘ extract) = id
    unfold_ops @Mapdt_Binddt_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
A: Type
mapdt
  (fun '(w1, t) => binddt ((ret ∘ extract) ⦿ w1) t) =
id
    assert (cut:
        (fun '(w1, t) =>
           binddt (G := fun A => A) (A := A) (B := A)
             (U := U) ((ret (T := T) ∘ extract) ⦿ w1) t)
        = @extract (prod W) _  (U A)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
A: Type
(fun '(w1, t) => binddt ((ret ∘ extract) ⦿ w1) t) =
extract
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
A: Type
cut: (fun '(w1, t) => binddt ((ret ∘ extract) ⦿ w1) t) =
extract
mapdt
  (fun '(w1, t) => binddt ((ret ∘ extract) ⦿ w1) t) =
id
    {
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
A: Type
(fun '(w1, t) => binddt ((ret ∘ extract) ⦿ w1) t) =
extract ext [w t].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
A: Type
w: W
t: U A
binddt ((ret ∘ extract) ⦿ w) t = extract (w, t)
      rewrite extract_preincr2.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
A: Type
w: W
t: U A
binddt (ret ∘ extract) t = extract (w, t)
      rewrite (kdtm_binddt1 (U := U) (T := T)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
A: Type
w: W
t: U A
id t = extract (w, t)
      reflexivity. }
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
A: Type
cut: (fun '(w1, t) => binddt ((ret ∘ extract) ⦿ w1) t) =
extract
mapdt
  (fun '(w1, t) => binddt ((ret ∘ extract) ⦿ w1) t) =
id
    replace
      (fun '((w1, t) : W * U A) =>
         binddt (G := fun A => A) (A := A) (B := A)
           (U := U) ((ret (T := T) ∘ extract) ⦿ w1) t)
      with (@extract (prod W) _  (U A)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
A: Type
cut: (fun '(w1, t) => binddt ((ret ∘ extract) ⦿ w1) t) =
extract
mapdt extract = id
    rewrite kdtf_mapdt1.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
A: Type
cut: (fun '(w1, t) => binddt ((ret ∘ extract) ⦿ w1) t) =
extract
id = id
    reflexivity.
  Qed.

  Lemma kdtm_binddt2_compose :
    forall (G1 : Type -> Type) (H : Map G1)
      (H0 : Pure G1) (H1 : Mult G1),
      Applicative G1 ->
      forall (G2 : Type -> Type) (H3 : Map G2)
        (H4 : Pure G2) (H5 : Mult G2),
        Applicative G2 ->
        forall (B C : Type) (g : W * B -> G2 (T C))
          (A : Type) (f : W * A -> G1 (T B)),
          map (binddt (T := T) (U := F ∘ U) g) ∘
            binddt (T := T) (U := F ∘ U) f =
            binddt (G := G1 ∘ G2) (T := T) (U := F ∘ U) (kc7 G1 G2 g f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
forall (G1 : Type -> Type) (H : Map G1) (H0 : Pure G1)
  (H1 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H3 : Map G2)
  (H4 : Pure G2) (H5 : Mult G2),
Applicative G2 ->
forall (B C : Type) (g : W * B -> G2 (T C)) (A : Type)
  (f : W * A -> G1 (T B)),
map (binddt g) ∘ binddt f = binddt (kc7 G1 G2 g f)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
forall (G1 : Type -> Type) (H : Map G1) (H0 : Pure G1)
  (H1 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H3 : Map G2)
  (H4 : Pure G2) (H5 : Mult G2),
Applicative G2 ->
forall (B C : Type) (g : W * B -> G2 (T C)) (A : Type)
  (f : W * A -> G1 (T B)),
map (binddt g) ∘ binddt f = binddt (kc7 G1 G2 g f)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1: Type -> Type
H0: Map G1
H1: Pure G1
H2: Mult G1
H3: Applicative G1
G2: Type -> Type
H4: Map G2
H5: Pure G2
H6: Mult G2
H7: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
map (binddt g) ∘ binddt f = binddt (kc7 G1 G2 g f)
    unfold_ops @Mapdt_Binddt_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1: Type -> Type
H0: Map G1
H1: Pure G1
H2: Mult G1
H3: Applicative G1
G2: Type -> Type
H4: Map G2
H5: Pure G2
H6: Mult G2
H7: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
map (mapdt (fun '(w1, t) => binddt (g ⦿ w1) t))
∘ mapdt (fun '(w1, t) => binddt (f ⦿ w1) t) =
mapdt (fun '(w1, t) => binddt (kc7 G1 G2 g f ⦿ w1) t)
    change ((F ∘ U) ?X) with (F (U X)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1: Type -> Type
H0: Map G1
H1: Pure G1
H2: Mult G1
H3: Applicative G1
G2: Type -> Type
H4: Map G2
H5: Pure G2
H6: Mult G2
H7: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
map (mapdt (fun '(w1, t) => binddt (g ⦿ w1) t))
∘ mapdt (fun '(w1, t) => binddt (f ⦿ w1) t) =
mapdt (fun '(w1, t) => binddt (kc7 G1 G2 g f ⦿ w1) t)
    rewrite (kdtf_mapdt2 (T := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1: Type -> Type
H0: Map G1
H1: Pure G1
H2: Mult G1
H3: Applicative G1
G2: Type -> Type
H4: Map G2
H5: Pure G2
H6: Mult G2
H7: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
mapdt
  ((fun '(w1, t) => binddt (g ⦿ w1) t)
   ⋆3 (fun '(w1, t) => binddt (f ⦿ w1) t)) =
mapdt (fun '(w1, t) => binddt (kc7 G1 G2 g f ⦿ w1) t)
    fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1: Type -> Type
H0: Map G1
H1: Pure G1
H2: Mult G1
H3: Applicative G1
G2: Type -> Type
H4: Map G2
H5: Pure G2
H6: Mult G2
H7: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
(fun '(w1, t) => binddt (g ⦿ w1) t)
⋆3 (fun '(w1, t) => binddt (f ⦿ w1) t) =
(fun '(w1, t) => binddt (kc7 G1 G2 g f ⦿ w1) t) ext [w t].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1: Type -> Type
H0: Map G1
H1: Pure G1
H2: Mult G1
H3: Applicative G1
G2: Type -> Type
H4: Map G2
H5: Pure G2
H6: Mult G2
H7: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
w: W
t: U A
((fun '(w1, t) => binddt (g ⦿ w1) t)
 ⋆3 (fun '(w1, t) => binddt (f ⦿ w1) t)) (w, t) =
binddt (kc7 G1 G2 g f ⦿ w) t
    change ((G1 ∘ G2) ?X) with (G1 (G2 X)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1: Type -> Type
H0: Map G1
H1: Pure G1
H2: Mult G1
H3: Applicative G1
G2: Type -> Type
H4: Map G2
H5: Pure G2
H6: Mult G2
H7: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
w: W
t: U A
((fun '(w1, t) => binddt (g ⦿ w1) t)
 ⋆3 (fun '(w1, t) => binddt (f ⦿ w1) t)) (w, t) =
binddt (kc7 G1 G2 g f ⦿ w) t
    rewrite <- (kc7_preincr).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1: Type -> Type
H0: Map G1
H1: Pure G1
H2: Mult G1
H3: Applicative G1
G2: Type -> Type
H4: Map G2
H5: Pure G2
H6: Mult G2
H7: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
w: W
t: U A
((fun '(w1, t) => binddt (g ⦿ w1) t)
 ⋆3 (fun '(w1, t) => binddt (f ⦿ w1) t)) (w, t) =
binddt (kc7 G1 G2 (g ⦿ w) (f ⦿ w)) t
    rewrite <- kdtm_binddt2.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1: Type -> Type
H0: Map G1
H1: Pure G1
H2: Mult G1
H3: Applicative G1
G2: Type -> Type
H4: Map G2
H5: Pure G2
H6: Mult G2
H7: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
w: W
t: U A
((fun '(w1, t) => binddt (g ⦿ w1) t)
 ⋆3 (fun '(w1, t) => binddt (f ⦿ w1) t)) (w, t) =
(map (binddt (g ⦿ w)) ∘ binddt (f ⦿ w)) t
    rewrite kc3_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1: Type -> Type
H0: Map G1
H1: Pure G1
H2: Mult G1
H3: Applicative G1
G2: Type -> Type
H4: Map G2
H5: Pure G2
H6: Mult G2
H7: Applicative G2
B, C: Type
g: W * B -> G2 (T C)
A: Type
f: W * A -> G1 (T B)
w: W
t: U A
map ((fun '(w1, t) => binddt (g ⦿ w1) t) ∘ pair w)
  (binddt (f ⦿ w) t) =
(map (binddt (g ⦿ w)) ∘ binddt (f ⦿ w)) t
    reflexivity.
  Qed.

  Lemma kdtm_morph_compose:
    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 : W * A -> G1 (T B)),
        ϕ (F (U B)) ∘ binddt (U := F ∘ U) f =
          binddt (U := F ∘ U) (ϕ (T B) ∘ f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
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 : W * A -> G1 (T B)),
ϕ (F (U B)) ∘ binddt f = binddt (ϕ (T B) ∘ f)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
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 : W * A -> G1 (T B)),
ϕ (F (U B)) ∘ binddt f = binddt (ϕ (T B) ∘ f)
    introv Happl.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
Happl: ApplicativeMorphism G1 G2 ϕ
forall (A B : Type) (f : W * A -> G1 (T B)),
ϕ (F (U B)) ∘ binddt f = binddt (ϕ (T B) ∘ f) intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
Happl: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
ϕ (F (U B)) ∘ binddt f = binddt (ϕ (T B) ∘ f)
    assert (Applicative G1) by now inversion Happl.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
Happl: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
H6: Applicative G1
ϕ (F (U B)) ∘ binddt f = binddt (ϕ (T B) ∘ f)
    assert (Applicative G2) by now inversion Happl.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
Happl: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
H6: Applicative G1
H7: Applicative G2
ϕ (F (U B)) ∘ binddt f = binddt (ϕ (T B) ∘ f)
    unfold_ops @Mapdt_Binddt_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
Happl: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
H6: Applicative G1
H7: Applicative G2
ϕ (F (U B))
∘ mapdt (fun '(w1, t) => binddt (f ⦿ w1) t) =
mapdt (fun '(w1, t) => binddt ((ϕ (T B) ∘ f) ⦿ w1) t)
    rewrite (kdtf_morph (A := U A) (B := U B) (ϕ := ϕ) (T := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
Happl: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
H6: Applicative G1
H7: Applicative G2
mapdt (ϕ (U B) ∘ (fun '(w1, t) => binddt (f ⦿ w1) t)) =
mapdt (fun '(w1, t) => binddt ((ϕ (T B) ∘ f) ⦿ w1) t)
    fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
Happl: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
H6: Applicative G1
H7: Applicative G2
ϕ (U B) ∘ (fun '(w1, t) => binddt (f ⦿ w1) t) =
(fun '(w1, t) => binddt ((ϕ (T B) ∘ f) ⦿ w1) t)
    ext [w' t'].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
Happl: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
H6: Applicative G1
H7: Applicative G2
w': W
t': U A
(ϕ (U B) ∘ (fun '(w1, t) => binddt (f ⦿ w1) t))
  (w', t') = binddt ((ϕ (T B) ∘ f) ⦿ w') t'
    unfold compose; compose near t' on left.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
Happl: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
H6: Applicative G1
H7: Applicative G2
w': W
t': U A
(ϕ (U B) ∘ binddt (f ⦿ w')) t' =
binddt ((ϕ (T B) ○ f) ⦿ w') t'
    rewrite (kdtm_morph G1 G2 (U := U)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Mapdt_WF: Mapdt W F
T: Type -> Type
Return_T: Return T
U: Type -> Type
Binddt_WTU: Binddt W T U
Binddt_WTT: Binddt W T T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  W F
DecoratedTraversableRightPreModule0: DecoratedTraversableRightPreModule
  W T U
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
Happl: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: W * A -> G1 (T B)
H6: Applicative G1
H7: Applicative G2
w': W
t': U A
binddt (ϕ (T B) ∘ f ⦿ w') t' =
binddt ((ϕ (T B) ○ f) ⦿ w') t'
    reflexivity.
  Qed.

  (** ** <<DecoratedTraversableRightModule>> Instances *)
  (******************************************************************************)
  #[export] Instance DecoratedTraversableRightPreModule_compose:
    DecoratedTraversableRightPreModule W T (F ○ U) :=
    {| kdtm_binddt1 := kdtm_binddt1_compose;
      kdtm_binddt2 := kdtm_binddt2_compose;
      kdtm_morph := kdtm_morph_compose;
    |}.

End compose_functor_module.