From Tealeaves Require Import
  Classes.Categorical.DecoratedFunctor
  Classes.Categorical.DecoratedMonad (shift, shift_map2, shift_spec, shift_zero, shift_extract)
  Classes.Categorical.RightComodule
  Classes.Categorical.Bimonad
  Functors.Early.Writer.

#[local] Generalizable Variables E T W F G.

Import Monad.Notations.
Import Strength.Notations.
Import Product.Notations.
Import Monoid.Notations.
Import Categorical.Monad.Notations.

#[local] Arguments map F%function_scope {Map} {A B}%type_scope f%function_scope _.
#[local] Arguments dec {E}%type_scope F%function_scope {Decorate} {A}%type_scope _.
#[local] Arguments ret T%function_scope {Return} (A)%type_scope _.
#[local] Arguments join T%function_scope {Join} {A}%type_scope _.

(** * A Decorated Functor is Precisely a Right comodule of <<(E ×)>> *)
(**********************************************************************)
Definition RightComodule_DecoratedFunctor
  `{DecoratedFunctor E F}
 : RightComodule F (prod E) :=
  {| rcom_coaction_coaction := dfun_dec_dec;
     rcom_map_extr_coaction := dfun_dec_extract;
  |}.

Definition DecoratedFunctor_RightComodule
  `{Map F} `{RightCoaction F (prod E)}
  `{! RightComodule F (prod E)} `{Monoid E}
 : DecoratedFunctor E F :=
  {| dfun_dec_dec := rcom_coaction_coaction;
     dfun_dec_extract := rcom_map_extr_coaction;
  |}.

(** * Decorated Functors Form a Monoidal Category *)
(**********************************************************************)

(** ** Null-Decorated Functors *)
(** Every functor is trivially decorated using the operation that
    pairs each leaf with the unit of the monoid. We call such functors
    null-decorated. This allows us to see _all_ functors as (maybe
    trivially) decorated. *)
(**********************************************************************)
Section DecoratedFunctor_Zero.

  Context
    `{Monoid W}
    `{Functor F}.

  Instance Decorate_zero: Decorate W F :=
    fun A => @map F _ A (W * A) (pair Ƶ).

  Instance Natural_dec_zero:
    Natural (@dec W F _).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
Natural (@dec W F Decorate_zero)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
Natural (@dec W F Decorate_zero)
    constructor; try typeclasses eauto.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
forall (A B : Type) (f : A -> B),
map (F ○ prod W) f ∘ dec F = dec F ∘ map F f
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A, B: Type
f: A -> B
map (F ○ prod W) f ∘ dec F = dec F ∘ map F f unfold_ops @Map_compose @Decorate_zero.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A, B: Type
f: A -> B
map F (map (prod W) f) ∘ map F (pair Ƶ) =
map F (pair Ƶ) ∘ map F f
    now do 2 rewrite fun_map_map.
  Qed.

  Lemma dec_dec_zero {A}:
    dec F ∘ dec F (A:=A) =
    map F (cojoin (W :=(W ×))) ∘ dec F.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
dec F ∘ dec F = map F cojoin ∘ dec F
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
dec F ∘ dec F = map F cojoin ∘ dec F
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
dec F ∘ dec F = map F cojoin ∘ dec F unfold_ops @Decorate_zero.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
map F (pair Ƶ) ∘ map F (pair Ƶ) =
map F cojoin ∘ map F (pair Ƶ)
    now do 2 rewrite fun_map_map.
  Qed.

  Lemma dec_extract_zero {A}:
    map F (extract (W := (W ×))) ∘ dec F = @id (F A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
map F extract ∘ dec F = id
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
map F extract ∘ dec F = id
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
map F extract ∘ dec F = id unfold_ops @Decorate_zero.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
map F extract ∘ map F (pair Ƶ) = id
    rewrite fun_map_map.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
map F (extract ∘ pair Ƶ) = id
    unfold compose; cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
map F (fun a : A => a) = id
    now rewrite fun_map_id.
  Qed.

  Instance DecoratedFunctor_zero: DecoratedFunctor W F :=
    {| dfun_dec_natural := Natural_dec_zero;
       dfun_dec_dec := @dec_dec_zero;
       dfun_dec_extract := @dec_extract_zero;
    |}.

End DecoratedFunctor_Zero.

(** ** The Identity Null-Decorated functor *)
(**********************************************************************)
Section DecoratedFunctor_I.

  Context
    `{Monoid W}.

  Definition dec_I: forall A, A -> prod W A :=
    fun A => @pair W A Ƶ.

  #[global] Instance Decorate_I: Decorate W (fun A => A) := dec_I.

  #[global] Instance Natural_dec_I:
    Natural (G:=prod W) (fun _ => dec (fun A => A)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Natural (fun A : Type => dec (fun A0 : Type => A0))
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Natural (fun A : Type => dec (fun A0 : Type => A0))
    constructor; try typeclasses eauto.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : A -> B),
map (prod W) f ∘ dec (fun A0 : Type => A0) =
dec (fun A0 : Type => A0) ∘ map (fun H : Type => H) f
    reflexivity.
  Qed.

  Lemma dec_dec_I {A}:
    dec (fun A => A) ∘ dec (A:=A) (fun A => A) =
    map (fun A => A) (fun '(n, a) => (n, (n, a))) ∘ dec (fun A => A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
dec (fun A : Type => A) ∘ dec (fun A : Type => A) =
map (fun A : Type => A) (fun '(n, a) => (n, (n, a)))
∘ dec (fun A : Type => A)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
dec (fun A : Type => A) ∘ dec (fun A : Type => A) =
map (fun A : Type => A) (fun '(n, a) => (n, (n, a)))
∘ dec (fun A : Type => A)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
dec (fun A : Type => A) ∘ dec (fun A : Type => A) =
map (fun A : Type => A) (fun '(n, a) => (n, (n, a)))
∘ dec (fun A : Type => A) cbv.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
pair unit0 ○ pair unit0 = pair unit0 ○ pair unit0
    reflexivity.
  Qed.

  Lemma dec_extract_I {A}:
    map (fun A => A) (extract (W := (W ×))) ∘ dec (fun A => A) = (@id A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
map (fun A : Type => A) extract
∘ dec (fun A : Type => A) = id
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
map (fun A : Type => A) extract
∘ dec (fun A : Type => A) = id
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
map (fun A : Type => A) extract
∘ dec (fun A : Type => A) = id reflexivity.
  Qed.

  #[global] Instance DecoratedFunctor_I:
    DecoratedFunctor W (fun A => A) :=
    {| dfun_dec_natural := Natural_dec_I;
       dfun_dec_dec := @dec_dec_I;
       dfun_dec_extract := @dec_extract_I;
    |}.

End DecoratedFunctor_I.

(** ** Decorated Functors are Closed under Composition *)
(**********************************************************************)
Section Decoratedfunctor_composition.

  Context
    `{Monoid W}
    `{Map F} `{Map G}
    `{Decorate W F} `{Decorate W G}
    `{! DecoratedFunctor W F}
    `{! DecoratedFunctor W G}.

  #[global] Instance Decorate_compose: Decorate W (F ∘ G) :=
    fun A => map F (shift G) ∘ dec F ∘ map F (dec G).

  Instance Natural_dec_compose:
    Natural (fun A => dec (A:=A) (E:=W) (F ∘ G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
Natural (fun A : Type => dec (F ∘ G))
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
Natural (fun A : Type => dec (F ∘ G))
    constructor; try typeclasses eauto.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
forall (A B : Type) (f : A -> B),
map (F ∘ G ○ prod W) f ∘ dec (F ∘ G) =
dec (F ∘ G) ∘ map (F ∘ G) f introv.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map (F ∘ G ○ prod W) f ∘ dec (F ∘ G) =
dec (F ∘ G) ∘ map (F ∘ G) f
    unfold_ops @Map_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map (F ∘ G) (map (prod W) f) ∘ dec (F ∘ G) =
dec (F ∘ G) ∘ map F (map G f) unfold map at 1.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (map G (map (prod W) f)) ∘ dec (F ∘ G) =
dec (F ∘ G) ∘ map F (map G f)
    unfold_ops @Decorate_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (map G (map (prod W) f))
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (map G f)
    (* Move << F (shift G)>> past <<F (G ∘ F) f>>. *)
    repeat reassociate <- on left.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (map G (map (prod W) f)) ∘ map F (shift G)
∘ dec F ∘ map F (dec G) =
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (map G f)
    unfold_compose_in_compose; rewrite (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (map G (map (prod W) f) ∘ shift G) ∘ dec F
∘ map F (dec G) =
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (map G f)
    change (map G (map (W ×) f)) with (map (G ∘ (W ×)) f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (map (G ∘ prod W) f ∘ shift G) ∘ dec F
∘ map F (dec G) =
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (map G f)
    #[local] Set Keyed Unification.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (map (G ∘ prod W) f ∘ shift G) ∘ dec F
∘ map F (dec G) =
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (map G f)
    rewrite (shift_map2 G).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (shift G ∘ map (prod W ∘ G ∘ prod W) f) ∘ dec F
∘ map F (dec G) =
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (map G f)
    #[local] Unset Keyed Unification.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (shift G ∘ map (prod W ∘ G ∘ prod W) f) ∘ dec F
∘ map F (dec G) =
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (map G f)
    rewrite <- (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (shift G) ∘ map F (map (prod W ∘ G ∘ prod W) f)
∘ dec F ∘ map F (dec G) =
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (map G f)
    (* mov <<dec F>> past <<F ∘ W ∘ G ∘ W f>> *)
    change (map F (map (prod W ∘ G ∘ prod W) f))
      with (map (F ∘ prod W) (map (G ∘ prod W) f)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (shift G)
∘ map (F ∘ prod W) (map (G ∘ prod W) f) ∘ dec F
∘ map F (dec G) =
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (map G f)
    repeat reassociate ->;
      reassociate <- near (map (F ∘ prod W) (map (G ∘ prod W) f)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (shift G)
∘ (map (F ∘ prod W) (map (G ∘ prod W) f) ∘ dec F
   ∘ map F (dec G)) =
map F (shift G)
∘ (dec F ∘ (map F (dec G) ∘ map F (map G f)))
    rewrite (natural (G := F ∘ prod W) (ϕ := @dec W F _)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (shift G)
∘ (dec F ∘ map F (map (G ∘ prod W) f) ∘ map F (dec G)) =
map F (shift G)
∘ (dec F ∘ (map F (dec G) ∘ map F (map G f)))
    (* move <<F (dec G)>> past <<F ((G ∘ W) f)>> *)
    reassociate -> on left.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (shift G)
∘ (dec F
   ∘ (map F (map (G ∘ prod W) f) ∘ map F (dec G))) =
map F (shift G)
∘ (dec F ∘ (map F (dec G) ∘ map F (map G f)))
    rewrite (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (shift G)
∘ (dec F ∘ map F (map (G ∘ prod W) f ∘ dec G)) =
map F (shift G)
∘ (dec F ∘ (map F (dec G) ∘ map F (map G f)))
    #[local] Set Keyed Unification.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (shift G)
∘ (dec F ∘ map F (map (G ∘ prod W) f ∘ dec G)) =
map F (shift G)
∘ (dec F ∘ (map F (dec G) ∘ map F (map G f)))
    rewrite (natural (G := G ∘ prod W) (ϕ := @dec W G _)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (shift G) ∘ (dec F ∘ map F (dec G ∘ map G f)) =
map F (shift G)
∘ (dec F ∘ (map F (dec G) ∘ map F (map G f)))
    #[local] Unset Keyed Unification.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A, B: Type
f: A -> B
map F (shift G) ∘ (dec F ∘ map F (dec G ∘ map G f)) =
map F (shift G)
∘ (dec F ∘ (map F (dec G) ∘ map F (map G f)))
    now rewrite <- (fun_map_map (F := F)).
  Qed.

  (** The next few lemmas are used to build up a proof of the
   "double decoration law", [dfun_dec_dec (F ∘ G)] *)

  (** Split the decoration wire on <<G>> into two wires with
      <<dfun_dec_dec G>> law. *)
  Lemma dec_dec_compose_1 {A}:
    (map F (map (G ∘ prod W) (cojoin (W := prod W)) ∘ strength (F := G)))
      ∘ dec F
      ∘ map F (dec G)
    = (map F (strength (F := G)))
        ∘ dec F
        ∘ map F (dec G ∘ dec G (A := A)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map (G ∘ prod W) cojoin ∘ σ) ∘ dec F
∘ map F (dec G) =
map F (σ) ∘ dec F ∘ map F (dec G ∘ dec G)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map (G ∘ prod W) cojoin ∘ σ) ∘ dec F
∘ map F (dec G) =
map F (σ) ∘ dec F ∘ map F (dec G ∘ dec G)
    (* Move <<F (strength)>> past <<F ((W ○ G) (cojoin (prod W)))>> *)
    rewrite (natural (G := (G ∘ prod W)) (ϕ := @strength G _ W)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ ∘ map (prod W ○ G) cojoin) ∘ dec F
∘ map F (dec G) =
map F (σ) ∘ dec F ∘ map F (dec G ∘ dec G)
    unfold_ops @Map_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ ∘ map (prod W) (map G cojoin)) ∘ dec F
∘ map F (dec G) =
map F (σ) ∘ dec F ∘ map F (dec G ∘ dec G)
    rewrite <- (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ map F (map (prod W) (map G cojoin))
∘ dec F ∘ map F (dec G) =
map F (σ) ∘ dec F ∘ map F (dec G ∘ dec G)
    (* Move <<dec F>> past <<F ((W ○ G) (cojoin (prod W)))>> *)
    change (map ?F (map (prod W) ?f)) with (map (F ∘ (prod W)) f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ map (F ∘ prod W) (map G cojoin) ∘ dec F
∘ map F (dec G) =
map F (σ) ∘ dec F ∘ map F (dec G ∘ dec G)
    reassociate -> near (dec F).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ (map (F ∘ prod W) (map G cojoin) ∘ dec F)
∘ map F (dec G) =
map F (σ) ∘ dec F ∘ map F (dec G ∘ dec G)
    rewrite (natural (ϕ := @dec W F _) (G := F ∘ prod W)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ (dec F ∘ map F (map G cojoin))
∘ map F (dec G) =
map F (σ) ∘ dec F ∘ map F (dec G ∘ dec G)
    do 2 reassociate -> near (map F (dec G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ)
∘ (dec F ∘ (map F (map G cojoin) ∘ map F (dec G))) =
map F (σ) ∘ dec F ∘ map F (dec G ∘ dec G)
    rewrite (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ (dec F ∘ map F (map G cojoin ∘ dec G)) =
map F (σ) ∘ dec F ∘ map F (dec G ∘ dec G)
    now rewrite <- (dfun_dec_dec (E := W) (F := G)).
  Qed.

  Lemma strength_cojoin_r {A}:
    (map G (cojoin (W := (W ×))))
      ∘ strength (F := G)
    = strength (F := G)
        ∘ map (prod W) (strength (F := G))
        ∘ cojoin (W := (W ×)) (A := G A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map G cojoin ∘ σ = σ ∘ map (prod W) (σ) ∘ cojoin
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map G cojoin ∘ σ = σ ∘ map (prod W) (σ) ∘ cojoin
    ext [w a].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
w: W
a: G A
(map G cojoin ∘ σ) (w, a) =
(σ ∘ map (prod W) (σ) ∘ cojoin) (w, a) unfold strength, compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
w: W
a: G A
map G cojoin (map G (pair w) a) =
(let
 '(a, t) :=
  map (prod W) (fun '(a, t) => map G (pair a) t)
    (cojoin (w, a)) in map G (pair a) t) cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
w: W
a: G A
map G cojoin (map G (pair w) a) =
map G (pair (id w)) (map G (pair w) a)
    compose near a.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
w: W
a: G A
(map G cojoin ∘ map G (pair w)) a =
(map G (pair (id w)) ∘ map G (pair w)) a now do 2 rewrite (fun_map_map (F := G)).
  Qed.

  (** Split the decoration wire on <<F>> into two wires with
     <<dfun_dec_dec F>>. *)
  Lemma dec_dec_compose_2 {A}:
    (map F (map G (cojoin (W := prod W)) ∘ strength))
      ∘ dec F
    = (map F strength)
        ∘ dec F
        ∘ map F strength
        ∘ dec F (A := G A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G cojoin ∘ σ) ∘ dec F =
map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G cojoin ∘ σ) ∘ dec F =
map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F
    rewrite strength_cojoin_r.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ ∘ map (prod W) (σ) ∘ cojoin) ∘ dec F =
map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F
    rewrite <- (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ ∘ map (prod W) (σ)) ∘ map F cojoin ∘ dec F =
map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F
    reassociate -> on left.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ ∘ map (prod W) (σ)) ∘ (map F cojoin ∘ dec F) =
map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F rewrite <- (dfun_dec_dec (E := W) (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ ∘ map (prod W) (σ)) ∘ (dec F ∘ dec F) =
map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F
    reassociate <- on left.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ ∘ map (prod W) (σ)) ∘ dec F ∘ dec F =
map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F
    rewrite <- (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ map F (map (prod W) (σ)) ∘ dec F ∘ dec F =
map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F
    change (?f ∘ map F (map (prod W) strength) ∘ dec F ∘ ?g)
      with (f ∘ (map F (map (prod W) strength) ∘ dec F) ∘ g).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ (map F (map (prod W) (σ)) ∘ dec F) ∘ dec F =
map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F
    change (map ?F (map ?G ?f)) with (map (F ∘ G) f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ (map (F ∘ prod W) (σ) ∘ dec F) ∘ dec F =
map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F
    now rewrite (natural (ϕ := @dec W F _) (strength (B := A))).
  Qed.

  (** Slide the upper decoration wire on <<G>> past the lower
  decoration wire on <<F>>, which requires crossing them. *)
  Lemma dec_dec_compose_3 {A}:
    (map F strength)
      ∘ dec F
      ∘ map F (dec G) =
    (map (F ∘ G) (bdist (prod W) (prod W)))
      ∘ map F (dec G)
      ∘ map F strength
      ∘ dec F (A := G A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ dec F ∘ map F (dec G) =
map (F ∘ G) (bdist (prod W) (prod W)) ∘ map F (dec G)
∘ map F (σ) ∘ dec F
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ dec F ∘ map F (dec G) =
map (F ∘ G) (bdist (prod W) (prod W)) ∘ map F (dec G)
∘ map F (σ) ∘ dec F
    unfold_ops @BeckDistribution_strength.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ dec F ∘ map F (dec G) =
map (F ∘ G) (σ) ∘ map F (dec G) ∘ map F (σ) ∘ dec F
    #[local] Set Keyed Unification.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ dec F ∘ map F (dec G) =
map (F ∘ G) (σ) ∘ map F (dec G) ∘ map F (σ) ∘ dec F
    rewrite (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ dec F ∘ map F (dec G) =
map F (map G (σ) ∘ dec G) ∘ map F (σ) ∘ dec F
    rewrite (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ dec F ∘ map F (dec G) =
map F (map G (σ) ∘ dec G ∘ σ) ∘ dec F
    #[local] Unset Keyed Unification.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ dec F ∘ map F (dec G) =
map F (map G (σ) ∘ dec G ∘ σ) ∘ dec F
    reassociate -> on left.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ (dec F ∘ map F (dec G)) =
map F (map G (σ) ∘ dec G ∘ σ) ∘ dec F rewrite <- (natural (ϕ := @dec W F _)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ (map (F ○ prod W) (dec G) ∘ dec F) =
map F (map G (σ) ∘ dec G ∘ σ) ∘ dec F
    unfold_ops @Map_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ (map F (map (prod W) (dec G)) ∘ dec F) =
map F (map G (σ) ∘ dec G ∘ σ) ∘ dec F reassociate <- on left.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ) ∘ map F (map (prod W) (dec G)) ∘ dec F =
map F (map G (σ) ∘ dec G ∘ σ) ∘ dec F
    rewrite (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ ∘ map (prod W) (dec G)) ∘ dec F =
map F (map G (σ) ∘ dec G ∘ σ) ∘ dec F fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (σ ∘ map (prod W) (dec G)) =
map F (map G (σ) ∘ dec G ∘ σ) fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
σ ∘ map (prod W) (dec G) = map G (σ) ∘ dec G ∘ σ
    unfold compose; ext [w x]; cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
w: W
x: G A
map G (pair (id w)) (dec G x) =
map G (σ) (dec G (map G (pair w) x))
    compose near x.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
w: W
x: G A
(map G (pair (id w)) ∘ dec G) x =
map G (σ) ((dec G ∘ map G (pair w)) x) rewrite <- (natural (ϕ := @dec W G _)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
w: W
x: G A
(map G (pair (id w)) ∘ dec G) x =
map G (σ) ((map (G ○ prod W) (pair w) ∘ dec G) x)
    unfold_ops @Map_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
w: W
x: G A
(map G (pair (id w)) ∘ dec G) x =
map G (σ) ((map G (map (prod W) (pair w)) ∘ dec G) x) compose near x on right.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
w: W
x: G A
(map G (pair (id w)) ∘ dec G) x =
(map G (σ) ∘ (map G (map (prod W) (pair w)) ∘ dec G))
  x
    reassociate <- on right.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
w: W
x: G A
(map G (pair (id w)) ∘ dec G) x =
(map G (σ) ∘ map G (map (prod W) (pair w)) ∘ dec G) x rewrite (fun_map_map (F := G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
w: W
x: G A
(map G (pair (id w)) ∘ dec G) x =
(map G (σ ∘ map (prod W) (pair w)) ∘ dec G) x
    unfold strength, compose, id.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
w: W
x: G A
map G (pair w) (dec G x) =
map G
  (fun a : W * A =>
   let
   '(a0, t) := map (prod W) (pair w) a in
    map (prod W) (pair a0) t) (dec G x) fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
w: W
x: G A
pair w =
(fun a : W * A =>
 let
 '(a0, t) := map (prod W) (pair w) a in
  map (prod W) (pair a0) t)
    now ext [? ?].
  Qed.

  (** Re-arrange using naturality *)
  Lemma dec_dec_compose_5: forall (A: Type),
      map F (map G (join (prod W))) ∘
        map F σ ∘ dec F ∘ map F (dec G) ∘
        (map F (map G (join (prod W))) ∘ map F strength) ∘
        dec F ∘ map F (dec G) =
        map F
          (map G (join (prod W)) ∘
             map G (map (prod W ∘ prod W) (join (prod W))) ∘ strength)
          ∘ dec F ∘ map F (dec G) ∘
          map F σ ∘ dec F ∘ map F (dec G (A := A)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
forall A : Type,
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
∘ (map F (map G (μ (prod W))) ∘ map F (σ)) ∘ dec F
∘ map F (dec G) =
map F
  (map G (μ (prod W))
   ∘ map G (map (prod W ∘ prod W) (μ (prod W))) ∘ 
   σ) ∘ dec F ∘ map F (dec G) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
forall A : Type,
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
∘ (map F (map G (μ (prod W))) ∘ map F (σ)) ∘ dec F
∘ map F (dec G) =
map F
  (map G (μ (prod W))
   ∘ map G (map (prod W ∘ prod W) (μ (prod W))) ∘ 
   σ) ∘ dec F ∘ map F (dec G) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
∘ (map F (map G (μ (prod W))) ∘ map F (σ)) ∘ dec F
∘ map F (dec G) =
map F
  (map G (μ (prod W))
   ∘ map G (map (prod W ∘ prod W) (μ (prod W))) ∘ 
   σ) ∘ dec F ∘ map F (dec G) ∘ map F (σ) ∘ dec F
∘ map F (dec G) fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
∘ (map F (map G (μ (prod W))) ∘ map F (σ)) ∘ dec F =
map F
  (map G (μ (prod W))
   ∘ map G (map (prod W ∘ prod W) (μ (prod W))) ∘ 
   σ) ∘ dec F ∘ map F (dec G) ∘ map F (σ) ∘ dec F fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
∘ (map F (map G (μ (prod W))) ∘ map F (σ)) =
map F
  (map G (μ (prod W))
   ∘ map G (map (prod W ∘ prod W) (μ (prod W))) ∘ 
   σ) ∘ dec F ∘ map F (dec G) ∘ map F (σ) reassociate <-.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W)))
∘ map F (σ) =
map F
  (map G (μ (prod W))
   ∘ map G (map (prod W ∘ prod W) (μ (prod W))) ∘ 
   σ) ∘ dec F ∘ map F (dec G) ∘ map F (σ)
    unfold_ops @Map_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W)))
∘ map F (σ) =
map F
  (map G (μ (prod W))
   ∘ map G (map (prod W) (map (prod W) (μ (prod W))))
   ∘ σ) ∘ dec F ∘ map F (dec G) ∘ map F (σ)
    change (map G (map (prod W) (map (prod W) (join (A:=?A) (prod W)))))
      with (map (G ○ prod W) (map (prod W) (join (A:=A) (prod W)))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W)))
∘ map F (σ) =
map F
  (map G (μ (prod W))
   ∘ map (G ○ prod W) (map (prod W) (μ (prod W))) ∘ 
   σ) ∘ dec F ∘ map F (dec G) ∘ map F (σ)
    reassociate -> near strength.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W)))
∘ map F (σ) =
map F
  (map G (μ (prod W))
   ∘ (map (G ○ prod W) (map (prod W) (μ (prod W))) ∘ σ))
∘ dec F ∘ map F (dec G) ∘ map F (σ)
    rewrite (natural (ϕ := @strength G _ W)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W)))
∘ map F (σ) =
map F
  (map G (μ (prod W))
   ∘ (σ ∘ map (prod W ○ G) (map (prod W) (μ (prod W)))))
∘ dec F ∘ map F (dec G) ∘ map F (σ)
    rewrite <- (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W)))
∘ map F (σ) =
map F (map G (μ (prod W)))
∘ map F
    (σ ∘ map (prod W ○ G) (map (prod W) (μ (prod W))))
∘ dec F ∘ map F (dec G) ∘ map F (σ)
    rewrite <- (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W)))
∘ map F (σ) =
map F (map G (μ (prod W)))
∘ (map F (σ)
   ∘ map F
       (map (prod W ○ G) (map (prod W) (μ (prod W)))))
∘ dec F ∘ map F (dec G) ∘ map F (σ)
    reassociate -> near (@dec W F H2 (G (W * (prod W ∘ prod W) A))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W)))
∘ map F (σ) =
map F (map G (μ (prod W)))
∘ (map F (σ)
   ∘ map F
       (map (prod W ○ G) (map (prod W) (μ (prod W))))
   ∘ dec F) ∘ map F (dec G) ∘ map F (σ)
    change (map F (map (prod W ○ G) (map (prod W) (join (A:=?A) (prod W)))))
      with (map (F ○ prod W) (map G (map (prod W) (join (A:=A) (prod W))))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W)))
∘ map F (σ) =
map F (map G (μ (prod W)))
∘ (map F (σ)
   ∘ map (F ○ prod W)
       (map G (map (prod W) (μ (prod W)))) ∘ dec F)
∘ map F (dec G) ∘ map F (σ)
    reassociate -> near (dec F).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ (map F (σ) ∘ dec F)
∘ map F (dec G) ∘ map F (map G (μ (prod W)))
∘ map F (σ) =
map F (map G (μ (prod W)))
∘ (map F (σ)
   ∘ (map (F ○ prod W)
        (map G (map (prod W) (μ (prod W)))) ∘ dec F))
∘ map F (dec G) ∘ map F (σ)
    rewrite (natural (ϕ := @dec W F _)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ (map F (σ) ∘ dec F)
∘ map F (dec G) ∘ map F (map G (μ (prod W)))
∘ map F (σ) =
map F (map G (μ (prod W)))
∘ (map F (σ)
   ∘ (dec F
      ∘ map F (map G (map (prod W) (μ (prod W))))))
∘ map F (dec G) ∘ map F (σ) fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ (map F (σ) ∘ dec F)
∘ map F (dec G) ∘ map F (map G (μ (prod W))) =
map F (map G (μ (prod W)))
∘ (map F (σ)
   ∘ (dec F
      ∘ map F (map G (map (prod W) (μ (prod W))))))
∘ map F (dec G)
    do 3 reassociate <-.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W))) =
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (map G (map (prod W) (μ (prod W))))
∘ map F (dec G)
    reassociate -> on right.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W))) =
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ (map F (map G (map (prod W) (μ (prod W))))
   ∘ map F (dec G))
    rewrite (fun_map_map (F := F) _ _ _ (@dec W G _ (W * (W * A)))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W))) =
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (map G (map (prod W) (μ (prod W))) ∘ dec G)
    change (map G (map (prod W) (join (A:=?A) (prod W))))
      with (map (G ∘ prod W) (join (A:=A) (prod W))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W))) =
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (map (G ∘ prod W) (μ (prod W)) ∘ dec G)
    rewrite (natural (ϕ := @dec W G _)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W))) =
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G ∘ map G (μ (prod W)))
    rewrite <- (fun_map_map (F := F)) at 1.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (μ (prod W))) =
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ (map F (dec G) ∘ map F (map G (μ (prod W))))
    reflexivity.
  Qed.

  #[local] Set Keyed Unification.
  Theorem dec_dec_compose {A}:
    dec (F ∘ G) ∘ dec (F ∘ G) =
    map (F ∘ G) (cojoin (W := prod W)) ∘ dec (F ∘ G) (A:=A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
dec (F ∘ G) ∘ dec (F ∘ G) =
map (F ∘ G) cojoin ∘ dec (F ∘ G)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
dec (F ∘ G) ∘ dec (F ∘ G) =
map (F ∘ G) cojoin ∘ dec (F ∘ G)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
dec (F ∘ G) ∘ dec (F ∘ G) =
map (F ∘ G) cojoin ∘ dec (F ∘ G) unfold_ops @Map_compose @Decorate_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F (map G cojoin)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G))
    (* Rewrite the RHS with the butterfly law *)
    do 2 reassociate <- on right.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F (map G cojoin) ∘ map F (shift G) ∘ dec F
∘ map F (dec G) rewrite (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F (map G cojoin ∘ shift G) ∘ dec F ∘ map F (dec G)
    unfold shift at 3.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F (map G cojoin ∘ (map G (uncurry incr) ∘ σ))
∘ dec F ∘ map F (dec G)
    reassociate <- on right.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F (map G cojoin ∘ map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) rewrite (fun_map_map (F := G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F (map G (cojoin ∘ uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G)
    rewrite incr_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F (map G (cojoin ∘ μ (prod W)) ∘ σ) ∘ dec F
∘ map F (dec G)
    rewrite (Writer.bimonad_butterfly).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W))
      ∘ cojoin ∘ map (prod W) cojoin) ∘ σ) ∘ dec F
∘ map F (dec G)
    (* Rewrite the outer (prod W) wire with the <<dfun_dec_dec>> law *)
    rewrite <- (fun_map_map (F := G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W))
      ∘ cojoin) ∘ map G (map (prod W) cojoin) ∘ σ)
∘ dec F ∘ map F (dec G)
    change (map ?F (map ?G ?f)) with (map (F ∘ G) f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W))
      ∘ cojoin) ∘ map (G ∘ prod W) cojoin ∘ σ) ∘ dec F
∘ map F (dec G)
    reassociate -> near (strength (F := G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W))
      ∘ cojoin) ∘ (map (G ∘ prod W) cojoin ∘ σ))
∘ dec F ∘ map F (dec G) rewrite <- (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W))
      ∘ cojoin)) ∘ map F (map (G ∘ prod W) cojoin ∘ σ)
∘ dec F ∘ map F (dec G)
    change (?f ∘ map F (map (G ∘ prod W) cojoin ∘ strength (F := G)) ∘ dec F ∘ map F (dec G))
      with (f ∘ (map F (map (G ∘ prod W) cojoin ∘ strength (F := G)) ∘ dec F ∘ map F (dec G))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W))
      ∘ cojoin))
∘ (map F (map (G ∘ prod W) cojoin ∘ σ) ∘ dec F
   ∘ map F (dec G))
    rewrite dec_dec_compose_1.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W))
      ∘ cojoin))
∘ (map F (σ) ∘ dec F ∘ map F (dec G ∘ dec G))
    (* Rewrite the outer (prod W) wire with the <<dfun_dec_dec>> law *)
    do 2 reassociate <- on right.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W))
      ∘ cojoin)) ∘ map F (σ) ∘ dec F
∘ map F (dec G ∘ dec G) rewrite (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W))
      ∘ cojoin) ∘ σ) ∘ dec F ∘ map F (dec G ∘ dec G)
    rewrite <- (fun_map_map (F := G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W)))
   ∘ map G cojoin ∘ σ) ∘ dec F ∘ map F (dec G ∘ dec G) reassociate -> near strength.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W)))
   ∘ (map G cojoin ∘ σ)) ∘ dec F
∘ map F (dec G ∘ dec G)
    rewrite <- (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W))))
∘ map F (map G cojoin ∘ σ) ∘ dec F
∘ map F (dec G ∘ dec G) reassociate -> near (dec F).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W))))
∘ (map F (map G cojoin ∘ σ) ∘ dec F)
∘ map F (dec G ∘ dec G)
    rewrite dec_dec_compose_2.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W))))
∘ (map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F)
∘ map F (dec G ∘ dec G)
    repeat change (map ?F (map ?G ?f)) with (map (F ∘ G) f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map (F ∘ G)
  (map (prod W) (μ (prod W)) ∘ μ (prod W)
   ∘ map (prod W) (bdist (prod W) (prod W)))
∘ (map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F)
∘ map F (dec G ∘ dec G)
    (* Slide a decoration on <<F>> and one on <<G>> past each other *)
    rewrite <- (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map (F ∘ G)
  (map (prod W) (μ (prod W)) ∘ μ (prod W)
   ∘ map (prod W) (bdist (prod W) (prod W)))
∘ (map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F)
∘ (map F (dec G) ∘ map F (dec G)) do 4 reassociate <- on right.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) =
map (F ∘ G)
  (map (prod W) (μ (prod W)) ∘ μ (prod W)
   ∘ map (prod W) (bdist (prod W) (prod W)))
∘ map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (dec G)
    do 2 reassociate <- on left.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (shift G) ∘ dec F ∘ map F (dec G) =
map (F ∘ G)
  (map (prod W) (μ (prod W)) ∘ μ (prod W)
   ∘ map (prod W) (bdist (prod W) (prod W)))
∘ map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (dec G)
    rewrite <- (fun_map_map (F := F ∘ G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (shift G) ∘ dec F ∘ map F (dec G) =
map (F ∘ G) (map (prod W) (μ (prod W)) ∘ μ (prod W))
∘ map (F ∘ G) (map (prod W) (bdist (prod W) (prod W)))
∘ map F (σ) ∘ dec F ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (dec G)
    change (?f ∘ map F strength
             ∘ dec F
             ∘ map F (dec G)
             ∘ ?g) with
        (f ∘ (map F strength
                   ∘ dec F
                   ∘ map F (dec G))
           ∘ g).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (shift G) ∘ dec F ∘ map F (dec G) =
map (F ∘ G) (map (prod W) (μ (prod W)) ∘ μ (prod W))
∘ map (F ∘ G) (map (prod W) (bdist (prod W) (prod W)))
∘ map F (σ) ∘ dec F
∘ (map F (σ) ∘ dec F ∘ map F (dec G)) ∘ map F (dec G)
    rewrite dec_dec_compose_3.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (shift G) ∘ dec F ∘ map F (dec G) =
map (F ∘ G) (map (prod W) (μ (prod W)) ∘ μ (prod W))
∘ map (F ∘ G) (map (prod W) (bdist (prod W) (prod W)))
∘ map F (σ) ∘ dec F
∘ (map (F ∘ G) (bdist (prod W) (prod W))
   ∘ map F (dec G) ∘ map F (σ) ∘ dec F)
∘ map F (dec G)
    (* Flatten out a distribution bubble.  Move the second decoration
       on <<F>> out of the way to juxtapose the two distributions. *)
    rewrite (fun_map_map (F := F ∘ G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G)
∘ map F (shift G) ∘ dec F ∘ map F (dec G) =
map (F ∘ G)
  (map (prod W) (μ (prod W)) ∘ μ (prod W)
   ∘ map (prod W) (bdist (prod W) (prod W)))
∘ map F (σ) ∘ dec F
∘ (map (F ∘ G) (bdist (prod W) (prod W))
   ∘ map F (dec G) ∘ map F (σ) ∘ dec F)
∘ map F (dec G) unfold shift.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map (F ∘ G)
  (map (prod W) (μ (prod W)) ∘ μ (prod W)
   ∘ map (prod W) (bdist (prod W) (prod W)))
∘ map F (σ) ∘ dec F
∘ (map (F ∘ G) (bdist (prod W) (prod W))
   ∘ map F (dec G) ∘ map F (σ) ∘ dec F)
∘ map F (dec G)
    rewrite (fun_map_map (F := F) _ _ _(@strength G _ W (W * (W * (W * A))))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G
     (map (prod W) (μ (prod W)) ∘ μ (prod W)
      ∘ map (prod W) (bdist (prod W) (prod W))) ∘ 
   σ) ∘ dec F
∘ (map (F ∘ G) (bdist (prod W) (prod W))
   ∘ map F (dec G) ∘ map F (σ) ∘ dec F)
∘ map F (dec G)
    rewrite <- (fun_map_map (F := G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W))
   ∘ map G (map (prod W) (bdist (prod W) (prod W)))
   ∘ σ) ∘ dec F
∘ (map (F ∘ G) (bdist (prod W) (prod W))
   ∘ map F (dec G) ∘ map F (σ) ∘ dec F)
∘ map F (dec G)
    change (map G (map (prod W) (bdist (prod W) (prod W))))
      with (map (G ○ prod W) (bdist (A := W * A) (prod W) (prod W))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W))
   ∘ map (G ○ prod W) (bdist (prod W) (prod W)) ∘ 
   σ) ∘ dec F
∘ (map (F ∘ G) (bdist (prod W) (prod W))
   ∘ map F (dec G) ∘ map F (σ) ∘ dec F)
∘ map F (dec G)
    reassociate -> near (@strength G _ W _).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W))
   ∘ (map (G ○ prod W) (bdist (prod W) (prod W)) ∘ σ))
∘ dec F
∘ (map (F ∘ G) (bdist (prod W) (prod W))
   ∘ map F (dec G) ∘ map F (σ) ∘ dec F)
∘ map F (dec G)
    rewrite (natural (ϕ := @strength G _ W)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W))
   ∘ (σ ∘ map (prod W ○ G) (bdist (prod W) (prod W))))
∘ dec F
∘ (map (F ∘ G) (bdist (prod W) (prod W))
   ∘ map F (dec G) ∘ map F (σ) ∘ dec F)
∘ map F (dec G)
    do 4 reassociate <-.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W)) ∘ σ
   ∘ map (prod W ○ G) (bdist (prod W) (prod W)))
∘ dec F ∘ map (F ∘ G) (bdist (prod W) (prod W))
∘ map F (dec G) ∘ map F (σ) ∘ dec F ∘ map F (dec G)
    rewrite <- (fun_map_map (F := F) _ _ _ (map (prod W ○ G) (bdist (prod W) (prod W)))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W)) ∘ σ)
∘ map F (map (prod W ○ G) (bdist (prod W) (prod W)))
∘ dec F ∘ map (F ∘ G) (bdist (prod W) (prod W))
∘ map F (dec G) ∘ map F (σ) ∘ dec F ∘ map F (dec G)
    change (map F (map (prod W ○ G) (bdist (A:=?A) (prod W) (prod W))))
      with (map (F ∘ prod W) (map G (bdist (A:=A) (prod W) (prod W)))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W)) ∘ σ)
∘ map (F ∘ prod W) (map G (bdist (prod W) (prod W)))
∘ dec F ∘ map (F ∘ G) (bdist (prod W) (prod W))
∘ map F (dec G) ∘ map F (σ) ∘ dec F ∘ map F (dec G)
    reassociate -> near (dec F (A := (G (W * (W * (W * A)))))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W)) ∘ σ)
∘ (map (F ∘ prod W) (map G (bdist (prod W) (prod W)))
   ∘ dec F) ∘ map (F ∘ G) (bdist (prod W) (prod W))
∘ map F (dec G) ∘ map F (σ) ∘ dec F ∘ map F (dec G)
    rewrite (natural (ϕ := @dec W F _)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W)) ∘ σ)
∘ (dec F ∘ map F (map G (bdist (prod W) (prod W))))
∘ map (F ∘ G) (bdist (prod W) (prod W))
∘ map F (dec G) ∘ map F (σ) ∘ dec F ∘ map F (dec G)
    reassociate <-.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W)) ∘ σ)
∘ dec F ∘ map F (map G (bdist (prod W) (prod W)))
∘ map (F ∘ G) (bdist (prod W) (prod W))
∘ map F (dec G) ∘ map F (σ) ∘ dec F ∘ map F (dec G)
    change (map F (map G (bdist (A:=?A) (prod W) (prod W))))
      with (map (F ∘ G) (bdist (A:=A) (prod W) (prod W))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W)) ∘ σ)
∘ dec F ∘ map (F ∘ G) (bdist (prod W) (prod W))
∘ map (F ∘ G) (bdist (prod W) (prod W))
∘ map F (dec G) ∘ map F (σ) ∘ dec F ∘ map F (dec G)
    reassociate -> near (map (F ∘ G) (bdist (prod W) (prod W))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W)) ∘ σ)
∘ dec F
∘ (map (F ∘ G) (bdist (prod W) (prod W))
   ∘ map (F ∘ G) (bdist (prod W) (prod W)))
∘ map F (dec G) ∘ map F (σ) ∘ dec F ∘ map F (dec G)
    rewrite (fun_map_map (F := F ∘ G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W)) ∘ σ)
∘ dec F
∘ map (F ∘ G)
    (bdist (prod W) (prod W) ∘ bdist (prod W) (prod W))
∘ map F (dec G) ∘ map F (σ) ∘ dec F ∘ map F (dec G)
    rewrite writer_dist_involution.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W)) ∘ σ)
∘ dec F ∘ map (F ∘ G) id ∘ map F (dec G) ∘ map F (σ)
∘ dec F ∘ map F (dec G)
    rewrite (fun_map_id (F := F ∘ G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W)) ∘ σ)
∘ dec F ∘ id ∘ map F (dec G) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
    change (?x ∘ id) with x.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (map (prod W) (μ (prod W)) ∘ μ (prod W)) ∘ σ)
∘ dec F ∘ map F (dec G) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
    (* final cleanup *)
    rewrite (natural (ϕ := @join (prod W) _)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G
     (μ (prod W) ∘ map (prod W ∘ prod W) (μ (prod W)))
   ∘ σ) ∘ dec F ∘ map F (dec G) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
    rewrite <- (fun_map_map (F := G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr) ∘ σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (μ (prod W))
   ∘ map G (map (prod W ∘ prod W) (μ (prod W))) ∘ 
   σ) ∘ dec F ∘ map F (dec G) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
    rewrite <- (fun_map_map (F := F)) at 1.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr)) ∘ map F (σ) ∘ dec F
∘ map F (dec G) ∘ map F (map G (uncurry incr) ∘ σ)
∘ dec F ∘ map F (dec G) =
map F
  (map G (μ (prod W))
   ∘ map G (map (prod W ∘ prod W) (μ (prod W))) ∘ 
   σ) ∘ dec F ∘ map F (dec G) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
    rewrite <- (fun_map_map (F := F)) at 1.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (uncurry incr)) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
∘ (map F (map G (uncurry incr)) ∘ map F (σ)) ∘ dec F
∘ map F (dec G) =
map F
  (map G (μ (prod W))
   ∘ map G (map (prod W ∘ prod W) (μ (prod W))) ∘ 
   σ) ∘ dec F ∘ map F (dec G) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
    do 2 rewrite incr_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G (μ (prod W))) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
∘ (map F (map G (μ (prod W))) ∘ map F (σ)) ∘ dec F
∘ map F (dec G) =
map F
  (map G (μ (prod W))
   ∘ map G (map (prod W ∘ prod W) (μ (prod W))) ∘ 
   σ) ∘ dec F ∘ map F (dec G) ∘ map F (σ) ∘ dec F
∘ map F (dec G)
    apply dec_dec_compose_5.
  Qed.
  #[local] Unset Keyed Unification.

  Theorem dec_extract_compose {A}:
    map (F ∘ G) (extract (W := (W ×))) ∘ dec (F ∘ G) = @id (F (G A)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map (F ∘ G) extract ∘ dec (F ∘ G) = id
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map (F ∘ G) extract ∘ dec (F ∘ G) = id
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map (F ∘ G) extract ∘ dec (F ∘ G) = id unfold_ops @Map_compose @Decorate_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G extract)
∘ (map F (shift G) ∘ dec F ∘ map F (dec G)) = id
    repeat reassociate <-.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G extract) ∘ map F (shift G) ∘ dec F
∘ map F (dec G) = id unfold_compose_in_compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G extract) ∘ map F (shift G) ∘ dec F
∘ map F (dec G) = id
    rewrite (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G extract ∘ shift G) ∘ dec F
∘ map F (dec G) = id
    rewrite (shift_extract G).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G extract ∘ extract) ∘ dec F
∘ map F (dec G) = id
    rewrite <- (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G extract) ∘ map F extract ∘ dec F
∘ map F (dec G) = id
    do 2 reassociate -> on left.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G extract)
∘ (map F extract ∘ (dec F ∘ map F (dec G))) = id
    reassociate <- near (map (A := W * G (W * A)) F (extract (W := (W ×)) (A := G (W * A)))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G extract)
∘ (map F extract ∘ dec F ∘ map F (dec G)) = id
    rewrite (dfun_dec_extract (E := W) (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G extract) ∘ (id ∘ map F (dec G)) = id
    change (id ∘ ?f) with f.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G extract) ∘ map F (dec G) = id
    rewrite (fun_map_map (F := F)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F (map G extract ∘ dec G) = id
    rewrite (dfun_dec_extract (E := W) (F := G)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
H0: Map F
G: Type -> Type
H1: Map G
H2: Decorate W F
H3: Decorate W G
DecoratedFunctor0: DecoratedFunctor W F
DecoratedFunctor1: DecoratedFunctor W G
A: Type
map F id = id
    now rewrite (fun_map_id (F := F)).
  Qed.

  #[global] Instance DecoratedFunctor_compose: DecoratedFunctor W (F ∘ G) :=
    {| dfun_dec_natural := Natural_dec_compose;
       dfun_dec_dec := @dec_dec_compose;
       dfun_dec_extract := @dec_extract_compose;
    |}.

End Decoratedfunctor_composition.

(** ** Category Laws for Composition of Decorated Functors *)
(** Next we prove that composition of decorated functors satisfies the
    laws of a category, i.e. that composition with the identity
    decorated functor on the left or is the identity, and that
    composition is associative. This is not immediately obvious
    because in each case we must verify that the <<dec>> operation is
    the same for both sides. *)
(**********************************************************************)
Section DecoratedFunctor_composition_laws.

  Section identity_laws.

    (** Let <<T>> be a decorated functor. *)
    Context
      `{Functor T}
      `{dec_T: Decorate W T}
      `{op: Monoid_op W}
      `{unit: Monoid_unit W}
      `{! DecoratedFunctor W T}
      `{! Monoid W}.

    (** *** Composition with a zero-decorated functor *)
    (** When <<F>> has a trivial decoration,
        <<dec (F ∘T)>> and <<dec (T ∘ F)>> have a special form. *)
    (******************************************************************)
    Section zero_decorated_composition.

      (** Let <<F>> be a functor, which we will treat as zero-decorated. *)
      Context
        (F: Type -> Type)
        `{Functor F}.

      (** Composition with a zero-decorated functor on the left returns <<T>>. *)
      Theorem decorate_zero_compose_l: forall (A: Type),
          @dec W (F ∘ T) (@Decorate_compose W op F _ T _ Decorate_zero dec_T) A =
          map F (dec T).
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
forall A : Type, dec (F ∘ T) = map F (dec T)
      Proof.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
forall A : Type, dec (F ∘ T) = map F (dec T)
        intros.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
dec (F ∘ T) = map F (dec T) unfold_ops @Decorate_compose.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map F (shift T) ∘ dec F ∘ map F (dec T) =
map F (dec T) unfold_ops @Decorate_zero.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map F (shift T) ∘ map F (pair Ƶ) ∘ map F (dec T) =
map F (dec T)
        do 2 rewrite (fun_map_map (F := F)).
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map F (shift T ∘ pair Ƶ ∘ dec T) = map F (dec T)
        fequal.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
shift T ∘ pair Ƶ ∘ dec T = dec T unfold shift.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (uncurry incr) ∘ σ ∘ pair Ƶ ∘ dec T = dec T
        reassociate -> near (pair Ƶ).
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (uncurry incr) ∘ (σ ∘ pair Ƶ) ∘ dec T = dec T rewrite strength_2.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (uncurry incr) ∘ map T (pair Ƶ) ∘ dec T = dec T
        rewrite (fun_map_map (F := T)).
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (uncurry incr ∘ pair Ƶ) ∘ dec T = dec T
        change (pair Ƶ) with (ret (W ×) (W * A)).
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (uncurry incr ∘ η (prod W) (W * A)) ∘ dec T =
dec T
        rewrite incr_spec.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (μ (prod W) ∘ η (prod W) (W * A)) ∘ dec T =
dec T
        rewrite (mon_join_ret (T := prod W)).
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T id ∘ dec T = dec T
        now rewrite (fun_map_id (F := T)).
      Qed.

      (** Composition with the identity functor on the left returns <<T>>. *)
      Theorem decorate_zero_compose_r: forall (A: Type),
          @dec W (T ∘ F) (@Decorate_compose W op T _ F _ dec_T Decorate_zero) A =
          map T σ ∘ dec T.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
forall A : Type, dec (T ∘ F) = map T (σ) ∘ dec T
      Proof.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
forall A : Type, dec (T ∘ F) = map T (σ) ∘ dec T
        intros.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
dec (T ∘ F) = map T (σ) ∘ dec T unfold_ops @Decorate_compose.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (shift F) ∘ dec T ∘ map T (dec F) =
map T (σ) ∘ dec T unfold_ops @Decorate_zero.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (shift F) ∘ dec T ∘ map T (map F (pair Ƶ)) =
map T (σ) ∘ dec T
        reassociate -> on left.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (shift F) ∘ (dec T ∘ map T (map F (pair Ƶ))) =
map T (σ) ∘ dec T
        rewrite <- (natural (ϕ := @dec W T _)).
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (shift F)
∘ (map (T ○ prod W) (map F (pair Ƶ)) ∘ dec T) =
map T (σ) ∘ dec T
        reassociate <-.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (shift F) ∘ map (T ○ prod W) (map F (pair Ƶ))
∘ dec T = map T (σ) ∘ dec T fequal.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (shift F) ∘ map (T ○ prod W) (map F (pair Ƶ)) =
map T (σ) unfold_ops @Map_compose.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (shift F)
∘ map T (map (prod W) (map F (pair Ƶ))) = map T (σ)
        rewrite (fun_map_map (F := T)).
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
map T (shift F ∘ map (prod W) (map F (pair Ƶ))) =
map T (σ) fequal.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
shift F ∘ map (prod W) (map F (pair Ƶ)) = σ
        ext [w t]; unfold compose; cbn.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
w: W
t: F A
shift F (id w, map F (pair Ƶ) t) = map F (pair w) t unfold id.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
w: W
t: F A
shift F (w, map F (pair Ƶ) t) = map F (pair w) t
        rewrite (shift_spec F).
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
w: W
t: F A
map F (map_fst (fun m : W => w ● m))
  (map F (pair Ƶ) t) = map F (pair w) t compose near t on left.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
w: W
t: F A
(map F (map_fst (fun m : W => w ● m)) ∘ map F (pair Ƶ))
  t = map F (pair w) t
        rewrite (fun_map_map (F := F)).
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
w: W
t: F A
map F (map_fst (fun m : W => w ● m) ∘ pair Ƶ) t =
map F (pair w) t fequal.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
w: W
t: F A
map_fst (fun m : W => w ● m) ∘ pair Ƶ = pair w ext a; cbn.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
F: Type -> Type
Map_F0: Map F
H0: Functor F
A: Type
w: W
t: F A
a: A
(w ● Ƶ, id a) = (w, a)
        now simpl_monoid.
      Qed.

    End zero_decorated_composition.

    (** *** Composition with the identity decorated functor *)
    (******************************************************************)
    Theorem decorate_identity_compose_l: forall (A: Type),
        @dec W ((fun A => A) ∘ T) (@Decorate_compose W op (fun A => A) _ T _ Decorate_zero dec_T) A =
        dec T.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
forall A : Type,
dec ((fun A0 : Type => A0) ∘ T) = dec T
    Proof.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
forall A : Type,
dec ((fun A0 : Type => A0) ∘ T) = dec T
      intros.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
A: Type
dec ((fun A : Type => A) ∘ T) = dec T now rewrite (decorate_zero_compose_l (fun A => A)).
    Qed.

    Theorem decorate_identity_compose_r: forall (A: Type),
        @dec W (T ∘ (fun A => A)) (@Decorate_compose W op T _ (fun A => A) _ dec_T Decorate_zero) A =
        dec T.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
forall A : Type,
dec (T ∘ (fun A0 : Type => A0)) = dec T
    Proof.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
forall A : Type,
dec (T ∘ (fun A0 : Type => A0)) = dec T
      intros.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
A: Type
dec (T ∘ (fun A : Type => A)) = dec T rewrite (decorate_zero_compose_r (fun A => A)).
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
A: Type
map T (σ) ∘ dec T = dec T
      rewrite strength_I.
T: Type -> Type
Map_F: Map T
H: Functor T
W: Type
dec_T: Decorate W T
op: Monoid_op W
unit: Monoid_unit W
DecoratedFunctor0: DecoratedFunctor W T
Monoid0: Monoid W
A: Type
map T id ∘ dec T = dec T now rewrite (fun_map_id (F := T)).
    Qed.

  End identity_laws.

  Section associativity_law.

    Context
      `{op: Monoid_op W}
      `{unit: Monoid_unit W}
      `{! Monoid W}
      `{Map T1} `{Map T2} `{Map T3}
      `{dec_T1: Decorate W T1}
      `{dec_T2: Decorate W T2}
      `{dec_T3: Decorate W T3}
      `{! DecoratedFunctor W T1}
      `{! DecoratedFunctor W T2}
      `{! DecoratedFunctor W T3}.

    Lemma decorate_compose_assoc1: forall (A: Type),
        (map T2 (map T1 (μ (A:=A) (prod W)) ∘ σ ∘ μ (prod W)) ∘ σ) =
        (map T2 (map T1 (μ (W ×)) ∘ σ) ∘ σ) ∘ map ((W ×) ∘ T2) (map T1 (μ (W ×)) ∘ σ).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
forall A : Type,
map T2 (map T1 (μ (prod W)) ∘ σ ∘ μ (prod W)) ∘ σ =
map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ)
    Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
forall A : Type,
map T2 (map T1 (μ (prod W)) ∘ σ ∘ μ (prod W)) ∘ σ =
map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ)
      intros.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T2 (map T1 (μ (prod W)) ∘ σ ∘ μ (prod W)) ∘ σ =
map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ) ext [w1 t].
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
(map T2 (map T1 (μ (prod W)) ∘ σ ∘ μ (prod W)) ∘ σ)
  (w1, t) =
(map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
 ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ))
  (w1, t) unfold compose; cbn.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
map T2
  (fun a : W * (W * T1 (W * A)) =>
   map T1 (μ (prod W)) (σ (μ (prod W) a)))
  (map T2 (pair w1) t) =
map T2 (map T1 (μ (prod W)) ○ σ)
  (map T2 (pair (id w1))
     (map T2 (map T1 (μ (prod W)) ○ σ) t))
      compose near t.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
(map T2
   (fun a : W * (W * T1 (W * A)) =>
    map T1 (μ (prod W)) (σ (μ (prod W) a)))
 ∘ map T2 (pair w1)) t =
map T2 (map T1 (μ (prod W)) ○ σ)
  ((map T2 (pair (id w1))
    ∘ map T2 (map T1 (μ (prod W)) ○ σ)) t) unfold id.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
(map T2
   (fun a : W * (W * T1 (W * A)) =>
    map T1 (μ (prod W)) (σ (μ (prod W) a)))
 ∘ map T2 (pair w1)) t =
map T2 (map T1 (μ (prod W)) ○ σ)
  ((map T2 (pair w1)
    ∘ map T2 (map T1 (μ (prod W)) ○ σ)) t)
      rewrite 2(fun_map_map (F := T2)).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
map T2
  ((fun a : W * (W * T1 (W * A)) =>
    map T1 (μ (prod W)) (σ (μ (prod W) a))) ∘ pair w1)
  t =
map T2 (map T1 (μ (prod W)) ○ σ)
  (map T2 (pair w1 ∘ (map T1 (μ (prod W)) ○ σ)) t)
      compose near t on right.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
map T2
  ((fun a : W * (W * T1 (W * A)) =>
    map T1 (μ (prod W)) (σ (μ (prod W) a))) ∘ pair w1)
  t =
(map T2 (map T1 (μ (prod W)) ○ σ)
 ∘ map T2 (pair w1 ∘ (map T1 (μ (prod W)) ○ σ))) t
      rewrite (fun_map_map (F := T2)).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
map T2
  ((fun a : W * (W * T1 (W * A)) =>
    map T1 (μ (prod W)) (σ (μ (prod W) a))) ∘ pair w1)
  t =
map T2
  (map T1 (μ (prod W)) ○ σ
   ∘ (pair w1 ∘ (map T1 (μ (prod W)) ○ σ))) t fequal.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
(fun a : W * (W * T1 (W * A)) =>
 map T1 (μ (prod W)) (σ (μ (prod W) a))) ∘ pair w1 =
map T1 (μ (prod W)) ○ σ
∘ (pair w1 ∘ (map T1 (μ (prod W)) ○ σ))
      ext [w2 t2].
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
w2: W
t2: T1 (W * A)
((fun a : W * (W * T1 (W * A)) =>
  map T1 (μ (prod W)) (σ (μ (prod W) a))) ∘ pair w1)
  (w2, t2) =
(map T1 (μ (prod W)) ○ σ
 ∘ (pair w1 ∘ (map T1 (μ (prod W)) ○ σ))) (w2, t2) unfold compose; cbn.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
w2: W
t2: T1 (W * A)
map T1 (μ (prod W)) (map T1 (pair (w1 ● w2)) (id t2)) =
map T1 (μ (prod W))
  (map T1 (pair w1)
     (map T1 (μ (prod W)) (map T1 (pair w2) t2))) unfold id.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
w2: W
t2: T1 (W * A)
map T1 (μ (prod W)) (map T1 (pair (w1 ● w2)) t2) =
map T1 (μ (prod W))
  (map T1 (pair w1)
     (map T1 (μ (prod W)) (map T1 (pair w2) t2)))
      compose near t2.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
w2: W
t2: T1 (W * A)
(map T1 (μ (prod W)) ∘ map T1 (pair (w1 ● w2))) t2 =
map T1 (μ (prod W))
  (map T1 (pair w1)
     ((map T1 (μ (prod W)) ∘ map T1 (pair w2)) t2)) rewrite 2(fun_map_map (F := T1)).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
w2: W
t2: T1 (W * A)
map T1 (μ (prod W) ∘ pair (w1 ● w2)) t2 =
map T1 (μ (prod W))
  (map T1 (pair w1) (map T1 (μ (prod W) ∘ pair w2) t2))
      do 2 (compose near t2 on right; rewrite 1(fun_map_map (F := T1))).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
w2: W
t2: T1 (W * A)
map T1 (μ (prod W) ∘ pair (w1 ● w2)) t2 =
map T1
  (μ (prod W) ∘ (pair w1 ∘ (μ (prod W) ∘ pair w2))) t2
      fequal.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
w2: W
t2: T1 (W * A)
μ (prod W) ∘ pair (w1 ● w2) =
μ (prod W) ∘ (pair w1 ∘ (μ (prod W) ∘ pair w2)) ext [w3 a].
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
w2: W
t2: T1 (W * A)
w3: W
a: A
(μ (prod W) ∘ pair (w1 ● w2)) (w3, a) =
(μ (prod W) ∘ (pair w1 ∘ (μ (prod W) ∘ pair w2)))
  (w3, a) cbn.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
w2: W
t2: T1 (W * A)
w3: W
a: A
((w1 ● w2) ● w3, id a) = (w1 ● (w2 ● w3), id (id a)) fequal.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
w1: W
t: T2 (W * T1 (W * A))
w2: W
t2: T1 (W * A)
w3: W
a: A
(w1 ● w2) ● w3 = w1 ● (w2 ● w3) now rewrite monoid_assoc.
    Qed.

    Set Keyed Unification.
    Theorem decorate_compose_assoc: forall (A: Type),
        @dec W (T3 ∘ T2 ∘ T1)
             (@Decorate_compose W op (T3 ∘ T2) _ T1 _ _ dec_T1) A =
        @dec W (T3 ∘ T2 ∘ T1)
             (@Decorate_compose W op T3 _ (T2 ∘ T1) _ dec_T3 _) A.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
forall A : Type,
dec (T3 ∘ T2 ∘ T1) = dec (T3 ∘ T2 ∘ T1)
    Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
forall A : Type,
dec (T3 ∘ T2 ∘ T1) = dec (T3 ∘ T2 ∘ T1)
      intros.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
dec (T3 ∘ T2 ∘ T1) = dec (T3 ∘ T2 ∘ T1) unfold_ops @Decorate_compose; unfold dec at 1 6.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map (T3 ∘ T2) (shift T1)
∘ (map T3 (shift T2) ∘ dec T3 ∘ map T3 (dec T2))
∘ map (T3 ∘ T2) (dec T1) =
map T3 (shift (T2 ∘ T1)) ∘ dec T3
∘ map T3
    (map T2 (shift T1) ∘ dec T2 ∘ map T2 (dec T1))
      do 2 reassociate <- on left.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map (T3 ∘ T2) (shift T1) ∘ map T3 (shift T2) ∘ dec T3
∘ map T3 (dec T2) ∘ map (T3 ∘ T2) (dec T1) =
map T3 (shift (T2 ∘ T1)) ∘ dec T3
∘ map T3
    (map T2 (shift T1) ∘ dec T2 ∘ map T2 (dec T1))
      rewrite (fun_map_map (F := T3)).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3 (map T2 (shift T1) ∘ shift T2) ∘ dec T3
∘ map T3 (dec T2) ∘ map (T3 ∘ T2) (dec T1) =
map T3 (shift (T2 ∘ T1)) ∘ dec T3
∘ map T3
    (map T2 (shift T1) ∘ dec T2 ∘ map T2 (dec T1))
      reassociate -> near (map (T3 ∘ T2) (dec T1));
        rewrite (fun_map_map (F := T3)).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3 (map T2 (shift T1) ∘ shift T2) ∘ dec T3
∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (shift (T2 ∘ T1)) ∘ dec T3
∘ map T3
    (map T2 (shift T1) ∘ dec T2 ∘ map T2 (dec T1))
      unfold shift at 1 2.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (uncurry incr) ∘ σ)
   ∘ (map T2 (uncurry incr) ∘ σ)) ∘ dec T3
∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (shift (T2 ∘ T1)) ∘ dec T3
∘ map T3
    (map T2 (shift T1) ∘ dec T2 ∘ map T2 (dec T1))
      reassociate <- on left.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (uncurry incr) ∘ σ)
   ∘ map T2 (uncurry incr) ∘ σ) ∘ dec T3
∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (shift (T2 ∘ T1)) ∘ dec T3
∘ map T3
    (map T2 (shift T1) ∘ dec T2 ∘ map T2 (dec T1))
      rewrite (fun_map_map (F := T2)).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (uncurry incr) ∘ σ ∘ uncurry incr)
   ∘ σ) ∘ dec T3 ∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (shift (T2 ∘ T1)) ∘ dec T3
∘ map T3
    (map T2 (shift T1) ∘ dec T2 ∘ map T2 (dec T1))
      repeat rewrite incr_spec.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ ∘ μ (prod W)) ∘ σ)
∘ dec T3 ∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (shift (T2 ∘ T1)) ∘ dec T3
∘ map T3
    (map T2 (shift T1) ∘ dec T2 ∘ map T2 (dec T1))
      rewrite decorate_compose_assoc1.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
   ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ))
∘ dec T3 ∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (shift (T2 ∘ T1)) ∘ dec T3
∘ map T3
    (map T2 (shift T1) ∘ dec T2 ∘ map T2 (dec T1))
      unfold shift at 1 2.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
   ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ))
∘ dec T3 ∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (map (T2 ∘ T1) (uncurry incr) ∘ σ) ∘ dec T3
∘ map T3
    (map T2 (map T1 (uncurry incr) ∘ σ) ∘ dec T2
     ∘ map T2 (dec T1))
      change (map T2 (map T1 (μ (A:=?A) (prod W)) ∘ σ) ∘ dec T2 ∘ map T2 (dec T1))
        with (map T2 (map T1 (μ (A:=A) (prod W)) ∘ σ) ∘ (dec T2 ∘ map T2 (dec T1))).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
   ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ))
∘ dec T3 ∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (map (T2 ∘ T1) (uncurry incr) ∘ σ) ∘ dec T3
∘ map T3
    (map T2 (map T1 (uncurry incr) ∘ σ) ∘ dec T2
     ∘ map T2 (dec T1))
      rewrite <- (fun_map_map (F := T3) _ _ _ (dec T2 ∘ map T2 (dec T1))).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
   ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ))
∘ dec T3 ∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (map (T2 ∘ T1) (uncurry incr) ∘ σ) ∘ dec T3
∘ (map T3
     (H0 (W * T1 (W * A)) (T1 (W * A))
        (map T1 (uncurry incr) ∘ σ))
   ∘ map T3 (dec T2 ∘ map T2 (dec T1)))
      change (H0 ?x ?y ?f) with (map T2 f).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
   ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ))
∘ dec T3 ∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (map (T2 ∘ T1) (uncurry incr) ∘ σ) ∘ dec T3
∘ (map T3 (map T2 (map T1 (uncurry incr) ∘ σ))
   ∘ map T3 (dec T2 ∘ map T2 (dec T1)))
      (* ^^ not sure why this guy got unfolded *)
      reassociate <- on right.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
   ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ))
∘ dec T3 ∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (map (T2 ∘ T1) (uncurry incr) ∘ σ) ∘ dec T3
∘ map T3 (map T2 (map T1 (uncurry incr) ∘ σ))
∘ map T3 (dec T2 ∘ map T2 (dec T1))
      repeat rewrite incr_spec.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
   ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ))
∘ dec T3 ∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (map (T2 ∘ T1) (μ (prod W)) ∘ σ) ∘ dec T3
∘ map T3 (map T2 (map T1 (μ (prod W)) ∘ σ))
∘ map T3 (dec T2 ∘ map T2 (dec T1))
      reassociate -> near (map T3 (map T2 (map T1 (μ (prod W)) ∘ σ))).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
   ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ))
∘ dec T3 ∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (map (T2 ∘ T1) (μ (prod W)) ∘ σ)
∘ (dec T3 ∘ map T3 (map T2 (map T1 (μ (prod W)) ∘ σ)))
∘ map T3 (dec T2 ∘ map T2 (dec T1))
      rewrite <- (natural (ϕ := @dec W T3 _)).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
   ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ))
∘ dec T3 ∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (map (T2 ∘ T1) (μ (prod W)) ∘ σ)
∘ (map (T3 ○ prod W)
     (map T2 (map T1 (μ (prod W)) ∘ σ)) ∘ dec T3)
∘ map T3 (dec T2 ∘ map T2 (dec T1))
      reassociate <- on right.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
   ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ))
∘ dec T3 ∘ map T3 (dec T2 ∘ map T2 (dec T1)) =
map T3 (map (T2 ∘ T1) (μ (prod W)) ∘ σ)
∘ map (T3 ○ prod W) (map T2 (map T1 (μ (prod W)) ∘ σ))
∘ dec T3 ∘ map T3 (dec T2 ∘ map T2 (dec T1)) fequal.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
   ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ))
∘ dec T3 =
map T3 (map (T2 ∘ T1) (μ (prod W)) ∘ σ)
∘ map (T3 ○ prod W) (map T2 (map T1 (μ (prod W)) ∘ σ))
∘ dec T3 fequal.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
   ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ)) =
map T3 (map (T2 ∘ T1) (μ (prod W)) ∘ σ)
∘ map (T3 ○ prod W) (map T2 (map T1 (μ (prod W)) ∘ σ))
      rewrite (fun_map_map (F := T3)).
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T3
  (map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
   ∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ)) =
map T3
  (map (T2 ∘ T1) (μ (prod W)) ∘ σ
   ∘ map (prod W) (map T2 (map T1 (μ (prod W)) ∘ σ))) fequal.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ) =
map (T2 ∘ T1) (μ (prod W)) ∘ σ
∘ map (prod W) (map T2 (map T1 (μ (prod W)) ∘ σ))
      rewrite strength_compose.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ) =
map (T2 ∘ T1) (μ (prod W)) ∘ (map T2 (σ) ∘ σ)
∘ map (prod W) (map T2 (map T1 (μ (prod W)) ∘ σ))
      reassociate <- on right.
W: Type
op: Monoid_op W
unit: Monoid_unit W
Monoid0: Monoid W
T1: Type -> Type
H: Map T1
T2: Type -> Type
H0: Map T2
T3: Type -> Type
H1: Map T3
dec_T1: Decorate W T1
dec_T2: Decorate W T2
dec_T3: Decorate W T3
DecoratedFunctor0: DecoratedFunctor W T1
DecoratedFunctor1: DecoratedFunctor W T2
DecoratedFunctor2: DecoratedFunctor W T3
A: Type
map T2 (map T1 (μ (prod W)) ∘ σ) ∘ σ
∘ map (prod W ∘ T2) (map T1 (μ (prod W)) ∘ σ) =
map (T2 ∘ T1) (μ (prod W)) ∘ map T2 (σ) ∘ σ
∘ map (prod W) (map T2 (map T1 (μ (prod W)) ∘ σ))
      now rewrite (fun_map_map (F := T2)).
    Qed.
    Unset Keyed Unification.

  End associativity_law.

End DecoratedFunctor_composition_laws.

(** ** Composition with Null-Decorated Functors *)
(**********************************************************************)
Section DecoratedFunctor_zero_composition.

  Context
    (F G: Type -> Type)
    `{Monoid W}
    `{Functor F}
    `{DecoratedFunctor W G}.

  Instance: Decorate W F := Decorate_zero.

  Theorem decorate_zero_compose {A}:
    `(dec (F ∘ G) (A := A) = map F (dec G)).
F, G: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
H1: Map G
H2: Decorate W G
H3: DecoratedFunctor W G
A: Type
dec (F ∘ G) = map F (dec G)
  Proof.
F, G: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
H1: Map G
H2: Decorate W G
H3: DecoratedFunctor W G
A: Type
dec (F ∘ G) = map F (dec G)
    intros.
F, G: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
H1: Map G
H2: Decorate W G
H3: DecoratedFunctor W G
A: Type
dec (F ∘ G) = map F (dec G) unfold_ops @Decorate_compose.
F, G: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
H1: Map G
H2: Decorate W G
H3: DecoratedFunctor W G
A: Type
map F (shift G) ∘ dec F ∘ map F (dec G) =
map F (dec G)
    unfold_ops @Decorate_instance_0 @Decorate_zero.
F, G: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
H1: Map G
H2: Decorate W G
H3: DecoratedFunctor W G
A: Type
map F (shift G) ∘ map F (pair Ƶ) ∘ map F (dec G) =
map F (dec G)
    reassociate -> near (map F (dec G)).
F, G: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
H1: Map G
H2: Decorate W G
H3: DecoratedFunctor W G
A: Type
map F (shift G) ∘ (map F (pair Ƶ) ∘ map F (dec G)) =
map F (dec G)
    do 2 rewrite (fun_map_map (F := F)).
F, G: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
H1: Map G
H2: Decorate W G
H3: DecoratedFunctor W G
A: Type
map F (shift G ∘ (pair Ƶ ∘ dec G)) = map F (dec G)
    reassociate <-.
F, G: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
H1: Map G
H2: Decorate W G
H3: DecoratedFunctor W G
A: Type
map F (shift G ∘ pair Ƶ ∘ dec G) = map F (dec G)
    replace (shift G ∘ (fun a: G (W * A) => (Ƶ, a))) with (@id (G (W * A))).
F, G: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
H1: Map G
H2: Decorate W G
H3: DecoratedFunctor W G
A: Type
map F (id ∘ dec G) = map F (dec G)
F, G: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
H1: Map G
H2: Decorate W G
H3: DecoratedFunctor W G
A: Type
id = shift G ∘ (fun a : G (W * A) => (Ƶ, a))
    now reflexivity.
F, G: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
H1: Map G
H2: Decorate W G
H3: DecoratedFunctor W G
A: Type
id = shift G ∘ (fun a : G (W * A) => (Ƶ, a))
    ext g.
F, G: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
H1: Map G
H2: Decorate W G
H3: DecoratedFunctor W G
A: Type
g: G (W * A)
id g = (shift G ∘ (fun a : G (W * A) => (Ƶ, a))) g unfold compose; cbn.
F, G: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
H1: Map G
H2: Decorate W G
H3: DecoratedFunctor W G
A: Type
g: G (W * A)
id g = shift G (Ƶ, g)
    now rewrite (shift_zero G).
  Qed.

End DecoratedFunctor_zero_composition.

(** * Monad Operations in As Homomorphisms of Decorated Functors *)
(**********************************************************************)
Section DecoratedMonad_characterization.

  Context
    `{Categorical.Monad.Monad T} `{Decorate W T} `{Monoid W}
    `{! Categorical.DecoratedFunctor.DecoratedFunctor W T}.

  (** <<ret T>> commutes with decoration if and only if <<dec T>> maps
     <<ret T>> to <<ret (T ∘ W)>> *)
  Lemma dec_ret_iff {A}:
    (dec T ∘ ret T A = ret T (W * A) ∘ dec (fun x => x) (A:=A)) <->
    (dec T ∘ ret T A = ret (T ∘ prod W) A).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
dec T ∘ η T A = η T (W * A) ∘ dec (fun x : Type => x) <->
dec T ∘ η T A = η (T ∘ prod W) A
  Proof with auto.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
dec T ∘ η T A = η T (W * A) ∘ dec (fun x : Type => x) <->
dec T ∘ η T A = η (T ∘ prod W) A
    split...
  Qed.

  (** <<join T>> commutes with decoration if and only if <<dec T>>
     maps <<join T>> to <<join (T ∘ prod W)>> of <<dec T ∘ map T (dec T)>>
     (in other words iff <<dec T>> commutes with <<join>>). *)
  Lemma dec_join_iff {A}:
    `(dec T ∘ join T = join T ∘ dec (T ∘ T) (A := A)) <->
    `(dec T ∘ join T = join (T ∘ prod W) ∘ dec T ∘ map T (dec T (A:=A))).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
dec T ∘ μ T = μ T ∘ dec (T ∘ T) <->
dec T ∘ μ T = μ (T ∘ prod W) ∘ dec T ∘ map T (dec T)
  Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
dec T ∘ μ T = μ T ∘ dec (T ∘ T) <->
dec T ∘ μ T = μ (T ∘ prod W) ∘ dec T ∘ map T (dec T)
    enough (Heq: join T ∘ dec (A := A) (T ∘ T)
                  = join (T ∘ prod W) ∘ dec T ∘ map T (dec T))
      by (split; intro hyp; now rewrite hyp).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
μ T ∘ dec (T ∘ T) =
μ (T ∘ prod W) ∘ dec T ∘ map T (dec T)
    unfold_ops @Join_Beck @Decorate_compose @BeckDistribution_strength.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
μ T ∘ (map T (shift T) ∘ dec T ∘ map T (dec T)) =
map T (μ (prod W)) ∘ μ T ∘ map T (σ) ∘ dec T
∘ map T (dec T)
    repeat reassociate <-.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
μ T ∘ map T (shift T) ∘ dec T ∘ map T (dec T) =
map T (μ (prod W)) ∘ μ T ∘ map T (σ) ∘ dec T
∘ map T (dec T) fequal.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
μ T ∘ map T (shift T) ∘ dec T =
map T (μ (prod W)) ∘ μ T ∘ map T (σ) ∘ dec T fequal.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
μ T ∘ map T (shift T) =
map T (μ (prod W)) ∘ μ T ∘ map T (σ)
    rewrite (natural (ϕ := @join T _)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
μ T ∘ map T (shift T) =
μ T ∘ map (T ∘ T) (μ (prod W)) ∘ map T (σ)
    unfold_ops @Map_compose.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
μ T ∘ map T (shift T) =
μ T ∘ map T (map T (μ (prod W))) ∘ map T (σ) reassociate -> on right.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
μ T ∘ map T (shift T) =
μ T ∘ (map T (map T (μ (prod W))) ∘ map T (σ))
    unfold_compose_in_compose.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
μ T ∘ map T (shift T) =
μ T ∘ (map T (map T (μ (prod W))) ∘ map T (σ))
    rewrite (fun_map_map (F := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
μ T ∘ map T (shift T) =
μ T ∘ map T (map T (μ (prod W)) ∘ σ)
    unfold shift.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
μ T ∘ map T (map T (uncurry incr) ∘ σ) =
μ T ∘ map T (map T (μ (prod W)) ∘ σ)
    rewrite incr_spec.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
H3: Decorate W T
op: Monoid_op W
unit0: Monoid_unit W
H4: Monoid W
H5: DecoratedFunctor W T
A: Type
μ T ∘ map T (map T (μ (prod W)) ∘ σ) =
μ T ∘ map T (map T (μ (prod W)) ∘ σ)
    reflexivity.
  Qed.

  (* TODO Prove (T ∘ prod W) is a monad *)
  (*
  Theorem decorated_monad_compatibility_spec:
    Monad_Hom T (T ∘ prod W) (@dec W T _) <->
    DecoratePreservingTransformation (fun A => A) T (ret T) /\
    DecoratePreservingTransformation (T ∘ T) T (@join T _).
  Proof with auto.
    split.
    - introv mhom. inverts mhom. inverts mhom_domain. split.
      + constructor...
        introv. symmetry. rewrite dec_ret_iff. apply mhom_ret.
      + constructor...
        introv. symmetry. rewrite dec_join_iff. apply mhom_join.
    - intros [h1 h2]. inverts h1. inverts h2.
      constructor; try typeclasses eauto.
      + admit.
      + admit.
      + introv  rewrite <- dec_ret_iff...
      + introv. rewrite <- dec_join_iff...
  Qed.

  Theorem decorated_monad_spec:
    Categorical.DecoratedMonad.DecoratedMonad W T <->
      Monad_Hom T (T ∘ prod W) (@dec W T _).
  Proof with try typeclasses eauto.
    rewrite decorated_monad_compatibility_spec.
    split; intro hyp.
    - inversion hyp. constructor...
      + constructor... intros. now rewrite (dmon_ret (W := W) (T := T)).
      + constructor... intros. now rewrite (dmon_join (W := W) (T := T)).
    - destruct hyp as [hyp1 hyp2]. constructor...
      + intros. inversion hyp1. now rewrite dectrans_commute.
      + intros. inversion hyp2. now rewrite <- dectrans_commute.
  Qed.
   *)

End DecoratedMonad_characterization.