(** This file implements "monads decorated by monoid <<W>>." *)
From Tealeaves Require Export
  Classes.Monoid
  Classes.Categorical.DecoratedFunctor
  Classes.Categorical.RightModule
  Functors.Early.Writer.

Import Monoid.Notations.
Import Product.Notations.

#[local] Generalizable Variables W T F.

#[local] Arguments ret (T)%function_scope {Return}
  (A)%type_scope _.
#[local] Arguments join T%function_scope {Join}
  (A)%type_scope _.
#[local] Arguments map F%function_scope {Map}
  {A B}%type_scope f%function_scope _.
#[local] Arguments extract (W)%function_scope {Extract}
  (A)%type_scope _.
#[local] Arguments cojoin W%function_scope {Cojoin}
  {A}%type_scope _.

(** * The [shift] operation *)
(* uncurry (incr W) = join (W ×) *)
(**********************************************************************)
Definition shift (F: Type -> Type) `{Map F} `{Monoid_op W} {A}:
  W * F (W * A) -> F (W * A) := map F (uncurry incr) ∘ strength.

(** ** Basic Properties of [shift] *)
(**********************************************************************)
Section shift_functor_lemmas.

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

  (** The definition of [shift] is convenient for theorizing, but
      [shift_spec] offers an intuitive characterization that is more
      convenient for practical reasoning. *)
  Corollary shift_spec {A}: forall (w: W) (x: F (W * A)),
      shift F (w, x) = map F (map_fst (fun m => w ● m)) x.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
forall (w : W) (x : F (W * A)),
shift F (w, x) =
map F (map_fst (fun m : W => w ● m)) x
  Proof.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
forall (w : W) (x : F (W * A)),
shift F (w, x) =
map F (map_fst (fun m : W => w ● m)) x
    intros ? x.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w: W
x: F (W * A)
shift F (w, x) =
map F (map_fst (fun m : W => w ● m)) x unfold shift.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w: W
x: F (W * A)
(map F (uncurry incr) ∘ strength) (w, x) =
map F (map_fst (fun m : W => w ● m)) x unfold_ops @Join_writer.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w: W
x: F (W * A)
(map F (uncurry incr) ∘ strength) (w, x) =
map F (map_fst (fun m : W => w ● m)) x
    unfold compose; cbn.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w: W
x: F (W * A)
map F (uncurry incr) (map F (pair w) x) =
map F (map_fst (fun m : W => w ● m)) x compose near x on left.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w: W
x: F (W * A)
(map F (uncurry incr) ∘ map F (pair w)) x =
map F (map_fst (fun m : W => w ● m)) x
    rewrite fun_map_map.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w: W
x: F (W * A)
map F (uncurry incr ∘ pair w) x =
map F (map_fst (fun m : W => w ● m)) x
    reflexivity.
  Qed.

  Corollary shift_spec2 {A: Type}:
    shift F (A := A) = map F (join (W ×) A) ∘ strength.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
shift F = map F (join (prod W) A) ∘ strength
  Proof.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
shift F = map F (join (prod W) A) ∘ strength
    intros.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
shift F = map F (join (prod W) A) ∘ strength
    unfold shift.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
map F (uncurry incr) ∘ strength =
map F (join (prod W) A) ∘ strength
    rewrite incr_spec.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
map F (join (prod W) A) ∘ strength =
map F (join (prod W) A) ∘ strength
    reflexivity.
  Qed.

  (** If we think of <<shift>> as a function of two arguments,
      then it is natural in its second argument. *)
  Lemma shift_map1 {A B} (t: F (W * A)) (w: W) (f: A -> B):
    shift F (w, map (F ∘ prod W) f t)
    = map (F ∘ prod W) f (shift F (w, t)).
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
t: F (W * A)
w: W
f: A -> B
shift F (w, map (F ∘ prod W) f t) =
map (F ∘ prod W) f (shift F (w, t))
  Proof.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
t: F (W * A)
w: W
f: A -> B
shift F (w, map (F ∘ prod W) f t) =
map (F ∘ prod W) f (shift F (w, t))
    unfold_ops @Map_compose.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
t: F (W * A)
w: W
f: A -> B
shift F (w, map F (map (prod W) f) t) =
map F (map (prod W) f) (shift F (w, t))
    rewrite shift_spec.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
t: F (W * A)
w: W
f: A -> B
shift F (w, map F (map (prod W) f) t) =
map F (map (prod W) f)
  (map F (map_fst (fun m : W => w ● m)) t)
    unfold compose.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
t: F (W * A)
w: W
f: A -> B
shift F (w, map F (map (prod W) f) t) =
map F (map (prod W) f)
  (map F (map_fst (fun m : W => w ● m)) t)
    rewrite shift_spec.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
t: F (W * A)
w: W
f: A -> B
map F (map_fst (fun m : W => w ● m))
  (map F (map (prod W) f) t) =
map F (map (prod W) f)
  (map F (map_fst (fun m : W => w ● m)) t)
    compose near t.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
t: F (W * A)
w: W
f: A -> B
(map F (map_fst (fun m : W => w ● m))
 ∘ map F (map (prod W) f)) t =
(map F (map (prod W) f)
 ∘ map F (map_fst (fun m : W => w ● m))) t
    rewrite 2(fun_map_map).
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
t: F (W * A)
w: W
f: A -> B
map F (map_fst (fun m : W => w ● m) ∘ map (prod W) f)
  t =
map F (map (prod W) f ∘ map_fst (fun m : W => w ● m))
  t
    unfold_ops @Map_reader.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
t: F (W * A)
w: W
f: A -> B
map F (map_fst (fun m : W => w ● m) ∘ map_snd f) t =
map F (map_snd f ∘ map_fst (fun m : W => w ● m)) t
    rewrite product_map_slide_pf.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
t: F (W * A)
w: W
f: A -> B
map F (map_snd f ∘ map_fst (fun m : W => w ● m)) t =
map F (map_snd f ∘ map_fst (fun m : W => w ● m)) t
    reflexivity.
  Qed.

  (** We can also say <<shift>> is a natural transformation
      of type <<(W ×) ∘ F ∘ (W ×) \to F ∘ (W ×)>>. *)
  Lemma shift_map2 {A B}: forall (f: A -> B),
      map (F ∘ prod W) f ∘ shift F =
        shift F ∘ map (prod W ∘ F ∘ prod W) f.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
forall f : A -> B,
map (F ∘ prod W) f ∘ shift F =
shift F ∘ map (prod W ∘ F ∘ prod W) f
  Proof.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
forall f : A -> B,
map (F ∘ prod W) f ∘ shift F =
shift F ∘ map (prod W ∘ F ∘ prod W) f
    intros.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
f: A -> B
map (F ∘ prod W) f ∘ shift F =
shift F ∘ map (prod W ∘ F ∘ prod W) f ext [w t].
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
f: A -> B
w: W
t: F (W * A)
(map (F ∘ prod W) f ∘ shift F) (w, t) =
(shift F ∘ map (prod W ∘ F ∘ prod W) f) (w, t) unfold compose at 2.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
f: A -> B
w: W
t: F (W * A)
map (F ∘ prod W) f (shift F (w, t)) =
(shift F ∘ map (prod W ∘ F ∘ prod W) f) (w, t)
    now rewrite <- shift_map1.
  Qed.

  Corollary shift_natural: Natural (@shift F _ W _).
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
Natural (@shift F Map_F W op)
  Proof.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
Natural (@shift F Map_F W op)
    constructor; try typeclasses eauto.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
forall (A B : Type) (f : A -> B),
map (F ○ prod W) f ∘ shift F =
shift F ∘ map (fun A0 : Type => W * F (W * A0)) f
    intros.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A, B: Type
f: A -> B
map (F ○ prod W) f ∘ shift F =
shift F ∘ map (fun A : Type => W * F (W * A)) f apply shift_map2.
  Qed.

  (** We can increment the first argument before applying <<shift>>,
      or we can <<shift>> and then increment. This lemma is used
      e.g. in the binding case of the decorate-join law. *)
  Lemma shift_increment {A}: forall (w: W),
      shift F (A := A) ∘ map_fst (fun m: W => w ● m) =
        map F (map_fst (fun m: W => w ● m)) ∘ shift F.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
forall w : W,
shift F ∘ map_fst (fun m : W => w ● m) =
map F (map_fst (fun m : W => w ● m)) ∘ shift F
  Proof.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
forall w : W,
shift F ∘ map_fst (fun m : W => w ● m) =
map F (map_fst (fun m : W => w ● m)) ∘ shift F
    intros.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w: W
shift F ∘ map_fst (fun m : W => w ● m) =
map F (map_fst (fun m : W => w ● m)) ∘ shift F ext [w' a].
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w, w': W
a: F (W * A)
(shift F ∘ map_fst (fun m : W => w ● m)) (w', a) =
(map F (map_fst (fun m : W => w ● m)) ∘ shift F)
  (w', a) unfold compose.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w, w': W
a: F (W * A)
shift F (map_fst (fun m : W => w ● m) (w', a)) =
map F (map_fst (fun m : W => w ● m)) (shift F (w', a)) cbn.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w, w': W
a: F (W * A)
shift F (w ● w', id a) =
map F (map_fst (fun m : W => w ● m)) (shift F (w', a)) rewrite 2(shift_spec).
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w, w': W
a: F (W * A)
map F (map_fst (fun m : W => (w ● w') ● m)) (id a) =
map F (map_fst (fun m : W => w ● m))
  (map F (map_fst (fun m : W => w' ● m)) a)
    compose near a on right.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w, w': W
a: F (W * A)
map F (map_fst (fun m : W => (w ● w') ● m)) (id a) =
(map F (map_fst (fun m : W => w ● m))
 ∘ map F (map_fst (fun m : W => w' ● m))) a rewrite fun_map_map.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w, w': W
a: F (W * A)
map F (map_fst (fun m : W => (w ● w') ● m)) (id a) =
map F
  (map_fst (fun m : W => w ● m)
   ∘ map_fst (fun m : W => w' ● m)) a
    fequal.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w, w': W
a: F (W * A)
map_fst (fun m : W => (w ● w') ● m) =
map_fst (fun m : W => w ● m)
∘ map_fst (fun m : W => w' ● m) ext [w'' a']; cbn.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w, w': W
a: F (W * A)
w'': W
a': A
((w ● w') ● w'', id a') = (w ● (w' ● w''), id (id a')) now rewrite monoid_assoc.
  Qed.

  (** Applying <<shift>>, followed by discarding annotations at the
      leaves, is equivalent to simply discarding the original
      annotations and the argument to <<shift>>. *)
  Lemma shift_extract {A}:
    map F (extract (prod W) A) ∘ shift F =
      map F (extract (prod W) A) ∘ extract (prod W) (F (W * A)).
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
map F (extract (prod W) A) ∘ shift F =
map F (extract (prod W) A)
∘ extract (prod W) (F (W * A))
  Proof.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
map F (extract (prod W) A) ∘ shift F =
map F (extract (prod W) A)
∘ extract (prod W) (F (W * A))
    unfold shift.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
map F (extract (prod W) A)
∘ (map F (uncurry incr) ∘ strength) =
map F (extract (prod W) A)
∘ extract (prod W) (F (W * A)) reassociate <- on left.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
map F (extract (prod W) A) ∘ map F (uncurry incr)
∘ strength =
map F (extract (prod W) A)
∘ extract (prod W) (F (W * A))
    ext [w t].
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w: W
t: F (W * A)
(map F (extract (prod W) A) ∘ map F (uncurry incr)
 ∘ strength) (w, t) =
(map F (extract (prod W) A)
 ∘ extract (prod W) (F (W * A))) (w, t) unfold compose; cbn.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w: W
t: F (W * A)
map F (extract (prod W) A)
  (map F (uncurry incr) (map F (pair w) t)) =
map F (extract (prod W) A) t
    do 2 compose near t on left.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w: W
t: F (W * A)
(map F (extract (prod W) A)
 ∘ (map F (uncurry incr) ∘ map F (pair w))) t =
map F (extract (prod W) A) t
    do 2 rewrite fun_map_map.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w: W
t: F (W * A)
map F (extract (prod W) A ∘ (uncurry incr ∘ pair w)) t =
map F (extract (prod W) A) t
    fequal.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
w: W
t: F (W * A)
extract (prod W) A ∘ (uncurry incr ∘ pair w) =
extract (prod W) A now ext [w' a].
  Qed.

  Lemma shift_zero {A}: forall (t: F (W * A)),
      shift F (Ƶ, t) = t.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
forall t : F (W * A), shift F (Ƶ, t) = t
  Proof.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
forall t : F (W * A), shift F (Ƶ, t) = t
    intros.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
t: F (W * A)
shift F (Ƶ, t) = t rewrite shift_spec.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
t: F (W * A)
map F (map_fst (fun m : W => Ƶ ● m)) t = t
    cut (map_fst (Y := A) (fun w => Ƶ ● w) = id).
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
t: F (W * A)
map_fst (fun w : W => Ƶ ● w) = id ->
map F (map_fst (fun m : W => Ƶ ● m)) t = t
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
t: F (W * A)
map_fst (fun w : W => Ƶ ● w) = id
    intros rw; rewrite rw.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
t: F (W * A)
rw: map_fst (fun w : W => Ƶ ● w) = id
map F id t = t
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
t: F (W * A)
map_fst (fun w : W => Ƶ ● w) = id now rewrite fun_map_id.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
t: F (W * A)
map_fst (fun w : W => Ƶ ● w) = id
    ext [w a].
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
t: F (W * A)
w: W
a: A
map_fst (fun w : W => Ƶ ● w) (w, a) = id (w, a) cbn.
F: Type -> Type
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_F: Map F
H0: Functor F
A: Type
t: F (W * A)
w: W
a: A
(Ƶ ● w, id a) = id (w, a) now simpl_monoid.
  Qed.

End shift_functor_lemmas.

From Tealeaves Require Import
  Classes.Categorical.RightComodule.

(** * Decorated Monads *)
(**********************************************************************)
Class DecoratedMonad
  (W: Type)
  (T: Type -> Type)
  `{Map T} `{Return T} `{Join T} `{Decorate W T}
  `{Monoid_op W} `{Monoid_unit W} :=
  { dmon_functor :> DecoratedFunctor W T;
    dmon_monad :> Monad T;
    dmon_monoid :> Monoid W;
    dmon_ret: forall (A: Type),
      dec T ∘ ret T A = ret T (W * A) ∘ pair Ƶ;
    dmon_join: forall (A: Type),
      dec T ∘ join T A =
        join T (W * A) ∘ map T (shift T) ∘ dec T ∘ map T (dec T);
  }.

(** * Decorated Right Modules *)
(**********************************************************************)
Section DecoratedModule.

  Context
    (W: Type)
    (F T: Type -> Type)
    `{Map T} `{Return T} `{Join T} `{Decorate W T}
    `{Map F} `{RightAction F T} `{Decorate W F}
    `{Monoid_op W} `{Monoid_unit W}.

  Class DecoratedRightModule :=
    { dmod_monad :> DecoratedMonad W T;
      dmod_functor :> DecoratedFunctor W T;
      dmon_module :> Categorical.RightModule.RightModule F T;
      dmod_action: forall (A: Type),
        dec F ∘ right_action F (A := A) =
          right_action F ∘ map F (shift T) ∘ dec F ∘ map F (dec T);
    }.

End DecoratedModule.

(** * Basic Properties of [shift] on Monads *)
(**********************************************************************)
Section shift_monad_lemmas.

  #[local] Generalizable Variables A.

  Context
    `{Monad T}
    `{Monoid W}.

  (** [shift] applied to a singleton simplifies to a singleton. *)
  Lemma shift_return `(a: A) (w1 w2: W):
    shift T (w2, ret T _ (w1, a)) = ret T _ (w2 ● w1, a).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
a: A
w1, w2: W
shift T (w2, ret T (W * A) (w1, a)) =
ret T (W * A) (w2 ● w1, a)
  Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
a: A
w1, w2: W
shift T (w2, ret T (W * A) (w1, a)) =
ret T (W * A) (w2 ● w1, a)
    unfold shift, compose.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
a: A
w1, w2: W
map T (uncurry incr)
  (strength (w2, ret T (W * A) (w1, a))) =
ret T (W * A) (w2 ● w1, a) rewrite strength_return.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
a: A
w1, w2: W
map T (uncurry incr)
  (ret T (W * (W * A)) (w2, (w1, a))) =
ret T (W * A) (w2 ● w1, a)
    compose near (w2, (w1, a)) on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
a: A
w1, w2: W
(map T (uncurry incr) ∘ ret T (W * (W * A)))
  (w2, (w1, a)) = ret T (W * A) (w2 ● w1, a)
    now rewrite (natural (F := fun A => A)).
  Qed.

  Lemma shift_join `(t: T (T (W * A))) (w: W):
    shift T (w, join T (W * A) t) =
      join T (W * A) (map T (fun t => shift T (w, t)) t).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
t: T (T (W * A))
w: W
shift T (w, join T (W * A) t) =
join T (W * A) (map T (shift T ○ pair w) t)
  Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
t: T (T (W * A))
w: W
shift T (w, join T (W * A) t) =
join T (W * A) (map T (shift T ○ pair w) t)
    rewrite (shift_spec T).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
t: T (T (W * A))
w: W
map T (map_fst (fun m : W => w ● m))
  (join T (W * A) t) =
join T (W * A) (map T (shift T ○ pair w) t) compose near t on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
t: T (T (W * A))
w: W
(map T (map_fst (fun m : W => w ● m)) ∘ join T (W * A))
  t = join T (W * A) (map T (shift T ○ pair w) t)
    rewrite natural.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
t: T (T (W * A))
w: W
(join T (W * A)
 ∘ map (T ∘ T) (map_fst (fun m : W => w ● m))) t =
join T (W * A) (map T (shift T ○ pair w) t) unfold compose; cbn.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
t: T (T (W * A))
w: W
join T (W * A)
  (map (T ○ T) (map_fst (fun m : W => w ● m)) t) =
join T (W * A) (map T (shift T ○ pair w) t)
    fequal.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
t: T (T (W * A))
w: W
map (T ○ T) (map_fst (fun m : W => w ● m)) t =
map T (shift T ○ pair w) t unfold_ops @Map_compose.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
t: T (T (W * A))
w: W
map T (map T (map_fst (fun m : W => w ● m))) t =
map T (shift T ○ pair w) t
    fequal.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
t: T (T (W * A))
w: W
map T (map_fst (fun m : W => w ● m)) =
shift T ○ pair w ext x.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H3: Monoid W
A: Type
t: T (T (W * A))
w: W
x: T (W * A)
map T (map_fst (fun m : W => w ● m)) x =
shift T (w, x) now rewrite (shift_spec T).
  Qed.

End shift_monad_lemmas.

(** ** Helper Lemmas for Proving Typeclass Instances *)
(** Each of the following lemmas is useful for proving one of the laws
    of decorated functors in the binder case(s) of proofs that proceed
    by induction on terms. *)
(**********************************************************************)
Section helper_lemmas.

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

  (** This lemma is useful for proving naturality of <<dec>>. *)
  Lemma dec_helper_1 {A B}: forall (f: A -> B) (t: F A) (w: W),
      map F (map (prod W) f) (dec F t) =
        dec F (map F f t) ->
      map F (map (prod W) f) (shift F (w, dec F t)) =
        shift F (w, dec F (map F f t)).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
A, B: Type
forall (f : A -> B) (t : F A) (w : W),
map F (map (prod W) f) (dec F t) = dec F (map F f t) ->
map F (map (prod W) f) (shift F (w, dec F t)) =
shift F (w, dec F (map F f t))
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
A, B: Type
forall (f : A -> B) (t : F A) (w : W),
map F (map (prod W) f) (dec F t) = dec F (map F f t) ->
map F (map (prod W) f) (shift F (w, dec F t)) =
shift F (w, dec F (map F f t))
    introv IH. (* there is a hidden compose to unfold *)
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
A, B: Type
f: A -> B
t: F A
w: W
IH: map F (map (prod W) f) (dec F t) =
dec F (map F f t)
map F (map (prod W) f) (shift F (w, dec F t)) =
shift F (w, dec F (map F f t))
    unfold compose; rewrite 2(shift_spec F).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
A, B: Type
f: A -> B
t: F A
w: W
IH: map F (map (prod W) f) (dec F t) =
dec F (map F f t)
map F (map (prod W) f)
  (map F (map_fst (fun m : W => w ● m)) (dec F t)) =
map F (map_fst (fun m : W => w ● m))
  (dec F (map F f t))
    compose near (dec F t) on left.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
A, B: Type
f: A -> B
t: F A
w: W
IH: map F (map (prod W) f) (dec F t) =
dec F (map F f t)
(map F (map (prod W) f)
 ∘ map F (map_fst (fun m : W => w ● m))) (dec F t) =
map F (map_fst (fun m : W => w ● m))
  (dec F (map F f t)) rewrite (fun_map_map).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
A, B: Type
f: A -> B
t: F A
w: W
IH: map F (map (prod W) f) (dec F t) =
dec F (map F f t)
map F (map (prod W) f ∘ map_fst (fun m : W => w ● m))
  (dec F t) =
map F (map_fst (fun m : W => w ● m))
  (dec F (map F f t))
    rewrite <- IH.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
A, B: Type
f: A -> B
t: F A
w: W
IH: map F (map (prod W) f) (dec F t) =
dec F (map F f t)
map F (map (prod W) f ∘ map_fst (fun m : W => w ● m))
  (dec F t) =
map F (map_fst (fun m : W => w ● m))
  (map F (map (prod W) f) (dec F t))
    compose near (dec F t) on right.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
A, B: Type
f: A -> B
t: F A
w: W
IH: map F (map (prod W) f) (dec F t) =
dec F (map F f t)
map F (map (prod W) f ∘ map_fst (fun m : W => w ● m))
  (dec F t) =
(map F (map_fst (fun m : W => w ● m))
 ∘ map F (map (prod W) f)) (dec F t) rewrite (fun_map_map).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
A, B: Type
f: A -> B
t: F A
w: W
IH: map F (map (prod W) f) (dec F t) =
dec F (map F f t)
map F (map (prod W) f ∘ map_fst (fun m : W => w ● m))
  (dec F t) =
map F (map_fst (fun m : W => w ● m) ∘ map (prod W) f)
  (dec F t)
    fequal.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
A, B: Type
f: A -> B
t: F A
w: W
IH: map F (map (prod W) f) (dec F t) =
dec F (map F f t)
map (prod W) f ∘ map_fst (fun m : W => w ● m) =
map_fst (fun m : W => w ● m) ∘ map (prod W) f now ext [w' a].
  Qed.

  Context
    `{Monad T}
    `{Decorate W T}.

  (** Now we can assume that <<dec>> is a natural transformation,
      which is needed for the following. *)
  Context
    `{! Natural (@dec W F _)}.

  (** This lemmas is useful for proving the dec-extract law. *)
  Lemma dec_helper_2 {A}: forall (t: F A) (w: W),
      map F (extract (prod W) A) (dec F t) = t ->
      map F (extract (prod W) A) (shift F (w, dec F t)) = t.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
forall (t : F A) (w : W),
map F (extract (prod W) A) (dec F t) = t ->
map F (extract (prod W) A) (shift F (w, dec F t)) = t
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
forall (t : F A) (w : W),
map F (extract (prod W) A) (dec F t) = t ->
map F (extract (prod W) A) (shift F (w, dec F t)) = t
    intros.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
H7: map F (extract (prod W) A) (dec F t) = t
map F (extract (prod W) A) (shift F (w, dec F t)) = t
    compose near (w, dec F t).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
H7: map F (extract (prod W) A) (dec F t) = t
(map F (extract (prod W) A) ∘ shift F) (w, dec F t) =
t
    rewrite (shift_extract F).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
H7: map F (extract (prod W) A) (dec F t) = t
(map F (extract (prod W) A)
 ∘ extract (prod W) (F (W * A))) (w, dec F t) = t unfold compose; cbn.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
H7: map F (extract (prod W) A) (dec F t) = t
map F (extract (prod W) A) (dec F t) = t
    auto.
  Qed.

  (** This lemmas is useful for proving the double decoration law. *)
  Lemma dec_helper_3 {A}: forall (t: F A) (w: W),
      dec F (dec F t) = map F (cojoin (prod W)) (dec F t) ->
      shift F (w, dec F (shift F (w, dec F t))) =
        map F (cojoin (prod W)) (shift F (w, dec F t)).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
forall (t : F A) (w : W),
dec F (dec F t) = map F (cojoin (prod W)) (dec F t) ->
shift F (w, dec F (shift F (w, dec F t))) =
map F (cojoin (prod W)) (shift F (w, dec F t))
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
forall (t : F A) (w : W),
dec F (dec F t) = map F (cojoin (prod W)) (dec F t) ->
shift F (w, dec F (shift F (w, dec F t))) =
map F (cojoin (prod W)) (shift F (w, dec F t))
    introv IH.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
shift F (w, dec F (shift F (w, dec F t))) =
map F (cojoin (prod W)) (shift F (w, dec F t)) unfold compose.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
shift F (w, dec F (shift F (w, dec F t))) =
map F (cojoin (prod W)) (shift F (w, dec F t)) rewrite 2(shift_spec F).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
map F (map_fst (fun m : W => w ● m))
  (dec F
     (map F (map_fst (fun m : W => w ● m)) (dec F t))) =
map F (cojoin (prod W))
  (map F (map_fst (fun m : W => w ● m)) (dec F t))
    compose near (dec F t).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
map F (map_fst (fun m : W => w ● m))
  ((dec F ∘ map F (map_fst (fun m : W => w ● m)))
     (dec F t)) =
(map F (cojoin (prod W))
 ∘ map F (map_fst (fun m : W => w ● m))) (dec F t)
    rewrite <- (natural (F := F) (G := F ○ prod W)).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
map F (map_fst (fun m : W => w ● m))
  ((map (F ○ prod W) (map_fst (fun m : W => w ● m))
    ∘ dec F) (dec F t)) =
(map F (cojoin (prod W))
 ∘ map F (map_fst (fun m : W => w ● m))) (dec F t)
    unfold compose.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
map F (map_fst (fun m : W => w ● m))
  (map (F ○ prod W) (map_fst (fun m : W => w ● m))
     (dec F (dec F t))) =
map F (cojoin (prod W))
  (map F (map_fst (fun m : W => w ● m)) (dec F t)) compose near (dec F (dec F t)).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
(map F (map_fst (fun m : W => w ● m))
 ∘ map (F ○ prod W) (map_fst (fun m : W => w ● m)))
  (dec F (dec F t)) =
map F (cojoin (prod W))
  (map F (map_fst (fun m : W => w ● m)) (dec F t))
    rewrite IH.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
(map F (map_fst (fun m : W => w ● m))
 ∘ map (F ○ prod W) (map_fst (fun m : W => w ● m)))
  (map F (cojoin (prod W)) (dec F t)) =
map F (cojoin (prod W))
  (map F (map_fst (fun m : W => w ● m)) (dec F t)) unfold_ops @Map_compose.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
(map F (map_fst (fun m : W => w ● m))
 ∘ map F (map (prod W) (map_fst (fun m : W => w ● m))))
  (map F (cojoin (prod W)) (dec F t)) =
map F (cojoin (prod W))
  (map F (map_fst (fun m : W => w ● m)) (dec F t))
    rewrite (fun_map_map).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
map F
  (map_fst (fun m : W => w ● m)
   ∘ map (prod W) (map_fst (fun m : W => w ● m)))
  (map F (cojoin (prod W)) (dec F t)) =
map F (cojoin (prod W))
  (map F (map_fst (fun m : W => w ● m)) (dec F t))
    compose near (dec F t).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
(map F
   (map_fst (fun m : W => w ● m)
    ∘ map (prod W) (map_fst (fun m : W => w ● m)))
 ∘ map F (cojoin (prod W))) (dec F t) =
(map F (cojoin (prod W))
 ∘ map F (map_fst (fun m : W => w ● m))) (dec F t)
    rewrite (fun_map_map).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
map F
  (map_fst (fun m : W => w ● m)
   ∘ map (prod W) (map_fst (fun m : W => w ● m))
   ∘ cojoin (prod W)) (dec F t) =
(map F (cojoin (prod W))
 ∘ map F (map_fst (fun m : W => w ● m))) (dec F t)
    rewrite (fun_map_map).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
map F
  (map_fst (fun m : W => w ● m)
   ∘ map (prod W) (map_fst (fun m : W => w ● m))
   ∘ cojoin (prod W)) (dec F t) =
map F (cojoin (prod W) ∘ map_fst (fun m : W => w ● m))
  (dec F t)
    unfold compose.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
map F
  (fun a : W * A =>
   map_fst (fun m : W => w ● m)
     (map (prod W) (map_fst (fun m : W => w ● m))
        (cojoin (prod W) a))) (dec F t) =
map F (cojoin (prod W) ○ map_fst (fun m : W => w ● m))
  (dec F t) fequal.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: F A
w: W
IH: dec F (dec F t) =
map F (cojoin (prod W)) (dec F t)
(fun a : W * A =>
 map_fst (fun m : W => w ● m)
   (map (prod W) (map_fst (fun m : W => w ● m))
      (cojoin (prod W) a))) =
cojoin (prod W) ○ map_fst (fun m : W => w ● m)
    now ext [w' a].
  Qed.

  (** This lemmas is useful for proving the decoration-join law. *)
  Lemma dec_helper_4 {A}: forall (t: T (T A)) (w: W),
      dec T (join T A t) =
        join T (W * A) (map T (shift T) (dec T (map T (dec T) t))) ->
      shift T (w, dec T (join T A t)) =
        join T (W * A)
          (map T (shift T) (shift T (w, dec T (map T (dec T) t)))).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
forall (t : T (T A)) (w : W),
dec T (join T A t) =
join T (W * A)
  (map T (shift T) (dec T (map T (dec T) t))) ->
shift T (w, dec T (join T A t)) =
join T (W * A)
  (map T (shift T)
     (shift T (w, dec T (map T (dec T) t))))
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
forall (t : T (T A)) (w : W),
dec T (join T A t) =
join T (W * A)
  (map T (shift T) (dec T (map T (dec T) t))) ->
shift T (w, dec T (join T A t)) =
join T (W * A)
  (map T (shift T)
     (shift T (w, dec T (map T (dec T) t))))
    introv IH.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: T (T A)
w: W
IH: dec T (join T A t) =
join T (W * A)
  (map T (shift T) (dec T (map T (dec T) t)))
shift T (w, dec T (join T A t)) =
join T (W * A)
  (map T (shift T)
     (shift T (w, dec T (map T (dec T) t)))) rewrite !(shift_spec T) in *.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: T (T A)
w: W
IH: dec T (join T A t) =
join T (W * A)
  (map T (shift T) (dec T (map T (dec T) t)))
map T (map_fst (fun m : W => w ● m))
  (dec T (join T A t)) =
join T (W * A)
  (map T (shift T)
     (map T (map_fst (fun m : W => w ● m))
        (dec T (map T (dec T) t)))) rewrite IH.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: T (T A)
w: W
IH: dec T (join T A t) =
join T (W * A)
  (map T (shift T) (dec T (map T (dec T) t)))
map T (map_fst (fun m : W => w ● m))
  (join T (W * A)
     (map T (shift T) (dec T (map T (dec T) t)))) =
join T (W * A)
  (map T (shift T)
     (map T (map_fst (fun m : W => w ● m))
        (dec T (map T (dec T) t))))
    compose near (dec T (map T (dec T) t)) on right.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: T (T A)
w: W
IH: dec T (join T A t) =
join T (W * A)
  (map T (shift T) (dec T (map T (dec T) t)))
map T (map_fst (fun m : W => w ● m))
  (join T (W * A)
     (map T (shift T) (dec T (map T (dec T) t)))) =
join T (W * A)
  ((map T (shift T)
    ∘ map T (map_fst (fun m : W => w ● m)))
     (dec T (map T (dec T) t)))
    rewrite (fun_map_map (F := T)).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: T (T A)
w: W
IH: dec T (join T A t) =
join T (W * A)
  (map T (shift T) (dec T (map T (dec T) t)))
map T (map_fst (fun m : W => w ● m))
  (join T (W * A)
     (map T (shift T) (dec T (map T (dec T) t)))) =
join T (W * A)
  (map T (shift T ∘ map_fst (fun m : W => w ● m))
     (dec T (map T (dec T) t))) rewrite (shift_increment T).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: T (T A)
w: W
IH: dec T (join T A t) =
join T (W * A)
  (map T (shift T) (dec T (map T (dec T) t)))
map T (map_fst (fun m : W => w ● m))
  (join T (W * A)
     (map T (shift T) (dec T (map T (dec T) t)))) =
join T (W * A)
  (map T
     (map T (map_fst (fun m : W => w ● m)) ∘ shift T)
     (dec T (map T (dec T) t)))
    rewrite <- (fun_map_map (F := T)).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: T (T A)
w: W
IH: dec T (join T A t) =
join T (W * A)
  (map T (shift T) (dec T (map T (dec T) t)))
map T (map_fst (fun m : W => w ● m))
  (join T (W * A)
     (map T (shift T) (dec T (map T (dec T) t)))) =
join T (W * A)
  ((map T (map T (map_fst (fun m : W => w ● m)))
    ∘ map T (shift T)) (dec T (map T (dec T) t)))
    change (map T (map T ?f)) with (map (T ∘ T) f).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: T (T A)
w: W
IH: dec T (join T A t) =
join T (W * A)
  (map T (shift T) (dec T (map T (dec T) t)))
map T (map_fst (fun m : W => w ● m))
  (join T (W * A)
     (map T (shift T) (dec T (map T (dec T) t)))) =
join T (W * A)
  ((map (T ∘ T) (map_fst (fun m : W => w ● m))
    ∘ map T (shift T)) (dec T (map T (dec T) t)))
    compose near (dec T (map T (dec T) t)).
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: T (T A)
w: W
IH: dec T (join T A t) =
join T (W * A)
  (map T (shift T) (dec T (map T (dec T) t)))
map T (map_fst (fun m : W => w ● m))
  ((join T (W * A) ∘ map T (shift T))
     (dec T (map T (dec T) t))) =
(join T (W * A)
 ∘ (map (T ∘ T) (map_fst (fun m : W => w ● m))
    ∘ map T (shift T))) (dec T (map T (dec T) t))
    reassociate <-.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: T (T A)
w: W
IH: dec T (join T A t) =
join T (W * A)
  (map T (shift T) (dec T (map T (dec T) t)))
map T (map_fst (fun m : W => w ● m))
  ((join T (W * A) ∘ map T (shift T))
     (dec T (map T (dec T) t))) =
(join T (W * A)
 ∘ map (T ∘ T) (map_fst (fun m : W => w ● m))
 ∘ map T (shift T)) (dec T (map T (dec T) t))
    #[local] Set Keyed Unification.
F: Type -> Type
Map_F: Map F
H: Functor F
W: Type
H0: Decorate W F
op: Monoid_op W
unit0: Monoid_unit W
H1: Monoid W
T: Type -> Type
H2: Map T
H3: Return T
H4: Join T
H5: Monad T
H6: Decorate W T
Natural0: Natural (@dec W F H0)
A: Type
t: T (T A)
w: W
IH: dec T (join T A t) =
join T (W * A)
  (map T (shift T) (dec T (map T (dec T) t)))
map T (map_fst (fun m : W => w ● m))
  ((join T (W * A) ∘ map T (shift T))
     (dec T (map T (dec T) t))) =
(join T (W * A)
 ∘ map (T ∘ T) (map_fst (fun m : W => w ● m))
 ∘ map T (shift T)) (dec T (map T (dec T) t))
    now rewrite <- (natural (ϕ := @join T _)).
    #[local] Unset Keyed Unification.
  Qed.

End helper_lemmas.

#[local] Generalizable Variables ϕ A B.

(** * Pushing Decorations through a Monoid Homomorphism *)
(** If a functor is readable by a monoid, it is readable by any target
    of a homomorphism from that monoid too. *)
(**********************************************************************)
Section DecoratedFunctor_monoid_homomorphism.

  Import Product.Notations.

  Context
    (Wsrc Wtgt: Type)
    `{Monoid_Morphism Wsrc Wtgt ϕ}
    `{Decorate Wsrc F} `{Map F} `{Return F} `{Join F}
    `{! DecoratedMonad Wsrc F}.

  Instance Decorate_homomorphism:
    Decorate Wtgt F := fun A => map F (map_fst ϕ) ∘ dec F.

  Instance Natural_read_morphism:
    Natural (@dec Wtgt F Decorate_homomorphism).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
Natural (@dec Wtgt F Decorate_homomorphism)
  Proof.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
Natural (@dec Wtgt F Decorate_homomorphism)
    constructor.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
Functor F
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
Functor (F ○ prod Wtgt)
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
forall (A B : Type) (f : A -> B),
map (F ○ prod Wtgt) f ∘ dec F = dec F ∘ map F f
    -
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
Functor F typeclasses eauto.
    -
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
Functor (F ○ prod Wtgt) typeclasses eauto.
    -
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
forall (A B : Type) (f : A -> B),
map (F ○ prod Wtgt) f ∘ dec F = dec F ∘ map F f intros.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A, B: Type
f: A -> B
map (F ○ prod Wtgt) f ∘ dec F = dec F ∘ map F f unfold_ops @Decorate_homomorphism.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A, B: Type
f: A -> B
map (F ○ prod Wtgt) f ∘ (map F (map_fst ϕ) ∘ dec F) =
map F (map_fst ϕ) ∘ dec F ∘ map F f
      unfold_ops @Map_compose.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A, B: Type
f: A -> B
map F (map (prod Wtgt) f)
∘ (map F (map_fst ϕ) ∘ dec F) =
map F (map_fst ϕ) ∘ dec F ∘ map F f

      reassociate <- on left.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A, B: Type
f: A -> B
map F (map (prod Wtgt) f) ∘ map F (map_fst ϕ) ∘ dec F =
map F (map_fst ϕ) ∘ dec F ∘ map F f
      rewrite (fun_map_map (F := F)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A, B: Type
f: A -> B
map F (map (prod Wtgt) f ∘ map_fst ϕ) ∘ dec F =
map F (map_fst ϕ) ∘ dec F ∘ map F f
      rewrite (product_map_commute).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A, B: Type
f: A -> B
map F (map_fst ϕ ∘ map (prod Wsrc) f) ∘ dec F =
map F (map_fst ϕ) ∘ dec F ∘ map F f
      rewrite <- (fun_map_map (F := F)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A, B: Type
f: A -> B
map F (map_fst ϕ) ∘ map F (map (prod Wsrc) f) ∘ dec F =
map F (map_fst ϕ) ∘ dec F ∘ map F f
      reassociate -> on left.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A, B: Type
f: A -> B
map F (map_fst ϕ)
∘ (map F (map (prod Wsrc) f) ∘ dec F) =
map F (map_fst ϕ) ∘ dec F ∘ map F f
      change (map F (map (prod Wsrc) f)) with
        (map (F ∘ prod Wsrc) f).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A, B: Type
f: A -> B
map F (map_fst ϕ) ∘ (map (F ∘ prod Wsrc) f ∘ dec F) =
map F (map_fst ϕ) ∘ dec F ∘ map F f
      reassociate ->.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A, B: Type
f: A -> B
map F (map_fst ϕ) ∘ (map (F ∘ prod Wsrc) f ∘ dec F) =
map F (map_fst ϕ) ∘ (dec F ∘ map F f)
      rewrite <- (natural (ϕ := @dec Wsrc F _ )).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A, B: Type
f: A -> B
map F (map_fst ϕ) ∘ (map (F ∘ prod Wsrc) f ∘ dec F) =
map F (map_fst ϕ) ∘ (map (F ○ prod Wsrc) f ∘ dec F)
      reflexivity.
  Qed.

  Lemma map_hom_cojoin: forall (A: Type),
      map_fst ϕ ∘ map (prod Wsrc) (map_fst ϕ) ∘
        cojoin (prod Wsrc) (A := A) =
        cojoin (prod Wtgt) ∘ map_fst ϕ.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
forall A : Type,
map_fst ϕ ∘ map (prod Wsrc) (map_fst ϕ)
∘ cojoin (prod Wsrc) = cojoin (prod Wtgt) ∘ map_fst ϕ
  Proof.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
forall A : Type,
map_fst ϕ ∘ map (prod Wsrc) (map_fst ϕ)
∘ cojoin (prod Wsrc) = cojoin (prod Wtgt) ∘ map_fst ϕ
    intros.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map_fst ϕ ∘ map (prod Wsrc) (map_fst ϕ)
∘ cojoin (prod Wsrc) = cojoin (prod Wtgt) ∘ map_fst ϕ now ext [w a].
  Qed.

  Instance DecoratedFunctor_morphism:
    Categorical.DecoratedFunctor.DecoratedFunctor Wtgt F.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
DecoratedFunctor Wtgt F
  Proof.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
DecoratedFunctor Wtgt F
    constructor; try typeclasses eauto.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
forall A : Type,
dec F ∘ dec F = map F (cojoin (prod Wtgt)) ∘ dec F
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
forall A : Type,
map F (extract (prod Wtgt) A) ∘ dec F = id
    -
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
forall A : Type,
dec F ∘ dec F = map F (cojoin (prod Wtgt)) ∘ dec F intros.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
dec F ∘ dec F = map F (cojoin (prod Wtgt)) ∘ dec F unfold dec, Decorate_homomorphism.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (map_fst ϕ) ∘ dec F
∘ (map F (map_fst ϕ) ∘ dec F) =
map F (cojoin (prod Wtgt))
∘ (map F (map_fst ϕ) ∘ dec F)
      reassociate <-.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (map_fst ϕ) ∘ dec F ∘ map F (map_fst ϕ) ∘ dec F =
map F (cojoin (prod Wtgt))
∘ (map F (map_fst ϕ) ∘ dec F) reassociate -> near (map F (map_fst ϕ)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (map_fst ϕ) ∘ (dec F ∘ map F (map_fst ϕ))
∘ dec F =
map F (cojoin (prod Wtgt))
∘ (map F (map_fst ϕ) ∘ dec F)
      rewrite <- (natural (ϕ := @dec Wsrc F _) (map_fst ϕ)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (map_fst ϕ)
∘ (map (F ○ prod Wsrc) (map_fst ϕ) ∘ dec F) ∘ dec F =
map F (cojoin (prod Wtgt))
∘ (map F (map_fst ϕ) ∘ dec F)
      reassociate <-.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (map_fst ϕ) ∘ map (F ○ prod Wsrc) (map_fst ϕ)
∘ dec F ∘ dec F =
map F (cojoin (prod Wtgt))
∘ (map F (map_fst ϕ) ∘ dec F)
      unfold_ops @Map_compose.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (map_fst ϕ)
∘ map F (map (prod Wsrc) (map_fst ϕ)) ∘ dec F ∘ dec F =
map F (cojoin (prod Wtgt))
∘ (map F (map_fst ϕ) ∘ dec F) rewrite (fun_map_map (F := F)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (map_fst ϕ ∘ map (prod Wsrc) (map_fst ϕ))
∘ dec F ∘ dec F =
map F (cojoin (prod Wtgt))
∘ (map F (map_fst ϕ) ∘ dec F)
      reassociate -> near (@dec Wsrc F _ A).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (map_fst ϕ ∘ map (prod Wsrc) (map_fst ϕ))
∘ (dec F ∘ dec F) =
map F (cojoin (prod Wtgt))
∘ (map F (map_fst ϕ) ∘ dec F)
      rewrite (dfun_dec_dec (E := Wsrc) (F := F)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (map_fst ϕ ∘ map (prod Wsrc) (map_fst ϕ))
∘ (map F (cojoin (prod Wsrc)) ∘ dec F) =
map F (cojoin (prod Wtgt))
∘ (map F (map_fst ϕ) ∘ dec F)
      reassociate <-.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (map_fst ϕ ∘ map (prod Wsrc) (map_fst ϕ))
∘ map F (cojoin (prod Wsrc)) ∘ dec F =
map F (cojoin (prod Wtgt))
∘ (map F (map_fst ϕ) ∘ dec F) rewrite (fun_map_map (F := F)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F
  (map_fst ϕ ∘ map (prod Wsrc) (map_fst ϕ)
   ∘ cojoin (prod Wsrc)) ∘ dec F =
map F (cojoin (prod Wtgt))
∘ (map F (map_fst ϕ) ∘ dec F)
      reassociate <-.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F
  (map_fst ϕ ∘ map (prod Wsrc) (map_fst ϕ)
   ∘ cojoin (prod Wsrc)) ∘ dec F =
map F (cojoin (prod Wtgt)) ∘ map F (map_fst ϕ) ∘ dec F rewrite (fun_map_map (F := F)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F
  (map_fst ϕ ∘ map (prod Wsrc) (map_fst ϕ)
   ∘ cojoin (prod Wsrc)) ∘ dec F =
map F (cojoin (prod Wtgt) ∘ map_fst ϕ) ∘ dec F
      rewrite map_hom_cojoin.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (cojoin (prod Wtgt) ∘ map_fst ϕ) ∘ dec F =
map F (cojoin (prod Wtgt) ∘ map_fst ϕ) ∘ dec F
      reflexivity.
    -
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
forall A : Type,
map F (extract (prod Wtgt) A) ∘ dec F = id intros.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (extract (prod Wtgt) A) ∘ dec F = id unfold dec, Decorate_homomorphism.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (extract (prod Wtgt) A)
∘ (map F (map_fst ϕ) ∘ dec F) = id
      reassociate <-.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (extract (prod Wtgt) A) ∘ map F (map_fst ϕ)
∘ dec F = id rewrite (fun_map_map (F := F)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (extract (prod Wtgt) A ∘ map_fst ϕ) ∘ dec F = id
      replace (extract (Wtgt ×) A ∘ map_fst ϕ)
        with (extract (Wsrc ×) A) by now ext [w a].
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
map F (extract (prod Wsrc) A) ∘ dec F = id
      rewrite (dfun_dec_extract (E := Wsrc) (F := F)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
A: Type
id = id
      reflexivity.
  Qed.

  Instance DecoratedMonad_morphism:
    DecoratedMonad.DecoratedMonad Wtgt F.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
DecoratedMonad Wtgt F
  Proof.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
DecoratedMonad Wtgt F
    inversion H.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
DecoratedMonad Wtgt F
    constructor; try typeclasses eauto.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
forall A : Type,
dec F ∘ ret F A = ret F (Wtgt * A) ∘ pair Ƶ
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
forall A : Type,
dec F ∘ join F A =
join F (Wtgt * A) ∘ map F (shift F) ∘ dec F
∘ map F (dec F)
    -
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
forall A : Type,
dec F ∘ ret F A = ret F (Wtgt * A) ∘ pair Ƶ intros.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
dec F ∘ ret F A = ret F (Wtgt * A) ∘ pair Ƶ unfold dec, Decorate_homomorphism.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
map F (map_fst ϕ) ∘ dec F ∘ ret F A =
ret F (Wtgt * A) ∘ pair Ƶ
      reassociate ->.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
map F (map_fst ϕ) ∘ (dec F ∘ ret F A) =
ret F (Wtgt * A) ∘ pair Ƶ rewrite (dmon_ret (W := Wsrc) (T := F)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
map F (map_fst ϕ) ∘ (ret F (Wsrc * A) ∘ pair Ƶ) =
ret F (Wtgt * A) ∘ pair Ƶ
      reassociate <-.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
map F (map_fst ϕ) ∘ ret F (Wsrc * A) ∘ pair Ƶ =
ret F (Wtgt * A) ∘ pair Ƶ rewrite (natural (ϕ := @ret F _)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
ret F (Wtgt * A) ∘ map (fun A : Type => A) (map_fst ϕ)
∘ pair Ƶ = ret F (Wtgt * A) ∘ pair Ƶ
      ext a.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
a: A
(ret F (Wtgt * A)
 ∘ map (fun A : Type => A) (map_fst ϕ) ∘ pair Ƶ) a =
(ret F (Wtgt * A) ∘ pair Ƶ) a unfold compose; cbn.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
a: A
ret F (Wtgt * A) (ϕ Ƶ, id a) = ret F (Wtgt * A) (Ƶ, a)
      now rewrite (monmor_unit).
    -
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
forall A : Type,
dec F ∘ join F A =
join F (Wtgt * A) ∘ map F (shift F) ∘ dec F
∘ map F (dec F) intros.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
dec F ∘ join F A =
join F (Wtgt * A) ∘ map F (shift F) ∘ dec F
∘ map F (dec F) unfold dec, Decorate_homomorphism.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
map F (map_fst ϕ) ∘ dec F ∘ join F A =
join F (Wtgt * A) ∘ map F (shift F)
∘ (map F (map_fst ϕ) ∘ dec F)
∘ map F (map F (map_fst ϕ) ∘ dec F)
      reassociate ->.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
map F (map_fst ϕ) ∘ (dec F ∘ join F A) =
join F (Wtgt * A) ∘ map F (shift F)
∘ (map F (map_fst ϕ) ∘ dec F)
∘ map F (map F (map_fst ϕ) ∘ dec F) rewrite (dmon_join (W := Wsrc) (T := F)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
map F (map_fst ϕ)
∘ (join F (Wsrc * A) ∘ map F (shift F) ∘ dec F
   ∘ map F (dec F)) =
join F (Wtgt * A) ∘ map F (shift F)
∘ (map F (map_fst ϕ) ∘ dec F)
∘ map F (map F (map_fst ϕ) ∘ dec F)
      repeat reassociate <-.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
map F (map_fst ϕ) ∘ join F (Wsrc * A)
∘ map F (shift F) ∘ dec F ∘ map F (dec F) =
join F (Wtgt * A) ∘ map F (shift F)
∘ map F (map_fst ϕ) ∘ dec F
∘ map F (map F (map_fst ϕ) ∘ dec F)
      rewrite (natural (ϕ := @join F _)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A) ∘ map (F ∘ F) (map_fst ϕ)
∘ map F (shift F) ∘ dec F ∘ map F (dec F) =
join F (Wtgt * A) ∘ map F (shift F)
∘ map F (map_fst ϕ) ∘ dec F
∘ map F (map F (map_fst ϕ) ∘ dec F)
      reassociate -> near (map F (shift F)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ (map (F ∘ F) (map_fst ϕ) ∘ map F (shift F)) ∘ dec F
∘ map F (dec F) =
join F (Wtgt * A) ∘ map F (shift F)
∘ map F (map_fst ϕ) ∘ dec F
∘ map F (map F (map_fst ϕ) ∘ dec F)
      unfold_ops @Map_compose.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ (map F (map F (map_fst ϕ)) ∘ map F (shift F))
∘ dec F ∘ map F (dec F) =
join F (Wtgt * A) ∘ map F (shift F)
∘ map F (map_fst ϕ) ∘ dec F
∘ map F (map F (map_fst ϕ) ∘ dec F)
      unfold_compose_in_compose.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ (map F (map F (map_fst ϕ)) ∘ map F (shift F))
∘ dec F ∘ map F (dec F) =
join F (Wtgt * A) ∘ map F (shift F)
∘ map F (map_fst ϕ) ∘ dec F
∘ map F (map F (map_fst ϕ) ∘ dec F)
      rewrite (fun_map_map (F := F) _ _ _
                 (shift F) (map F (map_fst ϕ))).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ map F (map F (map_fst ϕ) ∘ shift F) ∘ dec F
∘ map F (dec F) =
join F (Wtgt * A) ∘ map F (shift F)
∘ map F (map_fst ϕ) ∘ dec F
∘ map F (map F (map_fst ϕ) ∘ dec F)
      reassociate -> near (map F (map_fst ϕ)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ map F (map F (map_fst ϕ) ∘ shift F) ∘ dec F
∘ map F (dec F) =
join F (Wtgt * A)
∘ (map F (shift F) ∘ map F (map_fst ϕ)) ∘ dec F
∘ map F (map F (map_fst ϕ) ∘ dec F)
      rewrite (fun_map_map (F := F)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ map F (map F (map_fst ϕ) ∘ shift F) ∘ dec F
∘ map F (dec F) =
join F (Wtgt * A) ∘ map F (shift F ∘ map_fst ϕ)
∘ dec F ∘ map F (map F (map_fst ϕ) ∘ dec F)
      rewrite <- (fun_map_map (F := F) _ _ _
                   (dec F) (map F (map_fst ϕ))).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ map F (map F (map_fst ϕ) ∘ shift F) ∘ dec F
∘ map F (dec F) =
join F (Wtgt * A) ∘ map F (shift F ∘ map_fst ϕ)
∘ dec F ∘ (map F (map F (map_fst ϕ)) ∘ map F (dec F))
      reassociate <-.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ map F (map F (map_fst ϕ) ∘ shift F) ∘ dec F
∘ map F (dec F) =
join F (Wtgt * A) ∘ map F (shift F ∘ map_fst ϕ)
∘ dec F ∘ map F (map F (map_fst ϕ)) ∘ map F (dec F)
      reassociate -> near (map F (map F (map_fst ϕ))).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ map F (map F (map_fst ϕ) ∘ shift F) ∘ dec F
∘ map F (dec F) =
join F (Wtgt * A) ∘ map F (shift F ∘ map_fst ϕ)
∘ (dec F ∘ map F (map F (map_fst ϕ))) ∘ map F (dec F)
      rewrite <- (natural (ϕ := @dec Wsrc F _)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ map F (map F (map_fst ϕ) ∘ shift F) ∘ dec F
∘ map F (dec F) =
join F (Wtgt * A) ∘ map F (shift F ∘ map_fst ϕ)
∘ (map (F ○ prod Wsrc) (map F (map_fst ϕ)) ∘ dec F)
∘ map F (dec F)
      reassociate <-.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ map F (map F (map_fst ϕ) ∘ shift F) ∘ dec F
∘ map F (dec F) =
join F (Wtgt * A) ∘ map F (shift F ∘ map_fst ϕ)
∘ map (F ○ prod Wsrc) (map F (map_fst ϕ)) ∘ dec F
∘ map F (dec F) unfold_ops @Map_compose.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ map F (map F (map_fst ϕ) ∘ shift F) ∘ dec F
∘ map F (dec F) =
join F (Wtgt * A) ∘ map F (shift F ∘ map_fst ϕ)
∘ map F (map (prod Wsrc) (map F (map_fst ϕ))) ∘ dec F
∘ map F (dec F)
      reassociate -> near (map F (map (prod Wsrc) (map F (map_fst ϕ)))).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ map F (map F (map_fst ϕ) ∘ shift F) ∘ dec F
∘ map F (dec F) =
join F (Wtgt * A)
∘ (map F (shift F ∘ map_fst ϕ)
   ∘ map F (map (prod Wsrc) (map F (map_fst ϕ))))
∘ dec F ∘ map F (dec F)
      rewrite (fun_map_map (F := F)).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
join F (Wtgt * A)
∘ map F (map F (map_fst ϕ) ∘ shift F) ∘ dec F
∘ map F (dec F) =
join F (Wtgt * A)
∘ map F
    (shift F ∘ map_fst ϕ
     ∘ map (prod Wsrc) (map F (map_fst ϕ))) ∘ dec F
∘ map F (dec F)
      repeat fequal.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
map F (map_fst ϕ) ∘ shift F =
shift F ∘ map_fst ϕ
∘ map (prod Wsrc) (map F (map_fst ϕ)) ext [w t].
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
w: Wsrc
t: F (Wsrc * A)
(map F (map_fst ϕ) ∘ shift F) (w, t) =
(shift F ∘ map_fst ϕ
 ∘ map (prod Wsrc) (map F (map_fst ϕ))) (w, t)
      unfold compose; cbn.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
w: Wsrc
t: F (Wsrc * A)
map F (map_fst ϕ) (shift F (w, t)) =
shift F (ϕ (id w), id (map F (map_fst ϕ) t))
      change (id ?f) with f.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
w: Wsrc
t: F (Wsrc * A)
map F (map_fst ϕ) (shift F (w, t)) =
shift F (ϕ w, map F (map_fst ϕ) t) unfold shift.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
w: Wsrc
t: F (Wsrc * A)
map F (map_fst ϕ)
  ((map F (uncurry incr) ∘ strength) (w, t)) =
(map F (uncurry incr) ∘ strength)
  (ϕ w, map F (map_fst ϕ) t)
      unfold compose; cbn.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
w: Wsrc
t: F (Wsrc * A)
map F (map_fst ϕ)
  (map F (uncurry incr) (map F (pair w) t)) =
map F (uncurry incr)
  (map F (pair (ϕ w)) (map F (map_fst ϕ) t))
      do 2 (compose near t;
            repeat rewrite (fun_map_map (F := F))).
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
w: Wsrc
t: F (Wsrc * A)
map F (map_fst ϕ ∘ (uncurry incr ∘ pair w)) t =
map F (uncurry incr ∘ (pair (ϕ w) ∘ map_fst ϕ)) t
      fequal.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
w: Wsrc
t: F (Wsrc * A)
map_fst ϕ ∘ (uncurry incr ∘ pair w) =
uncurry incr ∘ (pair (ϕ w) ∘ map_fst ϕ) ext [w' a].
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
w: Wsrc
t: F (Wsrc * A)
w': Wsrc
a: A
(map_fst ϕ ∘ (uncurry incr ∘ pair w)) (w', a) =
(uncurry incr ∘ (pair (ϕ w) ∘ map_fst ϕ)) (w', a)
      unfold compose; cbn.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
w: Wsrc
t: F (Wsrc * A)
w': Wsrc
a: A
(ϕ (w ● w'), id a) = (ϕ w ● ϕ w', id a) rewrite monmor_op.
Wsrc, Wtgt: Type
src_op: Monoid_op Wsrc
src_unit: Monoid_unit Wsrc
tgt_op: Monoid_op Wtgt
tgt_unit: Monoid_unit Wtgt
ϕ: Wsrc -> Wtgt
H: Monoid_Morphism Wsrc Wtgt ϕ
F: Type -> Type
H0: Decorate Wsrc F
H1: Map F
H2: Return F
H3: Join F
DecoratedMonad0: DecoratedMonad Wsrc F
monmor_src: Monoid Wsrc
monmor_tgt: Monoid Wtgt
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : Wsrc,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
A: Type
w: Wsrc
t: F (Wsrc * A)
w': Wsrc
a: A
(ϕ w ● ϕ w', id a) = (ϕ w ● ϕ w', id a)
      reflexivity.
  Qed.

End DecoratedFunctor_monoid_homomorphism.