From Tealeaves Require Import
  Classes.Categorical.DecoratedTraversableFunctor
  Classes.Categorical.Monad
  Classes.Categorical.DecoratedMonad
  Classes.Monoid
  Categories.DecoratedFunctor
  Categories.TraversableFunctor.

#[local] Generalizable Variables W T F U G X Y ϕ op zero.

Import TraversableFunctor.Notations.
Import Monad.Notations.
Import Strength.Notations.
Import Product.Notations.
Import Monoid.Notations.

#[local] Arguments map F%function_scope {Map}
  {A B}%type_scope f%function_scope _.
#[local] Arguments join T%function_scope {Join}
  {A}%type_scope _.

(** * Monoid Structure of Decorated Traversable Functors *)
(**********************************************************************)
Section DecoratedTraversableFunctor_monoid.

  Context
    `{@Monoid W op zero}.

  Section identity.

    Existing Instance DecoratedFunctor_zero.
    Existing Instance Traversable_I.

    (** ** The Identity Functor is Decorated Traversable *)
    (******************************************************************)
    #[program] Instance DecoratedTraversable_I:
      DecoratedTraversableFunctor W (fun A => A).

    Remove Hints DecoratedFunctor_zero: typeclass_instances.

  End identity.

  (** ** Decorated Traversable Functors are Closed under Composition *)
  (********************************************************************)
  Section compose.

    #[local] Set Keyed Unification.

    Context
      `{Monoid W}
      (U T: Type -> Type)
      `{DecoratedTraversableFunctor W T}
      `{DecoratedTraversableFunctor W U}.

    (** Push the applicative wire underneath a <<shift>> operation *)
    Lemma strength_shift: forall (A: Type) `{Applicative G},
        δ T G ∘ map T σ ∘ shift T (A := G A) =
          map G (shift T) ∘ σ ∘ map (W ×) (δ T G ∘ map T σ).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
forall (A : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
δ T G ∘ map T (σ) ∘ shift T =
map G (shift T) ∘ σ ∘ map (prod W) (δ T G ∘ map T (σ))
    Proof.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
forall (A : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
δ T G ∘ map T (σ) ∘ shift T =
map G (shift T) ∘ σ ∘ map (prod W) (δ T G ∘ map T (σ))
      intros.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ T G ∘ map T (σ) ∘ shift T =
map G (shift T) ∘ σ ∘ map (prod W) (δ T G ∘ map T (σ)) unfold shift.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ T G ∘ map T (σ) ∘ (map T (uncurry incr) ∘ σ) =
map G (map T (uncurry incr) ∘ σ) ∘ σ
∘ map (prod W) (δ T G ∘ map T (σ)) ext [w t].
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
(δ T G ∘ map T (σ) ∘ (map T (uncurry incr) ∘ σ))
  (w, t) =
(map G (map T (uncurry incr) ∘ σ) ∘ σ
 ∘ map (prod W) (δ T G ∘ map T (σ))) (w, t)
      unfold compose; cbn; unfold id.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
δ T G
  (map T (σ) (map T (uncurry incr) (map T (pair w) t))) =
map G (map T (uncurry incr) ○ σ)
  (map G (pair w) (δ T G (map T (σ) t)))
      compose near t on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
δ T G
  (map T (σ)
     ((map T (uncurry incr) ∘ map T (pair w)) t)) =
map G (map T (uncurry incr) ○ σ)
  (map G (pair w) (δ T G (map T (σ) t))) rewrite (fun_map_map (F := T)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
δ T G (map T (σ) (map T (uncurry incr ∘ pair w) t)) =
map G (map T (uncurry incr) ○ σ)
  (map G (pair w) (δ T G (map T (σ) t)))
      compose near t on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
δ T G ((map T (σ) ∘ map T (uncurry incr ∘ pair w)) t) =
map G (map T (uncurry incr) ○ σ)
  (map G (pair w) (δ T G (map T (σ) t))) rewrite (fun_map_map (F := T)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
δ T G (map T (σ ∘ (uncurry incr ∘ pair w)) t) =
map G (map T (uncurry incr) ○ σ)
  (map G (pair w) (δ T G (map T (σ) t)))
      compose near ((δ T G (map T σ t))) on right.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
δ T G (map T (σ ∘ (uncurry incr ∘ pair w)) t) =
(map G (map T (uncurry incr) ○ σ) ∘ map G (pair w))
  (δ T G (map T (σ) t))
      rewrite (fun_map_map (F := G)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
δ T G (map T (σ ∘ (uncurry incr ∘ pair w)) t) =
map G (map T (uncurry incr) ○ σ ∘ pair w)
  (δ T G (map T (σ) t))
      reassociate <- on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
δ T G (map T (σ ∘ uncurry incr ∘ pair w) t) =
map G (map T (uncurry incr) ○ σ ∘ pair w)
  (δ T G (map T (σ) t))
      rewrite 2(incr_spec).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
δ T G (map T (σ ∘ join (prod W) ∘ pair w) t) =
map G (map T (join (prod W)) ○ σ ∘ pair w)
  (δ T G (map T (σ) t))
      rewrite (strength_join_l (F := G) (W := W)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
δ T G
  (map T
     (map G (join (prod W)) ∘ σ ∘ map (prod W) (σ)
      ∘ pair w) t) =
map G (map T (join (prod W)) ○ σ ∘ pair w)
  (δ T G (map T (σ) t))
      do 2 reassociate -> on left;
      rewrite <- (fun_map_map (F := T));
      reassociate <- on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
δ T G
  ((map T (map G (join (prod W)))
    ∘ map T (σ ∘ map (prod W) (σ) ∘ pair w)) t) =
map G (map T (join (prod W)) ○ σ ∘ pair w)
  (δ T G (map T (σ) t))
      change (map T (map G ?f)) with (map (T ∘ G) f).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
δ T G
  ((map (T ∘ G) (join (prod W))
    ∘ map T (σ ∘ map (prod W) (σ) ∘ pair w)) t) =
map G (map T (join (prod W)) ○ σ ∘ pair w)
  (δ T G (map T (σ) t))
      change (δ T G ((map (T ∘ G) (join (prod W)) ∘ ?f) t))
        with ((δ T G ∘ map (T ∘ G) (join (prod W))) (f t)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
(δ T G ∘ map (T ∘ G) (join (prod W)))
  (map T (σ ∘ map (prod W) (σ) ∘ pair w) t) =
map G (map T (join (prod W)) ○ σ ∘ pair w)
  (δ T G (map T (σ) t))
      rewrite <- (natural (ϕ := @dist T _ G _ _ _ )).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
(map (G ○ T) (join (prod W)) ∘ δ T G)
  (map T (σ ∘ map (prod W) (σ) ∘ pair w) t) =
map G (map T (join (prod W)) ○ σ ∘ pair w)
  (δ T G (map T (σ) t))
      (* now focus on the RHS *)
      unfold id.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
(map (G ○ T) (join (prod W)) ∘ δ T G)
  (map T (σ ∘ map (prod W) (σ) ∘ pair w) t) =
map G (map T (join (prod W)) ○ σ ∘ pair w)
  (δ T G (map T (σ) t))
      change (map T (join (prod W) (A := ?A)) ○ σ ∘ pair w)
        with  (map T (join (prod W) (A := A)) ∘ (σ ∘ pair w)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
(map (G ○ T) (join (prod W)) ∘ δ T G)
  (map T (σ ∘ map (prod W) (σ) ∘ pair w) t) =
map G (map T (join (prod W)) ∘ (σ ∘ pair w))
  (δ T G (map T (σ) t))
      rewrite (strength_2).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
(map (G ○ T) (join (prod W)) ∘ δ T G)
  (map T (σ ∘ map (prod W) (σ) ∘ pair w) t) =
map G (map T (join (prod W)) ∘ map T (pair w))
  (δ T G (map T (σ) t))
      rewrite <- (fun_map_map (F := G)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
(map (G ○ T) (join (prod W)) ∘ δ T G)
  (map T (σ ∘ map (prod W) (σ) ∘ pair w) t) =
(map G (map T (join (prod W)))
 ∘ map G (map T (pair w))) (δ T G (map T (σ) t))
      compose near (map T σ t) on right.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
(map (G ○ T) (join (prod W)) ∘ δ T G)
  (map T (σ ∘ map (prod W) (σ) ∘ pair w) t) =
(map G (map T (join (prod W)))
 ∘ map G (map T (pair w)) ∘ δ T G) (map T (σ) t)
      reassociate -> on right.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
(map (G ○ T) (join (prod W)) ∘ δ T G)
  (map T (σ ∘ map (prod W) (σ) ∘ pair w) t) =
(map G (map T (join (prod W)))
 ∘ (map G (map T (pair w)) ∘ δ T G)) (map T (σ) t)
      change (map G (map T ?f)) with (map (G ∘ T) f).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
(map (G ○ T) (join (prod W)) ∘ δ T G)
  (map T (σ ∘ map (prod W) (σ) ∘ pair w) t) =
(map (G ∘ T) (join (prod W))
 ∘ (map (G ∘ T) (pair w) ∘ δ T G)) (map T (σ) t)
      rewrite (natural (ϕ := @dist T _ G _ _ _) (pair w)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
(map (G ○ T) (join (prod W)) ∘ δ T G)
  (map T (σ ∘ map (prod W) (σ) ∘ pair w) t) =
(map (G ∘ T) (join (prod W))
 ∘ (δ T G ∘ map (T ○ G) (pair w))) (map T (σ) t)
      unfold compose.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
map (G ○ T) (join (prod W))
  (δ T G
     (map T
        (fun a : W * G A =>
         σ (map (prod W) (σ) (w, a))) t)) =
map (G ○ T) (join (prod W))
  (δ T G (map (T ○ G) (pair w) (map T (σ) t))) compose near t on right.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
w: W
t: T (W * G A)
map (G ○ T) (join (prod W))
  (δ T G
     (map T
        (fun a : W * G A =>
         σ (map (prod W) (σ) (w, a))) t)) =
map (G ○ T) (join (prod W))
  (δ T G ((map (T ○ G) (pair w) ∘ map T (σ)) t))
      now rewrite (fun_map_map (F := T)).
    Qed.

    (** Push the applicative wire underneath a <<dec (U∘T)>> operation *)
    Lemma strength_shift2: forall (A: Type) `{Applicative G},
        δ U G ∘ map U (σ ∘ map (prod W) (δ T G ∘ map T σ))
          ∘ (dec U ∘ map U (dec T (A := G A))) =
          map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
forall (A : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
δ U G ∘ map U (σ ∘ map (prod W) (δ T G ∘ map T (σ)))
∘ (dec U ∘ map U (dec T)) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
    Proof.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
forall (A : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
δ U G ∘ map U (σ ∘ map (prod W) (δ T G ∘ map T (σ)))
∘ (dec U ∘ map U (dec T)) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      intros.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ U G ∘ map U (σ ∘ map (prod W) (δ T G ∘ map T (σ)))
∘ (dec U ∘ map U (dec T)) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G rewrite <- (natural (ϕ := @dec W U _)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ U G ∘ map U (σ ∘ map (prod W) (δ T G ∘ map T (σ)))
∘ (map (U ○ prod W) (dec T) ∘ dec U) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      reassociate <- on left;
        reassociate -> near (map (U ○ prod W) (dec T)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ U G
∘ (map U (σ ∘ map (prod W) (δ T G ∘ map T (σ)))
   ∘ map (U ○ prod W) (dec T)) ∘ dec U =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      rewrite (fun_map_map (F := U)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ U G
∘ map U
    (σ ∘ map (prod W) (δ T G ∘ map T (σ))
     ∘ map (prod W) (dec T)) ∘ dec U =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G do 2 reassociate -> on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ U G
∘ (map U
     (σ
      ∘ (map (prod W) (δ T G ∘ map T (σ))
         ∘ map (prod W) (dec T))) ∘ dec U) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      rewrite (fun_map_map (F := prod W)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ U G
∘ (map U
     (σ ∘ map (prod W) (δ T G ∘ map T (σ) ∘ dec T))
   ∘ dec U) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      rewrite (dtfun_compat A); auto.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ U G
∘ (map U (σ ∘ map (prod W) (map G (dec T) ∘ δ T G))
   ∘ dec U) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      rewrite <- (fun_map_map (F := U)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ U G
∘ (map U (σ)
   ∘ map U (map (prod W) (map G (dec T) ∘ δ T G))
   ∘ dec U) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      change (map U (map (W ×) ?f)) with (map (U ∘ (W ×)) f).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ U G
∘ (map U (σ)
   ∘ map (U ∘ prod W) (map G (dec T) ∘ δ T G) ∘ dec U) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      reassociate -> on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ U G
∘ (map U (σ)
   ∘ (map (U ∘ prod W) (map G (dec T) ∘ δ T G) ∘ dec U)) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G rewrite (natural (ϕ := @dec W U _)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ U G
∘ (map U (σ) ∘ (dec U ∘ map U (map G (dec T) ∘ δ T G))) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      do 2 reassociate <- on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
δ U G ∘ map U (σ) ∘ dec U
∘ map U (map G (dec T) ∘ δ T G) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      rewrite (dtfun_compat _); auto.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
map G (dec U) ∘ δ U G ∘ map U (map G (dec T) ∘ δ T G) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      rewrite <- (fun_map_map (F := U)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
map G (dec U) ∘ δ U G
∘ (map U (map G (dec T)) ∘ map U (δ T G)) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G reassociate <- on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
map G (dec U) ∘ δ U G ∘ map U (map G (dec T))
∘ map U (δ T G) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      change (map U (map G ?f)) with (map (U ∘ G) f).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
map G (dec U) ∘ δ U G ∘ map (U ∘ G) (dec T)
∘ map U (δ T G) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      reassociate -> near (map (U ∘ G) (dec T)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
map G (dec U) ∘ (δ U G ∘ map (U ∘ G) (dec T))
∘ map U (δ T G) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      rewrite <- (natural (ϕ := @dist U _ G _ _ _)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
map G (dec U) ∘ (map (G ○ U) (dec T) ∘ δ U G)
∘ map U (δ T G) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      reassociate <- on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
map G (dec U) ∘ map (G ○ U) (dec T) ∘ δ U G
∘ map U (δ T G) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G
      rewrite (fun_map_map (F := G)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
A: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
map G (dec U ∘ map U (dec T)) ∘ δ U G ∘ map U (δ T G) =
map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G reflexivity.
    Qed.

    Theorem dtfun_compat_compose: forall `{Applicative G} {A: Type},
        δ (U ∘ T) G ∘ map (U ∘ T) σ ∘ dec (U ∘ T) (A := G A) =
          map G (dec (U ∘ T)) ∘ dist (U ∘ T) G.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall A : Type,
δ (U ∘ T) G ∘ map (U ∘ T) (σ) ∘ dec (U ∘ T) =
map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
    Proof.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall A : Type,
δ (U ∘ T) G ∘ map (U ∘ T) (σ) ∘ dec (U ∘ T) =
map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      intros.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
δ (U ∘ T) G ∘ map (U ∘ T) (σ) ∘ dec (U ∘ T) =
map G (dec (U ∘ T)) ∘ δ (U ∘ T) G reassociate -> on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
δ (U ∘ T) G ∘ (map (U ∘ T) (σ) ∘ dec (U ∘ T)) =
map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      unfold dec at 1, Decorate_compose.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
δ (U ∘ T) G
∘ (map (U ∘ T) (σ)
   ∘ (map U (shift T) ∘ dec U ∘ map U (dec T))) =
map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      unfold dist at 1, Dist_compose.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
δ U G ∘ map U (δ T G)
∘ (map (U ∘ T) (σ)
   ∘ (map U (shift T) ∘ dec U ∘ map U (dec T))) =
map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      (* bring <<strength G >> and <<shift T>> together*)
      do 3 reassociate <- on left;
      reassociate -> near (map U (shift T));
      rewrite (fun_map_map (F := U)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
δ U G ∘ map U (δ T G) ∘ map U (map T (σ) ∘ shift T)
∘ dec U ∘ map U (dec T) =
map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      reassociate -> near (map U (map T σ ∘ shift T)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
δ U G ∘ (map U (δ T G) ∘ map U (map T (σ) ∘ shift T))
∘ dec U ∘ map U (dec T) =
map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      rewrite (fun_map_map (F := U)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
δ U G ∘ map U (δ T G ∘ (map T (σ) ∘ shift T)) ∘ dec U
∘ map U (dec T) = map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      reassociate <- on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
δ U G ∘ map U (δ T G ∘ map T (σ) ∘ shift T) ∘ dec U
∘ map U (dec T) = map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      rewrite (strength_shift); auto.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
δ U G
∘ map U
    (map G (shift T) ∘ σ
     ∘ map (prod W) (δ T G ∘ map T (σ))) ∘ dec U
∘ map U (dec T) = map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      (* move <<δ U G>> under <<shift>> *)
      do 3 reassociate -> on left;
      rewrite <- (fun_map_map (F := U));
      do 3 reassociate <- on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
δ U G ∘ map U (map G (shift T))
∘ map U (σ ∘ map (prod W) (δ T G ∘ map T (σ))) ∘ dec U
∘ map U (dec T) = map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      change (map U (map G ?f)) with (map (U ∘ G) f).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
δ U G ∘ map (U ∘ G) (shift T)
∘ map U (σ ∘ map (prod W) (δ T G ∘ map T (σ))) ∘ dec U
∘ map U (dec T) = map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      rewrite <- (natural (ϕ := @dist U _ G _ _ _) (shift T)).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
map (G ○ U) (shift T) ∘ δ U G
∘ map U (σ ∘ map (prod W) (δ T G ∘ map T (σ))) ∘ dec U
∘ map U (dec T) = map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      do 3 reassociate -> on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
map (G ○ U) (shift T)
∘ (δ U G
   ∘ (map U (σ ∘ map (prod W) (δ T G ∘ map T (σ)))
      ∘ (dec U ∘ map U (dec T)))) =
map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      reassociate <- near (δ U G).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
map (G ○ U) (shift T)
∘ (δ U G
   ∘ map U (σ ∘ map (prod W) (δ T G ∘ map T (σ)))
   ∘ (dec U ∘ map U (dec T))) =
map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      rewrite strength_shift2; auto.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
map (G ○ U) (shift T)
∘ (map G (dec U ∘ map U (dec T)) ∘ δ (U ∘ T) G) =
map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      reassociate <- on left.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H9: Applicative G
A: Type
map (G ○ U) (shift T) ∘ map G (dec U ∘ map U (dec T))
∘ δ (U ∘ T) G = map G (dec (U ∘ T)) ∘ δ (U ∘ T) G
      now rewrite (fun_map_map (F := G)).
    Qed.

    (* TODO Investigate why DecoratedFunctor_compose solve the next
       instance automatically It seems like <<dtfun_decorated>> needs
       extra help here.  It seems like it doesn't want to pick up on
       the Dist instance or something.  *)
    Lemma composition_is_decorated: DecoratedFunctor W (U ∘ T).
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
DecoratedFunctor W (U ∘ T)
    Proof.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
DecoratedFunctor W (U ∘ T)
      inversion H4.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
dtfun_decorated: DecoratedFunctor W T
dtfun_traversable: TraversableFunctor T
dtfun_compat: forall (G : Type -> Type)
  (Map_G : Map G) (Pure_G : Pure G)
  (Mult_G : Mult G),
Applicative G ->
forall A : Type,
δ T G ∘ map T (σ) ∘ dec T =
map G (dec T) ∘ δ T G
DecoratedFunctor W (U ∘ T)
      inversion H8.
W: Type
op: Monoid_op W
zero: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit0: Monoid_unit W
H0: Monoid W
U, T: Type -> Type
H1: Map T
H2: Decorate W T
H3: ApplicativeDist T
H4: DecoratedTraversableFunctor W T
H5: Map U
H6: Decorate W U
H7: ApplicativeDist U
H8: DecoratedTraversableFunctor W U
dtfun_decorated: DecoratedFunctor W T
dtfun_traversable: TraversableFunctor T
dtfun_compat: forall (G : Type -> Type)
  (Map_G : Map G) (Pure_G : Pure G)
  (Mult_G : Mult G),
Applicative G ->
forall A : Type,
δ T G ∘ map T (σ) ∘ dec T =
map G (dec T) ∘ δ T G
dtfun_decorated0: DecoratedFunctor W U
dtfun_traversable0: TraversableFunctor U
dtfun_compat0: forall (G : Type -> Type)
  (Map_G : Map G) (Pure_G : Pure G)
  (Mult_G : Mult G),
Applicative G ->
forall A : Type,
δ U G ∘ map U (σ) ∘ dec U =
map G (dec U) ∘ δ U G
DecoratedFunctor W (U ∘ T)
      apply DecoratedFunctor_compose.
    Qed.

    #[program, global] Instance DecoratedTraversableFunctor_compose:
      DecoratedTraversableFunctor W (U ∘ T) :=
      {| dtfun_decorated := composition_is_decorated;
         dtfun_compat := @dtfun_compat_compose;
      |}.

  End compose.

End DecoratedTraversableFunctor_monoid.

(** ** Null-Decorated Traversable Functors are Decorated Traversable *)
(**********************************************************************)
Section TraversableFunctor_zero_DT.

  Context
    (T: Type -> Type)
    `{TraversableFunctor T}
    `{Monoid W}.

  Existing Instance Decorate_zero.
  Existing Instance DecoratedFunctor_zero.

  Theorem dtfun_compat_zero: forall `{Applicative G} {A: Type},
      dist T G ∘ map T σ ∘ dec T =
        map G (dec T) ∘ dist T G (A := A).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H2: Monoid W
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall A : Type,
δ T G ∘ map T (σ) ∘ dec T = map G (dec T) ∘ δ T G
  Proof.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H2: Monoid W
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall A : Type,
δ T G ∘ map T (σ) ∘ dec T = map G (dec T) ∘ δ T G
    intros.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H2: Monoid W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H3: Applicative G
A: Type
δ T G ∘ map T (σ) ∘ dec T = map G (dec T) ∘ δ T G unfold_ops @Decorate_zero.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H2: Monoid W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H3: Applicative G
A: Type
δ T G ∘ map T (σ) ∘ map T (pair Ƶ) =
map G (map T (pair Ƶ)) ∘ δ T G
    reassociate -> on left.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H2: Monoid W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H3: Applicative G
A: Type
δ T G ∘ (map T (σ) ∘ map T (pair Ƶ)) =
map G (map T (pair Ƶ)) ∘ δ T G rewrite (fun_map_map (F := T)).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H2: Monoid W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H3: Applicative G
A: Type
δ T G ∘ map T (σ ∘ pair Ƶ) =
map G (map T (pair Ƶ)) ∘ δ T G
    change_right (map (G ∘ T) (pair Ƶ) ∘ δ T G (A := A)).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H2: Monoid W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H3: Applicative G
A: Type
δ T G ∘ map T (σ ∘ pair Ƶ) =
map (G ∘ T) (pair Ƶ) ∘ δ T G
    rewrite (natural (ϕ := @dist T _ G _ _ _) (@pair W A Ƶ)).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H2: Monoid W
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H3: Applicative G
A: Type
δ T G ∘ map T (σ ∘ pair Ƶ) =
δ T G ∘ map (T ○ G) (pair Ƶ)
    now unfold_ops @Map_compose.
  Qed.

  Instance DecoratedTraversableFunctor_zero:
    DecoratedTraversableFunctor W T :=
    {| dtfun_compat := @dtfun_compat_zero
    |}.

End TraversableFunctor_zero_DT.

(** ** Identity and Associativity Laws *)
(* TODO *)
(**********************************************************************)