DecoratedMonad.v

From Tealeaves Require Export
  Classes.Kleisli.DecoratedFunctor
  Classes.Kleisli.Monad
  Classes.Kleisli.Comonad
  Functors.Early.Writer.

From Tealeaves Require Import
  Classes.Categorical.Monad (join).

Import Monoid.Notations.

#[local] Generalizable Variables W T U.

(** * Decorated Monads *)
(**********************************************************************)

(** ** Operation <<bindd>> *)
(**********************************************************************)
Class Bindd (W: Type) (T U: Type -> Type):=
  bindd: forall (A B: Type), (W * A -> T B) -> U A -> U B.

#[global] Arguments bindd {W}%type_scope {T U}%function_scope
  {Bindd} {A B}%type_scope.

(** ** Kleisli Composition *)
(**********************************************************************)
Definition kc5
  {W: Type}
  {T: Type -> Type}
  `{Monoid_op_W: Monoid_op W}
  `{Bindd_WTT: Bindd W T T}
  {A B C: Type}:
  (W * B -> T C) ->
  (W * A -> T B) ->
  (W * A -> T C) :=
  fun g f '(w, a) =>
    @bindd W T T Bindd_WTT B C (g ⦿ w) (f (w, a)).

#[local] Infix "⋆5" := (kc5) (at level 60): tealeaves_scope.

(** ** Typeclass *)
(**********************************************************************)
Class DecoratedRightPreModule (W: Type) (T U: Type -> Type)
  `{Monoid_op_W: Monoid_op W}
  `{Return_T: Return T}
  `{Bindd_WTT: Bindd W T T}
  `{Bindd_WTU: Bindd W T U} :=
  { kdmod_bindd1:
    forall (A: Type),
      bindd (U := U) (ret ∘ extract (A := A)) = id;
    kdmod_bindd2:
    forall (A B C: Type) (g: W * B -> T C) (f: W * A -> T B),
      bindd (U := U) g ∘ bindd f = bindd (g ⋆5 f);
  }.

Class DecoratedMonad
  (W: Type)
  (T: Type -> Type)
  `{Monoid_unit_W: Monoid_unit W}
  `{Monoid_op_W: Monoid_op W}
  `{Return_T: Return T}
  `{Bindd_WTT: Bindd W T T} :=
  { kdm_monoid :> Monoid W;
    kdm_premod :> DecoratedRightPreModule W T T;
    kdm_bindd0: forall (A B: Type) (f: W * A -> T B),
      bindd f ∘ ret = f ∘ ret;
  }.

Class DecoratedRightModule
  (W: Type)
  (T: Type -> Type)
  (U: Type -> Type)
  `{Monoid_unit_W: Monoid_unit W}
  `{Monoid_op_W: Monoid_op W}
  `{Return_T: Return T}
  `{Bindd_WTT: Bindd W T T}
  `{Bindd_WTU: Bindd W T U}
  :=
  { kdmod_monad :> DecoratedMonad W T;
    kdmod_premod :> DecoratedRightPreModule W T U;
  }.

#[local] Instance DecoratedRightModule_DecoratedMonad
  (W: Type)
  (T: Type -> Type)
  `{DecoratedMonad_WT: DecoratedMonad W T}:
  DecoratedRightModule W T T :=
  {| kdmod_premod := kdm_premod;
  |}.

Lemma kdm_bindd1 `{DecoratedMonad W T}:
  forall (A: Type), bindd (ret ∘ extract) = @id (T A).W: Type
T: Type -> Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
forall A : Type, bindd (ret ∘ extract) = id
Proof.W: Type
T: Type -> Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
forall A : Type, bindd (ret ∘ extract) = id
  apply kdmod_bindd1.
Qed.

Lemma kdm_bindd2 `{DecoratedMonad W T}:
  forall (A B C: Type) (g: W * B -> T C) (f: W * A -> T B),
    bindd g ∘ bindd f = bindd (g ⋆5 f).W: Type
T: Type -> Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
forall (A B C : Type) (g : W * B -> T C)
  (f : W * A -> T B),
bindd g ∘ bindd f = bindd (g ⋆5 f)
Proof.W: Type
T: Type -> Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
forall (A B C : Type) (g : W * B -> T C)
  (f : W * A -> T B),
bindd g ∘ bindd f = bindd (g ⋆5 f)
  apply kdmod_bindd2.
Qed.

(** ** Kleisli Category Laws *)
(**********************************************************************)
Section decorated_monad_kleisli_category.

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

  #[local] Generalizable Variables A B C D.

  (** *** Interaction with [incr], [preincr] *)
  (********************************************************************)
  Lemma kc5_incr: forall `(g: W * B -> T C) `(f: W * A -> T B) (w: W),
      (g ∘ incr w) ⋆5 (f ∘ incr w) = (g ⋆5 f) ∘ incr w.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
forall (B C : Type) (g : W * B -> T C) (A : Type)
  (f : W * A -> T B) (w : W),
g ∘ incr w ⋆5 f ∘ incr w = (g ⋆5 f) ∘ incr w
  Proof.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
forall (B C : Type) (g : W * B -> T C) (A : Type)
  (f : W * A -> T B) (w : W),
g ∘ incr w ⋆5 f ∘ incr w = (g ⋆5 f) ∘ incr w
    intros.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
A: Type
f: W * A -> T B
w: W
g ∘ incr w ⋆5 f ∘ incr w = (g ⋆5 f) ∘ incr w
    unfold kc5.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
A: Type
f: W * A -> T B
w: W
(fun '(w0, a) =>
 bindd ((g ∘ incr w) ⦿ w0) ((f ∘ incr w) (w0, a))) =
(fun '(w, a) => bindd (g ⦿ w) (f (w, a))) ∘ incr w
    ext [w' a].T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
A: Type
f: W * A -> T B
w, w': W
a: A
bindd ((g ∘ incr w) ⦿ w') ((f ∘ incr w) (w', a)) =
((fun '(w, a) => bindd (g ⦿ w) (f (w, a))) ∘ incr w)
  (w', a)
    unfold preincr.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
A: Type
f: W * A -> T B
w, w': W
a: A
bindd (g ∘ incr w ∘ incr w') ((f ∘ incr w) (w', a)) =
((fun '(w, a) => bindd (g ∘ incr w) (f (w, a)))
 ∘ incr w) (w', a)
    reassociate ->.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
A: Type
f: W * A -> T B
w, w': W
a: A
bindd (g ∘ (incr w ∘ incr w')) ((f ∘ incr w) (w', a)) =
((fun '(w, a) => bindd (g ∘ incr w) (f (w, a)))
 ∘ incr w) (w', a)
    rewrite incr_incr.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
A: Type
f: W * A -> T B
w, w': W
a: A
bindd (g ∘ incr (w ● w')) ((f ∘ incr w) (w', a)) =
((fun '(w, a) => bindd (g ∘ incr w) (f (w, a)))
 ∘ incr w) (w', a)
    reflexivity.
  Qed.

  Lemma kc5_preincr: forall `(g: W * B -> T C) `(f: W * A -> T B) (w: W),
      (g ⋆5 f) ⦿ w = g ⦿ w ⋆5 f ⦿ w.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
forall (B C : Type) (g : W * B -> T C) (A : Type)
  (f : W * A -> T B) (w : W),
(g ⋆5 f) ⦿ w = g ⦿ w ⋆5 f ⦿ w
  Proof.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
forall (B C : Type) (g : W * B -> T C) (A : Type)
  (f : W * A -> T B) (w : W),
(g ⋆5 f) ⦿ w = g ⦿ w ⋆5 f ⦿ w
    intros.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
A: Type
f: W * A -> T B
w: W
(g ⋆5 f) ⦿ w = g ⦿ w ⋆5 f ⦿ w
    unfold preincr.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
A: Type
f: W * A -> T B
w: W
(g ⋆5 f) ∘ incr w = g ∘ incr w ⋆5 f ∘ incr w
    rewrite kc5_incr.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
A: Type
f: W * A -> T B
w: W
(g ⋆5 f) ∘ incr w = (g ⋆5 f) ∘ incr w
    reflexivity.
  Qed.

  (** *** Right identity law *)
  (********************************************************************)
  Theorem kc5_id_r {B C}: forall (g: W * B -> T C),
      g ⋆5 (ret ∘ extract) = g.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
forall g : W * B -> T C, g ⋆5 ret ∘ extract = g
  Proof.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
forall g : W * B -> T C, g ⋆5 ret ∘ extract = g
    intros.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
g ⋆5 ret ∘ extract = g
    unfold kc5.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
(fun '(w, a) => bindd (g ⦿ w) ((ret ∘ extract) (w, a))) =
g
    ext [w a].T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
w: W
a: B
bindd (g ⦿ w) ((ret ∘ extract) (w, a)) = g (w, a)
    unfold compose; cbn.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
w: W
a: B
bindd (g ⦿ w) (ret a) = g (w, a)
    compose near a on left.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
w: W
a: B
(bindd (g ⦿ w) ∘ ret) a = g (w, a)
    rewrite kdm_bindd0.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
w: W
a: B
(g ⦿ w ∘ ret) a = g (w, a)
    rewrite preincr_ret.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
B, C: Type
g: W * B -> T C
w: W
a: B
(g ∘ pair w) a = g (w, a)
    reflexivity.
  Qed.

  (** *** Left identity law *)
  (********************************************************************)
  Theorem kc5_id_l {A B}: forall (f: W * A -> T B),
      (ret ∘ extract) ⋆5 f = f.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B: Type
forall f : W * A -> T B, ret ∘ extract ⋆5 f = f
  Proof.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B: Type
forall f : W * A -> T B, ret ∘ extract ⋆5 f = f
    intros.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B: Type
f: W * A -> T B
ret ∘ extract ⋆5 f = f
    unfold kc5.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B: Type
f: W * A -> T B
(fun '(w, a) => bindd ((ret ∘ extract) ⦿ w) (f (w, a))) =
f
    ext [w a].T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B: Type
f: W * A -> T B
w: W
a: A
bindd ((ret ∘ extract) ⦿ w) (f (w, a)) = f (w, a)
    rewrite preincr_assoc.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B: Type
f: W * A -> T B
w: W
a: A
bindd (ret ∘ extract ⦿ w) (f (w, a)) = f (w, a)
    rewrite extract_preincr.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B: Type
f: W * A -> T B
w: W
a: A
bindd (ret ∘ extract) (f (w, a)) = f (w, a)
    rewrite kdm_bindd1.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B: Type
f: W * A -> T B
w: W
a: A
id (f (w, a)) = f (w, a)
    reflexivity.
  Qed.

  (** *** Associativity law *)
  (********************************************************************)
  Theorem kc5_assoc {A B C D}:
    forall (h: W * C -> T D)
      (g: W * B -> T C) (f: W * A -> T B),
      h ⋆5 (g ⋆5 f) = (h ⋆5 g) ⋆5 f.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B, C, D: Type
forall (h : W * C -> T D) (g : W * B -> T C)
  (f : W * A -> T B), h ⋆5 (g ⋆5 f) = (h ⋆5 g) ⋆5 f
  Proof.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B, C, D: Type
forall (h : W * C -> T D) (g : W * B -> T C)
  (f : W * A -> T B), h ⋆5 (g ⋆5 f) = (h ⋆5 g) ⋆5 f
    intros.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B, C, D: Type
h: W * C -> T D
g: W * B -> T C
f: W * A -> T B
h ⋆5 (g ⋆5 f) = (h ⋆5 g) ⋆5 f unfold kc5.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B, C, D: Type
h: W * C -> T D
g: W * B -> T C
f: W * A -> T B
(fun '(w, a) =>
 bindd (h ⦿ w) (bindd (g ⦿ w) (f (w, a)))) =
(fun '(w, a) =>
 bindd
   ((fun '(w0, a0) => bindd (h ⦿ w0) (g (w0, a0))) ⦿ w)
   (f (w, a)))
    ext [w a].T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B, C, D: Type
h: W * C -> T D
g: W * B -> T C
f: W * A -> T B
w: W
a: A
bindd (h ⦿ w) (bindd (g ⦿ w) (f (w, a))) =
bindd ((fun '(w, a) => bindd (h ⦿ w) (g (w, a))) ⦿ w)
  (f (w, a))
    compose near (f (w, a)) on left.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B, C, D: Type
h: W * C -> T D
g: W * B -> T C
f: W * A -> T B
w: W
a: A
(bindd (h ⦿ w) ∘ bindd (g ⦿ w)) (f (w, a)) =
bindd ((fun '(w, a) => bindd (h ⦿ w) (g (w, a))) ⦿ w)
  (f (w, a))
    rewrite kdm_bindd2.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B, C, D: Type
h: W * C -> T D
g: W * B -> T C
f: W * A -> T B
w: W
a: A
bindd (h ⦿ w ⋆5 g ⦿ w) (f (w, a)) =
bindd ((fun '(w, a) => bindd (h ⦿ w) (g (w, a))) ⦿ w)
  (f (w, a))
    rewrite <- kc5_preincr.T: Type -> Type
W: Type
Monoid_unit_W: Monoid_unit W
Monoid_op_W: Monoid_op W
Return_T: Return T
Bindd_WTT: Bindd W T T
H: DecoratedMonad W T
A, B, C, D: Type
h: W * C -> T D
g: W * B -> T C
f: W * A -> T B
w: W
a: A
bindd ((h ⋆5 g) ⦿ w) (f (w, a)) =
bindd ((fun '(w, a) => bindd (h ⦿ w) (g (w, a))) ⦿ w)
  (f (w, a))
    reflexivity.
  Qed.

End decorated_monad_kleisli_category.

(** ** Decorated Monad Homomorphisms *)
(**********************************************************************)
Class DecoratedMonadHom
  (W: Type)
  (T: Type -> Type)
  (U: Type -> Type)
  `{Return T} `{Bindd W T T}
  `{Return U} `{Bindd W U U}
  (ϕ: forall (A: Type), T A -> U A) :=
  { kdm_hom_bind: forall (A B: Type) (f: W * A -> T B),
      ϕ B ∘ @bindd W T T _ A B f = @bindd W U U _ A B (ϕ B ∘ f) ∘ ϕ A;
    kdm_hom_ret: forall (A: Type),
      ϕ A ∘ @ret T _ A = @ret U _ A;
  }.

Class DecoratedRightModuleHom
  (W: Type)
  (T: Type -> Type)
  (U: Type -> Type)
  (V: Type -> Type)
  `{Monoid_unit_W: Monoid_unit W}
  `{Monoid_op_W: Monoid_op W}
  `{Return_T: Return T}
  `{Bindd_WTT: Bindd W T V}
  `{Bindd_WTU: Bindd W T U}
  (ϕ: forall (A: Type), U A -> V A) :=
  { kdmod_hom_bind: forall (A B: Type) (f: W * A -> T B),
      ϕ B ∘ @bindd W T U _ A B f = @bindd W T V _ A B f ∘ ϕ A;
  }.

Class ParallelDecoratedRightModuleHom
  (T T' U U': Type -> Type)
  `{Return T}
  `{Bindd W T U}
  `{Bindd W T' U'}
  (ψ: forall (A: Type), T A -> T' A)
  (ϕ: forall (A: Type), U A -> U' A) :=
  { kdmod_parhom_bind: forall (A B: Type) (f: W * A -> T B),
      ϕ B ∘ bindd f = bindd (ψ B ∘ f) ∘ ϕ A;
  }.

(** * Derived Structures *)
(**********************************************************************)

(** ** Derived Operations *)
(**********************************************************************)
Module DerivedOperations.
  Section operations.

    Context
      (W: Type)
      (T: Type -> Type)
      (U: Type -> Type)
      `{Return_T: Return T}
      `{Bindd_WTU: Bindd W T U}.

    #[export] Instance Map_Bindd: Map U :=
      fun A B f => bindd (ret ∘ f ∘ extract).
    #[export] Instance Bind_Bindd: Bind T U :=
      fun A B f => bindd (f ∘ extract).
    #[export] Instance Mapd_Bindd: Mapd W U :=
      fun A B f => bindd (ret ∘ f).

  End operations.
End DerivedOperations.

Section compatibility.

  Context
    (W: Type)
    (T: Type -> Type)
    (U: Type -> Type)
    `{Map_U: Map U}
    `{Bind_TU: Bind T U}
    `{Mapd_WU: Mapd W U}
    `{Return_T: Return T}
    `{Bindd_WTU: Bindd W T U}.

  Class Compat_Map_Bindd: Prop :=
    compat_map_bindd:
      Map_U = @DerivedOperations.Map_Bindd W T U Return_T Bindd_WTU.

  Class Compat_Mapd_Bindd: Prop :=
    compat_mapd_bindd:
      Mapd_WU = @DerivedOperations.Mapd_Bindd W T U Return_T Bindd_WTU.

  Class Compat_Bind_Bindd: Prop :=
    compat_bind_bindd:
      Bind_TU = @DerivedOperations.Bind_Bindd W T U Bindd_WTU.

End compatibility.

Section self.

  Context
    `{Return_T: Return T}
    `{Bindd_WTU: Bindd W T U}.

  #[export] Instance Compat_Map_Bindd_Self:
    Compat_Map_Bindd W T U
      (Map_U := DerivedOperations.Map_Bindd W T U).T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Compat_Map_Bindd W T U
  Proof.T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Compat_Map_Bindd W T U
    reflexivity.
  Qed.

  #[export] Instance Compat_Mapd_Bindd_Self:
    Compat_Mapd_Bindd W T U
      (Mapd_WU := DerivedOperations.Mapd_Bindd W T U).T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Compat_Mapd_Bindd W T U
  Proof.T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Compat_Mapd_Bindd W T U
    reflexivity.
  Qed.

  #[export] Instance Compat_Bind_Bindd_Self:
    Compat_Bind_Bindd W T U
      (Bind_TU := DerivedOperations.Bind_Bindd W T U).T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Compat_Bind_Bindd W T U
  Proof.T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Compat_Bind_Bindd W T U
    reflexivity.
  Qed.

  #[export] Instance Compat_Map_Bind_Bindd
    `{Map_U: Map U}
    `{Bind_TU: Bind T U}
    `{! Compat_Bind_Bindd W T U}
    `{! Compat_Map_Bindd W T U}:
    Compat_Map_Bind T U.T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Map_U: Map U
Bind_TU: Bind T U
Compat_Bind_Bindd0: Compat_Bind_Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Map_Bind T U
  Proof.T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Map_U: Map U
Bind_TU: Bind T U
Compat_Bind_Bindd0: Compat_Bind_Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Map_Bind T U
    hnf.T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Map_U: Map U
Bind_TU: Bind T U
Compat_Bind_Bindd0: Compat_Bind_Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Map_U = DerivedOperations.Map_Bind T U
    rewrite (compat_map_bindd W T U).T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Map_U: Map U
Bind_TU: Bind T U
Compat_Bind_Bindd0: Compat_Bind_Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
DerivedOperations.Map_Bindd W T U =
DerivedOperations.Map_Bind T U
    rewrite (compat_bind_bindd W T U).T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Map_U: Map U
Bind_TU: Bind T U
Compat_Bind_Bindd0: Compat_Bind_Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
DerivedOperations.Map_Bindd W T U =
DerivedOperations.Map_Bind T U
    reflexivity.
  Qed.

  #[export] Instance Compat_Map_Mapd_Bindd
    `{Map_U: Map U}
    `{Mapd_WU: Mapd W U}
    `{! Compat_Mapd_Bindd W T U}
    `{! Compat_Map_Bindd W T U}:
    Compat_Map_Mapd W U.T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Map_U: Map U
Mapd_WU: Mapd W U
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Map_Mapd W U
  Proof.T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Map_U: Map U
Mapd_WU: Mapd W U
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Map_Mapd W U
    hnf.T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Map_U: Map U
Mapd_WU: Mapd W U
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Map_U = DerivedOperations.Map_Mapd W U
    rewrite (compat_map_bindd W T U).T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Map_U: Map U
Mapd_WU: Mapd W U
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
DerivedOperations.Map_Bindd W T U =
DerivedOperations.Map_Mapd W U
    rewrite (compat_mapd_bindd W T U).T: Type -> Type
Return_T: Return T
W: Type
U: Type -> Type
Bindd_WTU: Bindd W T U
Map_U: Map U
Mapd_WU: Mapd W U
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
DerivedOperations.Map_Bindd W T U =
DerivedOperations.Map_Mapd W U
    reflexivity.
  Qed.

End self.

Section compat_laws.

  #[local] Generalizable Variables A B.

  Context
    `{Map_U: Map U}
    `{Bind_TU: Bind T U}
    `{Mapd_WU: Mapd W U}
    `{Return_T: Return T}
    `{Bindd_WTU: Bindd W T U}.

  Lemma map_to_bindd `{! Compat_Map_Bindd W T U} `(f: A -> B):
    map (F := U) f = bindd (ret ∘ f ∘ extract).U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
A, B: Type
f: A -> B
map f = bindd (ret ∘ f ∘ extract)
  Proof.U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
A, B: Type
f: A -> B
map f = bindd (ret ∘ f ∘ extract)
    rewrite (compat_map_bindd W T U).U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
A, B: Type
f: A -> B
DerivedOperations.Map_Bindd W T U A B f =
bindd (ret ∘ f ∘ extract)
    reflexivity.
  Qed.

  Lemma mapd_to_bindd `{! Compat_Mapd_Bindd W T U} `(f: W * A -> B):
    mapd f = bindd (ret ∘ f).U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T U
A, B: Type
f: W * A -> B
mapd f = bindd (ret ∘ f)
  Proof.U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T U
A, B: Type
f: W * A -> B
mapd f = bindd (ret ∘ f)
    rewrite (compat_mapd_bindd W T U).U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T U
A, B: Type
f: W * A -> B
DerivedOperations.Mapd_Bindd W T U A B f =
bindd (ret ∘ f)
    reflexivity.
  Qed.

  Lemma bind_to_bindd  `{! Compat_Bind_Bindd W T U} `(f: A -> T B):
    bind f = bindd (f ∘ extract).U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Bind_Bindd0: Compat_Bind_Bindd W T U
A, B: Type
f: A -> T B
bind f = bindd (f ∘ extract)
  Proof.U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Bind_Bindd0: Compat_Bind_Bindd W T U
A, B: Type
f: A -> T B
bind f = bindd (f ∘ extract)
    rewrite (compat_bind_bindd W T U).U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Bind_Bindd0: Compat_Bind_Bindd W T U
A, B: Type
f: A -> T B
DerivedOperations.Bind_Bindd W T U A B f =
bindd (f ∘ extract)
    reflexivity.
  Qed.

  Lemma map_to_bind
    `{! Compat_Map_Bindd W T U}
    `{! Compat_Bind_Bindd W T U}
   : forall (A B: Type) (f: A -> B),
      map f = bind (ret ∘ f).U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Bind_Bindd0: Compat_Bind_Bindd W T U
forall (A B : Type) (f : A -> B),
map f = bind (ret ∘ f)
  Proof.U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Bind_Bindd0: Compat_Bind_Bindd W T U
forall (A B : Type) (f : A -> B),
map f = bind (ret ∘ f)
    intros.U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Bind_Bindd0: Compat_Bind_Bindd W T U
A, B: Type
f: A -> B
map f = bind (ret ∘ f)
    rewrite map_to_bindd.U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Bind_Bindd0: Compat_Bind_Bindd W T U
A, B: Type
f: A -> B
bindd (ret ∘ f ∘ extract) = bind (ret ∘ f)
    rewrite bind_to_bindd.U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Bind_Bindd0: Compat_Bind_Bindd W T U
A, B: Type
f: A -> B
bindd (ret ∘ f ∘ extract) = bindd (ret ∘ f ∘ extract)
    reflexivity.
  Qed.

  Lemma map_to_mapd
    `{! Compat_Map_Bindd W T U}
    `{! Compat_Mapd_Bindd W T U}
   : forall (A B: Type) (f: A -> B),
      map f = mapd (f ∘ extract).U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T U
forall (A B : Type) (f : A -> B),
map f = mapd (f ∘ extract)
  Proof.U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T U
forall (A B : Type) (f : A -> B),
map f = mapd (f ∘ extract)
    intros.U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T U
A, B: Type
f: A -> B
map f = mapd (f ∘ extract)
    rewrite map_to_bindd.U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T U
A, B: Type
f: A -> B
bindd (ret ∘ f ∘ extract) = mapd (f ∘ extract)
    rewrite mapd_to_bindd.U: Type -> Type
Map_U: Map U
T: Type -> Type
Bind_TU: Bind T U
W: Type
Mapd_WU: Mapd W U
Return_T: Return T
Bindd_WTU: Bindd W T U
Compat_Map_Bindd0: Compat_Map_Bindd W T U
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T U
A, B: Type
f: A -> B
bindd (ret ∘ f ∘ extract) =
bindd (ret ∘ (f ∘ extract))
    reflexivity.
  Qed.

End compat_laws.

(** ** Derived Kleisli Composition Laws *)
(**********************************************************************)
Section decorated_monad_derived_kleisli_laws.

  Import Kleisli.Monad.Notations.
  Import Kleisli.Comonad.Notations.

  #[local] Generalizable Variables A B C.

  Context
    `{Return_T: Return T}
    `{Bindd_WTT: Bindd W T T}
    `{Mapd_WT: Mapd W T}
    `{Bind_TT: Bind T T}
    `{Map_T: Map T}
    `{op: Monoid_op W}
    `{unit: Monoid_unit W}
    `{! Compat_Map_Bindd W T T}
    `{! Compat_Bind_Bindd W T T}
    `{! Compat_Mapd_Bindd W T T}
    `{! DecoratedMonad W T}.

  Context {A B C: Type}.

  (** *** Homogeneous cases *)
  (********************************************************************)
  Lemma kc5_11: forall (g: W * B -> C) (f: W * A -> B),
      (ret ∘ g) ⋆5 (ret ∘ f) = ret ∘ (g ⋆1 f).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : W * A -> B),
ret ∘ g ⋆5 ret ∘ f = ret ∘ (g ⋆1 f)
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : W * A -> B),
ret ∘ g ⋆5 ret ∘ f = ret ∘ (g ⋆1 f)
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> B
ret ∘ g ⋆5 ret ∘ f = ret ∘ (g ⋆1 f) unfold kc5.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> B
(fun '(w, a) =>
 bindd ((ret ∘ g) ⦿ w) ((ret ∘ f) (w, a))) =
ret ∘ (g ⋆1 f) ext [w' a].T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> B
w': W
a: A
bindd ((ret ∘ g) ⦿ w') ((ret ∘ f) (w', a)) =
(ret ∘ (g ⋆1 f)) (w', a)
    unfold compose at 2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> B
w': W
a: A
bindd ((ret ∘ g) ⦿ w') (ret (f (w', a))) =
(ret ∘ (g ⋆1 f)) (w', a)
    compose near (f (w', a)).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> B
w': W
a: A
(bindd ((ret ∘ g) ⦿ w') ∘ ret) (f (w', a)) =
(ret ∘ (g ⋆1 f)) (w', a)
    rewrite kdm_bindd0.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> B
w': W
a: A
((ret ∘ g) ⦿ w' ∘ ret) (f (w', a)) =
(ret ∘ (g ⋆1 f)) (w', a)
    rewrite preincr_ret.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> B
w': W
a: A
(ret ∘ g ∘ pair w') (f (w', a)) =
(ret ∘ (g ⋆1 f)) (w', a)
    reflexivity.
  Qed.

  Lemma kc5_44: forall (g: B -> T C) (f: A -> T B),
      g ∘ extract ⋆5 f ∘ extract = (g ⋆ f) ∘ extract.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> T C) (f : A -> T B),
g ∘ extract ⋆5 f ∘ extract = (g ⋆ f) ∘ extract
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> T C) (f : A -> T B),
g ∘ extract ⋆5 f ∘ extract = (g ⋆ f) ∘ extract
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: A -> T B
g ∘ extract ⋆5 f ∘ extract = (g ⋆ f) ∘ extract unfold kc5, kc.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: A -> T B
(fun '(w, a) =>
 bindd ((g ∘ extract) ⦿ w) ((f ∘ extract) (w, a))) =
bind g ∘ f ∘ extract ext [w a].T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: A -> T B
w: W
a: A
bindd ((g ∘ extract) ⦿ w) ((f ∘ extract) (w, a)) =
(bind g ∘ f ∘ extract) (w, a)
    rewrite extract_preincr2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: A -> T B
w: W
a: A
bindd (g ∘ extract) ((f ∘ extract) (w, a)) =
(bind g ∘ f ∘ extract) (w, a)
    rewrite bind_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: A -> T B
w: W
a: A
bindd (g ∘ extract) ((f ∘ extract) (w, a)) =
(bindd (g ∘ extract) ∘ f ∘ extract) (w, a)
    reflexivity.
  Qed.

  Lemma kc5_00: forall (g: B -> C) (f: A -> B),
      (ret ∘ g ∘ extract) ⋆5 (ret ∘ f ∘ extract) =
        ret ∘ g ∘ f ∘ extract.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> C) (f : A -> B),
ret ∘ g ∘ extract ⋆5 ret ∘ f ∘ extract =
ret ∘ g ∘ f ∘ extract
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> C) (f : A -> B),
ret ∘ g ∘ extract ⋆5 ret ∘ f ∘ extract =
ret ∘ g ∘ f ∘ extract
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: A -> B
ret ∘ g ∘ extract ⋆5 ret ∘ f ∘ extract =
ret ∘ g ∘ f ∘ extract unfold kc5.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: A -> B
(fun '(w, a) =>
 bindd ((ret ∘ g ∘ extract) ⦿ w)
   ((ret ∘ f ∘ extract) (w, a))) =
ret ∘ g ∘ f ∘ extract ext [w a].T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: A -> B
w: W
a: A
bindd ((ret ∘ g ∘ extract) ⦿ w)
  ((ret ∘ f ∘ extract) (w, a)) =
(ret ∘ g ∘ f ∘ extract) (w, a)
    unfold compose at 3 4.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: A -> B
w: W
a: A
bindd ((ret ∘ g ∘ extract) ⦿ w)
  (ret (f (extract (w, a)))) =
(ret ∘ g ∘ f ∘ extract) (w, a) cbn.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: A -> B
w: W
a: A
bindd ((ret ∘ g ∘ extract) ⦿ w) (ret (f a)) =
(ret ∘ g ∘ f ∘ extract) (w, a)
    compose near (f a) on left.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: A -> B
w: W
a: A
(bindd ((ret ∘ g ∘ extract) ⦿ w) ∘ ret) (f a) =
(ret ∘ g ∘ f ∘ extract) (w, a)
    rewrite kdm_bindd0.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: A -> B
w: W
a: A
((ret ∘ g ∘ extract) ⦿ w ∘ ret) (f a) =
(ret ∘ g ∘ f ∘ extract) (w, a)
    rewrite extract_preincr2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: A -> B
w: W
a: A
(ret ∘ g ∘ extract ∘ ret) (f a) =
(ret ∘ g ∘ f ∘ extract) (w, a)
    reflexivity.
  Qed.

  (** *** Heterogeneous cases *)
  (********************************************************************)
  Lemma kc5_51: forall (g: W * B -> T C) (f: W * A -> B),
      g ⋆5 (ret ∘ f) = g ⋆1 f.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> T C) (f : W * A -> B),
g ⋆5 ret ∘ f = g ⋆1 f
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> T C) (f : W * A -> B),
g ⋆5 ret ∘ f = g ⋆1 f
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> B
g ⋆5 ret ∘ f = g ⋆1 f unfold kc5, kc1.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> B
(fun '(w, a) => bindd (g ⦿ w) ((ret ∘ f) (w, a))) =
g ∘ cobind f
    ext [w a].T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> B
w: W
a: A
bindd (g ⦿ w) ((ret ∘ f) (w, a)) =
(g ∘ cobind f) (w, a) unfold compose; cbn.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> B
w: W
a: A
bindd (g ⦿ w) (ret (f (w, a))) = g (w, f (w, a))
    compose near (f (w, a)) on left.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> B
w: W
a: A
(bindd (g ⦿ w) ∘ ret) (f (w, a)) = g (w, f (w, a))
    rewrite kdm_bindd0.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> B
w: W
a: A
(g ⦿ w ∘ ret) (f (w, a)) = g (w, f (w, a))
    rewrite preincr_ret.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> B
w: W
a: A
(g ∘ pair w) (f (w, a)) = g (w, f (w, a))
    reflexivity.
  Qed.

  Lemma kc5_54: forall (g: W * B -> T C) (f: A -> T B),
      g ⋆5 (f ∘ extract) = (fun '(w, t) => bindd (g ⦿ w) t) ∘ map f.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> T C) (f : A -> T B),
g ⋆5 f ∘ extract =
(fun '(w, t) => bindd (g ⦿ w) t) ∘ map f
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> T C) (f : A -> T B),
g ⋆5 f ∘ extract =
(fun '(w, t) => bindd (g ⦿ w) t) ∘ map f
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> T B
g ⋆5 f ∘ extract =
(fun '(w, t) => bindd (g ⦿ w) t) ∘ map f ext [w a].T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> T B
w: W
a: A
(g ⋆5 f ∘ extract) (w, a) =
((fun '(w, t) => bindd (g ⦿ w) t) ∘ map f) (w, a) reflexivity.
  Qed.

  Lemma kc5_50: forall (g: W * B -> T C) (f: A -> B),
      g ⋆5 (ret ∘ f ∘ extract) = g ∘ map f.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> T C) (f : A -> B),
g ⋆5 ret ∘ f ∘ extract = g ∘ map f
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> T C) (f : A -> B),
g ⋆5 ret ∘ f ∘ extract = g ∘ map f
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> B
g ⋆5 ret ∘ f ∘ extract = g ∘ map f ext [w a].T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> B
w: W
a: A
(g ⋆5 ret ∘ f ∘ extract) (w, a) = (g ∘ map f) (w, a) unfold kc5.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> B
w: W
a: A
bindd (g ⦿ w) ((ret ∘ f ∘ extract) (w, a)) =
(g ∘ map f) (w, a)
    unfold compose; cbn.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> B
w: W
a: A
bindd (g ⦿ w) (ret (f a)) = g (id w, f a)
    compose near (f a).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> B
w: W
a: A
(bindd (g ⦿ w) ∘ ret) (f a) = (g ∘ pair (id w)) (f a)
    rewrite kdm_bindd0.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> B
w: W
a: A
(g ⦿ w ∘ ret) (f a) = (g ∘ pair (id w)) (f a)
    rewrite preincr_ret.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> B
w: W
a: A
(g ∘ pair w) (f a) = (g ∘ pair (id w)) (f a)
    reflexivity.
  Qed.

  Lemma kc5_15: forall (g: W * B -> C) (f: W * A -> T B),
      (ret ∘ g) ⋆5 f = fun '(w, t) => mapd (g ⦿ w) (f (w, t)).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : W * A -> T B),
ret ∘ g ⋆5 f =
(fun '(w, t) => mapd (g ⦿ w) (f (w, t)))
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : W * A -> T B),
ret ∘ g ⋆5 f =
(fun '(w, t) => mapd (g ⦿ w) (f (w, t)))
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> T B
ret ∘ g ⋆5 f =
(fun '(w, t) => mapd (g ⦿ w) (f (w, t))) unfold kc5.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> T B
(fun '(w, a) => bindd ((ret ∘ g) ⦿ w) (f (w, a))) =
(fun '(w, t) => mapd (g ⦿ w) (f (w, t)))
    ext [w a].T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> T B
w: W
a: A
bindd ((ret ∘ g) ⦿ w) (f (w, a)) =
mapd (g ⦿ w) (f (w, a))
    rewrite mapd_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> T B
w: W
a: A
bindd ((ret ∘ g) ⦿ w) (f (w, a)) =
bindd (ret ∘ g ⦿ w) (f (w, a))
    reflexivity.
  Qed.

  Lemma kc5_45: forall (g: B -> T C) (f: W * A -> T B),
      (g ∘ extract) ⋆5 f = g ⋆ f.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> T C) (f : W * A -> T B),
g ∘ extract ⋆5 f = g ⋆ f
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> T C) (f : W * A -> T B),
g ∘ extract ⋆5 f = g ⋆ f
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> T B
g ∘ extract ⋆5 f = g ⋆ f unfold kc5, kc.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> T B
(fun '(w, a) => bindd ((g ∘ extract) ⦿ w) (f (w, a))) =
bind g ∘ f
    ext [w a].T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> T B
w: W
a: A
bindd ((g ∘ extract) ⦿ w) (f (w, a)) =
(bind g ∘ f) (w, a)
    rewrite extract_preincr2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> T B
w: W
a: A
bindd (g ∘ extract) (f (w, a)) = (bind g ∘ f) (w, a)
    rewrite bind_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> T B
w: W
a: A
bindd (g ∘ extract) (f (w, a)) =
(bindd (g ∘ extract) ∘ f) (w, a)
    reflexivity.
  Qed.

  Lemma kc5_05: forall (g: B -> C) (f: W * A -> T B),
      (ret ∘ g ∘ extract) ⋆5 f = map g ∘ f.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> C) (f : W * A -> T B),
ret ∘ g ∘ extract ⋆5 f = map g ∘ f
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> C) (f : W * A -> T B),
ret ∘ g ∘ extract ⋆5 f = map g ∘ f
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> T B
ret ∘ g ∘ extract ⋆5 f = map g ∘ f ext [w a].T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> T B
w: W
a: A
(ret ∘ g ∘ extract ⋆5 f) (w, a) = (map g ∘ f) (w, a) unfold kc5.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> T B
w: W
a: A
bindd ((ret ∘ g ∘ extract) ⦿ w) (f (w, a)) =
(map g ∘ f) (w, a)
    rewrite extract_preincr2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> T B
w: W
a: A
bindd (ret ∘ g ∘ extract) (f (w, a)) =
(map g ∘ f) (w, a)
    rewrite map_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> T B
w: W
a: A
bindd (ret ∘ g ∘ extract) (f (w, a)) =
(bindd (ret ∘ g ∘ extract) ∘ f) (w, a)
    reflexivity.
  Qed.

  Lemma kc5_41: forall (g: B -> T C) (f: W * A -> B),
      (g ∘ extract) ⋆5 (ret ∘ f) = g ∘ f.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> T C) (f : W * A -> B),
g ∘ extract ⋆5 ret ∘ f = g ∘ f
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> T C) (f : W * A -> B),
g ∘ extract ⋆5 ret ∘ f = g ∘ f
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> B
g ∘ extract ⋆5 ret ∘ f = g ∘ f unfold kc5.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> B
(fun '(w, a) =>
 bindd ((g ∘ extract) ⦿ w) ((ret ∘ f) (w, a))) = g ∘ f ext [w a].T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> B
w: W
a: A
bindd ((g ∘ extract) ⦿ w) ((ret ∘ f) (w, a)) =
(g ∘ f) (w, a)
    unfold compose at 2; cbn.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> B
w: W
a: A
bindd ((g ∘ extract) ⦿ w) (ret (f (w, a))) =
(g ∘ f) (w, a)
    compose near (f (w, a)) on left.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> B
w: W
a: A
(bindd ((g ∘ extract) ⦿ w) ∘ ret) (f (w, a)) =
(g ∘ f) (w, a)
    rewrite kdm_bindd0.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> B
w: W
a: A
((g ∘ extract) ⦿ w ∘ ret) (f (w, a)) = (g ∘ f) (w, a)
    rewrite extract_preincr2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> B
w: W
a: A
(g ∘ extract ∘ ret) (f (w, a)) = (g ∘ f) (w, a)
    reflexivity.
  Qed.

  Lemma kc5_14: forall (g: W * B -> C) (f: A -> T B),
      (ret ∘ g) ⋆5 (f ∘ extract) = fun '(w, a) => mapd (g ⦿ w) (f a).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : A -> T B),
ret ∘ g ⋆5 f ∘ extract =
(fun '(w, a) => mapd (g ⦿ w) (f a))
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : A -> T B),
ret ∘ g ⋆5 f ∘ extract =
(fun '(w, a) => mapd (g ⦿ w) (f a))
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> T B
ret ∘ g ⋆5 f ∘ extract =
(fun '(w, a) => mapd (g ⦿ w) (f a)) unfold kc5.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> T B
(fun '(w, a) =>
 bindd ((ret ∘ g) ⦿ w) ((f ∘ extract) (w, a))) =
(fun '(w, a) => mapd (g ⦿ w) (f a)) ext [w a].T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> T B
w: W
a: A
bindd ((ret ∘ g) ⦿ w) ((f ∘ extract) (w, a)) =
mapd (g ⦿ w) (f a)
    rewrite mapd_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> T B
w: W
a: A
bindd ((ret ∘ g) ⦿ w) ((f ∘ extract) (w, a)) =
bindd (ret ∘ g ⦿ w) (f a)
    reflexivity.
  Qed.

  Lemma kc5_01: forall (g: B -> C) (f: W * A -> B),
      (ret ∘ g ∘ extract) ⋆5 (ret ∘ f) = ret ∘ g ∘ f.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> C) (f : W * A -> B),
ret ∘ g ∘ extract ⋆5 ret ∘ f = ret ∘ g ∘ f
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> C) (f : W * A -> B),
ret ∘ g ∘ extract ⋆5 ret ∘ f = ret ∘ g ∘ f
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> B
ret ∘ g ∘ extract ⋆5 ret ∘ f = ret ∘ g ∘ f unfold kc5.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> B
(fun '(w, a) =>
 bindd ((ret ∘ g ∘ extract) ⦿ w) ((ret ∘ f) (w, a))) =
ret ∘ g ∘ f ext [w a].T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> B
w: W
a: A
bindd ((ret ∘ g ∘ extract) ⦿ w) ((ret ∘ f) (w, a)) =
(ret ∘ g ∘ f) (w, a)
    unfold compose at 3; cbn.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> B
w: W
a: A
bindd ((ret ∘ g ∘ extract) ⦿ w) (ret (f (w, a))) =
(ret ∘ g ∘ f) (w, a)
    compose near (f (w, a)) on left.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> B
w: W
a: A
(bindd ((ret ∘ g ∘ extract) ⦿ w) ∘ ret) (f (w, a)) =
(ret ∘ g ∘ f) (w, a)
    rewrite kdm_bindd0.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> B
w: W
a: A
((ret ∘ g ∘ extract) ⦿ w ∘ ret) (f (w, a)) =
(ret ∘ g ∘ f) (w, a)
    reflexivity.
  Qed.

  Lemma kc5_10: forall (g: W * B -> C) (f: A -> B),
      (ret ∘ g) ⋆5 (ret ∘ f ∘ extract) = ret ∘ g ∘ map f.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : A -> B),
ret ∘ g ⋆5 ret ∘ f ∘ extract = ret ∘ g ∘ map f
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : A -> B),
ret ∘ g ⋆5 ret ∘ f ∘ extract = ret ∘ g ∘ map f
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> B
ret ∘ g ⋆5 ret ∘ f ∘ extract = ret ∘ g ∘ map f unfold kc5.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> B
(fun '(w, a) =>
 bindd ((ret ∘ g) ⦿ w) ((ret ∘ f ∘ extract) (w, a))) =
ret ∘ g ∘ map f ext [w a].T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> B
w: W
a: A
bindd ((ret ∘ g) ⦿ w) ((ret ∘ f ∘ extract) (w, a)) =
(ret ∘ g ∘ map f) (w, a)
    unfold compose; cbn.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> B
w: W
a: A
bindd ((ret ○ g) ⦿ w) (ret (f a)) =
ret (g (id w, f a))
    compose near (f a).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> B
w: W
a: A
(bindd ((ret ○ g) ⦿ w) ∘ ret) (f a) =
ret ((g ∘ pair (id w)) (f a))
    rewrite kdm_bindd0.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> B
w: W
a: A
((ret ○ g) ⦿ w ∘ ret) (f a) =
ret ((g ∘ pair (id w)) (f a))
    unfold compose; cbn.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> B
w: W
a: A
((ret ○ g) ⦿ w) (ret (f a)) = ret (g (id w, f a))
    compose near (f a) on left.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> B
w: W
a: A
((ret ○ g) ⦿ w ∘ ret) (f a) = ret (g (id w, f a))
    rewrite preincr_ret.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
Mapd_WT: Mapd W T
Bind_TT: Bind T T
Map_T: Map T
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> B
w: W
a: A
(ret ○ g ∘ pair w) (f a) = ret (g (id w, f a))
    reflexivity.
  Qed.

End decorated_monad_derived_kleisli_laws.

(** ** Derived Composition Laws *)
(**********************************************************************)
Section decorated_monad_derived_composition_laws.

  Import Kleisli.Monad.Notations.
  Import Kleisli.Comonad.Notations.
  Import Product.Notations.

  #[local] Generalizable Variables A B C.

  Context
    `{Return_T: Return T}
    `{Bindd_WTT: Bindd W T T}
    `{Bindd_WTU: Bindd W T U}
    `{Mapd_WT: Mapd W T}
    `{Mapd_WU: Mapd W U}
    `{Bind_TT: Bind T T}
    `{Bind_TU: Bind T U}
    `{Map_T: Map T}
    `{Map_U: Map U}
    `{op: Monoid_op W}
    `{unit: Monoid_unit W}
    `{! Compat_Map_Bindd W T T}
    `{! Compat_Bind_Bindd W T T}
    `{! Compat_Mapd_Bindd W T T}
    `{! Compat_Map_Bindd W T U}
    `{! Compat_Bind_Bindd W T U}
    `{! Compat_Mapd_Bindd W T U}
    `{! DecoratedRightPreModule W T U}
    `{! DecoratedMonad W T}.

  Context (A B C: Type).

  (** *** Homogeneous cases *)
  (********************************************************************)
  Lemma mapd_mapd: forall (g: W * B -> C) (f: W * A -> B),
      mapd (T := U) g ∘ mapd f = mapd (g ⋆1 f).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : W * A -> B),
mapd g ∘ mapd f = mapd (g ⋆1 f)
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : W * A -> B),
mapd g ∘ mapd f = mapd (g ⋆1 f)
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> B
mapd g ∘ mapd f = mapd (g ⋆1 f)
    rewrite mapd_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> B
bindd (ret ∘ g) ∘ mapd f = mapd (g ⋆1 f)
    rewrite mapd_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> B
bindd (ret ∘ g) ∘ bindd (ret ∘ f) = mapd (g ⋆1 f)
    rewrite mapd_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> B
bindd (ret ∘ g) ∘ bindd (ret ∘ f) =
bindd (ret ∘ (g ⋆1 f))
    rewrite kdmod_bindd2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> B
bindd (ret ∘ g ⋆5 ret ∘ f) = bindd (ret ∘ (g ⋆1 f))
    rewrite kc5_11.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> B
bindd (ret ∘ (g ⋆1 f)) = bindd (ret ∘ (g ⋆1 f))
    reflexivity.
  Qed.

  Lemma bind_bind: forall (g: B -> T C) (f: A -> T B),
      bind g ∘ bind f = bind (U := U) (g ⋆ f).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> T C) (f : A -> T B),
bind g ∘ bind f = bind (g ⋆ f)
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> T C) (f : A -> T B),
bind g ∘ bind f = bind (g ⋆ f)
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: A -> T B
bind g ∘ bind f = bind (g ⋆ f)
    rewrite bind_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: A -> T B
bindd (g ∘ extract) ∘ bind f = bind (g ⋆ f)
    rewrite bind_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: A -> T B
bindd (g ∘ extract) ∘ bindd (f ∘ extract) =
bind (g ⋆ f)
    rewrite bind_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: A -> T B
bindd (g ∘ extract) ∘ bindd (f ∘ extract) =
bindd ((g ⋆ f) ∘ extract)
    rewrite kdmod_bindd2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: A -> T B
bindd (g ∘ extract ⋆5 f ∘ extract) =
bindd ((g ⋆ f) ∘ extract)
    rewrite kc5_44.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: A -> T B
bindd ((g ⋆ f) ∘ extract) = bindd ((g ⋆ f) ∘ extract)
    reflexivity.
  Qed.

  (** *** Composition with <<bindd>> and <<bind>> *)
  (********************************************************************)
  Corollary bind_bindd: forall (g: B -> T C) (f: W * A -> T B),
      bind g ∘ bindd f = bindd (U := U) (g ⋆ f).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> T C) (f : W * A -> T B),
bind g ∘ bindd f = bindd (g ⋆ f)
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> T C) (f : W * A -> T B),
bind g ∘ bindd f = bindd (g ⋆ f)
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> T B
bind g ∘ bindd f = bindd (g ⋆ f)
    rewrite bind_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> T B
bindd (g ∘ extract) ∘ bindd f = bindd (g ⋆ f)
    rewrite kdmod_bindd2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> T B
bindd (g ∘ extract ⋆5 f) = bindd (g ⋆ f)
    rewrite kc5_45.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> T B
bindd (g ⋆ f) = bindd (g ⋆ f)
    reflexivity.
  Qed.

  Corollary bindd_bind: forall (g: W * B -> T C) (f: A -> T B),
      bindd g ∘ bind (U := U) f =
        bindd ((fun '(w, t) => bindd (g ⦿ w) t) ∘ map f).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> T C) (f : A -> T B),
bindd g ∘ bind f =
bindd ((fun '(w, t) => bindd (g ⦿ w) t) ∘ map f)
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> T C) (f : A -> T B),
bindd g ∘ bind f =
bindd ((fun '(w, t) => bindd (g ⦿ w) t) ∘ map f)
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> T B
bindd g ∘ bind f =
bindd ((fun '(w, t) => bindd (g ⦿ w) t) ∘ map f)
    rewrite bind_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> T B
bindd g ∘ bindd (f ∘ extract) =
bindd ((fun '(w, t) => bindd (g ⦿ w) t) ∘ map f)
    rewrite kdmod_bindd2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> T B
bindd (g ⋆5 f ∘ extract) =
bindd ((fun '(w, t) => bindd (g ⦿ w) t) ∘ map f)
    rewrite kc5_54.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> T B
bindd ((fun '(w, t) => bindd (g ⦿ w) t) ∘ map f) =
bindd ((fun '(w, t) => bindd (g ⦿ w) t) ∘ map f)
    reflexivity.
  Qed.

  (** *** Composition with <<bindd>> and <<mapd>> *)
  (********************************************************************)
  Lemma bindd_mapd: forall (g: W * B -> T C) (f: W * A -> B),
      bindd g ∘ mapd f = bindd (U := U) (g ⋆1 f).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> T C) (f : W * A -> B),
bindd g ∘ mapd f = bindd (g ⋆1 f)
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> T C) (f : W * A -> B),
bindd g ∘ mapd f = bindd (g ⋆1 f)
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> B
bindd g ∘ mapd f = bindd (g ⋆1 f)
    rewrite mapd_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> B
bindd g ∘ bindd (ret ∘ f) = bindd (g ⋆1 f)
    rewrite kdmod_bindd2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> B
bindd (g ⋆5 ret ∘ f) = bindd (g ⋆1 f)
    rewrite kc5_51.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> B
bindd (g ⋆1 f) = bindd (g ⋆1 f)
    reflexivity.
  Qed.

  Corollary mapd_bindd: forall (g: W * B -> C) (f: W * A -> T B),
      mapd g ∘ bindd f =
        bindd (U := U) (fun '(w, t) => mapd (g ⦿ w) (f (w, t))).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : W * A -> T B),
mapd g ∘ bindd f =
bindd (fun '(w, t) => mapd (g ⦿ w) (f (w, t)))
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : W * A -> T B),
mapd g ∘ bindd f =
bindd (fun '(w, t) => mapd (g ⦿ w) (f (w, t)))
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> T B
mapd g ∘ bindd f =
bindd (fun '(w, t) => mapd (g ⦿ w) (f (w, t)))
    rewrite mapd_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> T B
bindd (ret ∘ g) ∘ bindd f =
bindd (fun '(w, t) => mapd (g ⦿ w) (f (w, t)))
    rewrite kdmod_bindd2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> T B
bindd (ret ∘ g ⋆5 f) =
bindd (fun '(w, t) => mapd (g ⦿ w) (f (w, t)))
    rewrite kc5_15.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: W * A -> T B
bindd (fun '(w, t) => mapd (g ⦿ w) (f (w, t))) =
bindd (fun '(w, t) => mapd (g ⦿ w) (f (w, t)))
    reflexivity.
  Qed.

  (** *** Composition with <<map>> *)
  (********************************************************************)
  Lemma bindd_map: forall (g: W * B -> T C) (f: A -> B),
      bindd g ∘ map f = bindd (U := U) (g ∘ map f).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> T C) (f : A -> B),
bindd g ∘ map f = bindd (g ∘ map f)
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> T C) (f : A -> B),
bindd g ∘ map f = bindd (g ∘ map f)
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> B
bindd g ∘ map f = bindd (g ∘ map f)
    rewrite map_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> B
bindd g ∘ bindd (ret ∘ f ∘ extract) =
bindd (g ∘ map f)
    rewrite kdmod_bindd2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> B
bindd (g ⋆5 ret ∘ f ∘ extract) = bindd (g ∘ map f)
    rewrite kc5_50.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: A -> B
bindd (g ∘ map f) = bindd (g ∘ map f)
    reflexivity.
  Qed.

  Corollary map_bindd: forall (g: B -> C) (f: W * A -> T B),
      map g ∘ bindd f = bindd (U := U) (map g ∘ f).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> C) (f : W * A -> T B),
map g ∘ bindd f = bindd (map g ∘ f)
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> C) (f : W * A -> T B),
map g ∘ bindd f = bindd (map g ∘ f)
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> T B
map g ∘ bindd f = bindd (map g ∘ f)
    rewrite map_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> T B
bindd (ret ∘ g ∘ extract) ∘ bindd f =
bindd (map g ∘ f)
    rewrite kdmod_bindd2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> T B
bindd (ret ∘ g ∘ extract ⋆5 f) = bindd (map g ∘ f)
    rewrite kc5_05.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> C
f: W * A -> T B
bindd (map g ∘ f) = bindd (map g ∘ f)
    reflexivity.
  Qed.

  (** *** Composition between <<mapd>> and <<bind>> *)
  (********************************************************************)
  Lemma mapd_bind: forall (g: W * B -> C) (f: A -> T B),
      mapd g ∘ bind f =
        bindd (U := U) (fun '(w, a) => mapd (g ⦿ w) (f a)).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : A -> T B),
mapd g ∘ bind f =
bindd (fun '(w, a) => mapd (g ⦿ w) (f a))
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : W * B -> C) (f : A -> T B),
mapd g ∘ bind f =
bindd (fun '(w, a) => mapd (g ⦿ w) (f a))
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> T B
mapd g ∘ bind f =
bindd (fun '(w, a) => mapd (g ⦿ w) (f a))
    rewrite mapd_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> T B
bindd (ret ∘ g) ∘ bind f =
bindd (fun '(w, a) => mapd (g ⦿ w) (f a))
    rewrite bind_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> T B
bindd (ret ∘ g) ∘ bindd (f ∘ extract) =
bindd (fun '(w, a) => mapd (g ⦿ w) (f a))
    rewrite kdmod_bindd2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> T B
bindd (ret ∘ g ⋆5 f ∘ extract) =
bindd (fun '(w, a) => mapd (g ⦿ w) (f a))
    rewrite kc5_14.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: W * B -> C
f: A -> T B
bindd (fun '(w, a) => mapd (g ⦿ w) (f a)) =
bindd (fun '(w, a) => mapd (g ⦿ w) (f a))
    reflexivity.
  Qed.

  Lemma bind_mapd: forall (g: B -> T C) (f: W * A -> B),
      bind g ∘ mapd f = bindd (U := U) (g ∘ f).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> T C) (f : W * A -> B),
bind g ∘ mapd f = bindd (g ∘ f)
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall (g : B -> T C) (f : W * A -> B),
bind g ∘ mapd f = bindd (g ∘ f)
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> B
bind g ∘ mapd f = bindd (g ∘ f)
    rewrite mapd_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> B
bind g ∘ bindd (ret ∘ f) = bindd (g ∘ f)
    rewrite bind_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> B
bindd (g ∘ extract) ∘ bindd (ret ∘ f) = bindd (g ∘ f)
    rewrite kdmod_bindd2.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> B
bindd (g ∘ extract ⋆5 ret ∘ f) = bindd (g ∘ f)
    rewrite kc5_41.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
g: B -> T C
f: W * A -> B
bindd (g ∘ f) = bindd (g ∘ f)
    reflexivity.
  Qed.

  (** *** Composition with <<ret>> *)
  (********************************************************************)
  Lemma bind_ret: forall (f: A -> T B),
      bind (U := T) f ∘ ret = f.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall f : A -> T B, bind f ∘ ret = f
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall f : A -> T B, bind f ∘ ret = f
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
f: A -> T B
bind f ∘ ret = f
    rewrite bind_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
f: A -> T B
bindd (f ∘ extract) ∘ ret = f
    rewrite kdm_bindd0.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
f: A -> T B
f ∘ extract ∘ ret = f
    reflexivity.
  Qed.

  Lemma mapd_ret: forall (f: W * A -> B),
      mapd (T := T) f ∘ ret = ret ∘ f ∘ ret (T := (W ×)).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall f : W * A -> B, mapd f ∘ ret = ret ∘ f ∘ ret
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
forall f : W * A -> B, mapd f ∘ ret = ret ∘ f ∘ ret
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
f: W * A -> B
mapd f ∘ ret = ret ∘ f ∘ ret
    rewrite mapd_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
f: W * A -> B
bindd (ret ∘ f) ∘ ret = ret ∘ f ∘ ret
    rewrite kdm_bindd0.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
f: W * A -> B
ret ∘ f ∘ ret = ret ∘ f ∘ ret
    reflexivity.
  Qed.

  (** *** Identity laws *)
  (********************************************************************)
  Lemma bind_id:
    bind (U := U) ret = @id (U A).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
bind ret = id
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
bind ret = id
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
bind ret = id
    rewrite bind_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
bindd (ret ∘ extract) = id
    rewrite kdmod_bindd1.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
id = id
    reflexivity.
  Qed.

  Lemma mapd_id:
    mapd (T := U) extract = @id (U A).T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
mapd extract = id
  Proof.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
mapd extract = id
    intros.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
mapd extract = id
    rewrite mapd_to_bindd.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
bindd (ret ∘ extract) = id
    rewrite kdmod_bindd1.T: Type -> Type
Return_T: Return T
W: Type
Bindd_WTT: Bindd W T T
U: Type -> Type
Bindd_WTU: Bindd W T U
Mapd_WT: Mapd W T
Mapd_WU: Mapd W U
Bind_TT: Bind T T
Bind_TU: Bind T U
Map_T: Map T
Map_U: Map U
op: Monoid_op W
unit: Monoid_unit W
Compat_Map_Bindd0: Compat_Map_Bindd W T T
Compat_Bind_Bindd0: Compat_Bind_Bindd W T T
Compat_Mapd_Bindd0: Compat_Mapd_Bindd W T T
Compat_Map_Bindd1: Compat_Map_Bindd W T U
Compat_Bind_Bindd1: Compat_Bind_Bindd W T U
Compat_Mapd_Bindd1: Compat_Mapd_Bindd W T U
DecoratedRightPreModule0: DecoratedRightPreModule W T
  U
DecoratedMonad0: DecoratedMonad W T
A, B, C: Type
id = id
    reflexivity.
  Qed.

End decorated_monad_derived_composition_laws.

(** ** Derived Typeclass Instances *)
(**********************************************************************)
Module DerivedInstances.
  Section decorated_monad_derivedinstances.

    Context
      (W: Type)
      (T: Type -> Type)
      (U: Type -> Type)
      `{Return_T: Return T}
      `{Bindd_WTT: Bindd W T T}
      `{Bindd_WTU: Bindd W T U}
      `{Mapd_WT: Mapd W T}
      `{Mapd_WU: Mapd W U}
      `{Bind_TT: Bind T T}
      `{Bind_TU: Bind T U}
      `{Map_T: Map T}
      `{Map_U: Map U}
      `{op: Monoid_op W}
      `{unit: Monoid_unit W}
      `{! Compat_Map_Bindd W T T}
      `{! Compat_Bind_Bindd W T T}
      `{! Compat_Mapd_Bindd W T T}
      `{! Compat_Map_Bindd W T U}
      `{! Compat_Bind_Bindd W T U}
      `{! Compat_Mapd_Bindd W T U}
      `{! DecoratedRightPreModule W T U}
      `{! DecoratedMonad W T}.

    #[local] Existing Instance DecoratedRightModule_DecoratedMonad.

    #[export] Instance RightPreModule_DecoratedRightPreModule:
      RightPreModule T U :=
      {| kmod_bind1 := bind_id;
         kmod_bind2 := bind_bind;
      |}.

    #[export] Instance RightPreModule_DecoratedRightPreModule_Monad:
      RightPreModule T T :=
      {| kmod_bind1 := bind_id;
         kmod_bind2 := bind_bind;
      |}.

    #[export] Instance Monad_DecoratedMonad:
      Kleisli.Monad.Monad T :=
      {| kmon_bind0 := bind_ret;
      |}.

    #[export] Instance DecoratedFunctor_DecoratedRightModule:
      Kleisli.DecoratedFunctor.DecoratedFunctor W U :=
      {| kdf_mapd1 := mapd_id;
         kdf_mapd2 := mapd_mapd;
      |}.

  End decorated_monad_derivedinstances.
End DerivedInstances.

(** * Instance for Writer *)
(**********************************************************************)
Import Product.Notations.

Section decorated_functor_reader.

  Context {W: Type} `{Monoid W}.

  #[export] Instance Bindd_Writer: Bindd W (W ×) (W ×) :=
    fun A B f => join (T := (W ×)) ∘ cobind f.

  (* This is local because exporting it leads to frequent
     typeclass resolution divergence for Monoid instances
     due to the circularity Monoid<-DecoratedMonad_Writer<-Monoid.
   *)

  #[local] Instance DecoratedMonad_Writer:
    DecoratedMonad W (W ×).W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
DecoratedMonad W (prod W)
  Proof.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
DecoratedMonad W (prod W)
    constructor.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Monoid W
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
DecoratedRightPreModule W (prod W) (prod W)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : W * A -> W * B),
bindd f ∘ ret = f ∘ ret
    -W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Monoid W assumption.
    -W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
DecoratedRightPreModule W (prod W) (prod W) constructor;
        unfold_ops @Bindd_Writer; intros.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
join ∘ cobind (ret ∘ extract) = id
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> W * C
f: W * A -> W * B
join ∘ cobind g ∘ (join ∘ cobind f) =
join ∘ cobind (g ⋆5 f)
      +W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
join ∘ cobind (ret ∘ extract) = id rewrite <- map_to_cobind.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
join ∘ map ret = id
        rewrite Monad.mon_join_map_ret.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
id = id
        reflexivity.
      +W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> W * C
f: W * A -> W * B
join ∘ cobind g ∘ (join ∘ cobind f) =
join ∘ cobind (g ⋆5 f) ext [w a].W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> W * C
f: W * A -> W * B
w: W
a: A
(join ∘ cobind g ∘ (join ∘ cobind f)) (w, a) =
(join ∘ cobind (g ⋆5 f)) (w, a)
        unfold kc5.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> W * C
f: W * A -> W * B
w: W
a: A
(join ∘ cobind g ∘ (join ∘ cobind f)) (w, a) =
(join
 ∘ cobind (fun '(w, a) => bindd (g ⦿ w) (f (w, a))))
  (w, a)
        unfold transparent tcs.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> W * C
f: W * A -> W * B
w: W
a: A
(map_fst (uncurry monoid_op) ○ α^-1
 ∘ (fun '(e, a) => (e, g (e, a)))
 ∘ (map_fst (uncurry monoid_op) ○ α^-1
    ∘ (fun '(e, a) => (e, f (e, a))))) (w, a) =
(map_fst (uncurry monoid_op) ○ α^-1
 ∘ (fun '(e, a) =>
    (e,
     let
     '(w, a0) := (e, a) in bindd (g ⦿ w) (f (w, a0)))))
  (w, a)
        unfold bindd.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> W * C
f: W * A -> W * B
w: W
a: A
(map_fst (uncurry monoid_op) ○ α^-1
 ∘ (fun '(e, a) => (e, g (e, a)))
 ∘ (map_fst (uncurry monoid_op) ○ α^-1
    ∘ (fun '(e, a) => (e, f (e, a))))) (w, a) =
(map_fst (uncurry monoid_op) ○ α^-1
 ∘ (fun '(e, a) =>
    (e,
     (map_fst (uncurry monoid_op) ○ α^-1
      ∘ (fun '(e0, a0) => (e0, (g ⦿ e) (e0, a0))))
       (f (e, a))))) (w, a)
        unfold compose, preincr, incr.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> W * C
f: W * A -> W * B
w: W
a: A
map_fst (uncurry monoid_op)
  (α^-1
     (let
      '(e, a) :=
       map_fst (uncurry monoid_op)
         (α^-1 (w, f (w, a))) in (e, g (e, a)))) =
map_fst (uncurry monoid_op)
  (α^-1
     (w,
      map_fst (uncurry monoid_op)
        (α^-1
           (let
            '(e, a) := f (w, a) in
             (e,
              (g ∘ (fun '(w1, a0) => (w ● w1, a0)))
                (e, a))))))
        unfold map_fst, map_tensor.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> W * C
f: W * A -> W * B
w: W
a: A
(let (x, y) :=
   α^-1
     (let
      '(e, a) :=
       let (x, y) := α^-1 (w, f (w, a)) in
       (uncurry monoid_op x, id y) in (e, g (e, a))) in
 (uncurry monoid_op x, id y)) =
(let (x, y) :=
   α^-1
     (w,
      let (x, y) :=
        α^-1
          (let
           '(e, a) := f (w, a) in
            (e,
             (g ∘ (fun '(w1, a0) => (w ● w1, a0)))
               (e, a))) in
      (uncurry monoid_op x, id y)) in
 (uncurry monoid_op x, id y))
        unfold uncurry, associator, associator_inv.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> W * C
f: W * A -> W * B
w: W
a: A
(let (x, y) :=
   let (x, p0) :=
     let
     '(e, a) :=
      let (x, y) :=
        let (y, z) := f (w, a) in (w, y, z) in
      (let '(x0, y0) := x in x0 ● y0, id y) in
      (e, g (e, a)) in
   let (y, z) := p0 in (x, y, z) in
 (let '(x0, y0) := x in x0 ● y0, id y)) =
(let (x, y) :=
   let (y, z) :=
     let (x, y) :=
       let (x, p0) :=
         let
         '(e, a) := f (w, a) in
          (e,
           (g ∘ (fun '(w1, a0) => (w ● w1, a0)))
             (e, a)) in
       let (y, z) := p0 in (x, y, z) in
     (let '(x0, y0) := x in x0 ● y0, id y) in
   (w, y, z) in
 (let '(x0, y0) := x in x0 ● y0, id y))
        unfold compose, id.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> W * C
f: W * A -> W * B
w: W
a: A
(let (x, y) :=
   let (x, p0) :=
     let
     '(e, a) :=
      let (x, y) :=
        let (y, z) := f (w, a) in (w, y, z) in
      (let '(x0, y0) := x in x0 ● y0, y) in
      (e, g (e, a)) in
   let (y, z) := p0 in (x, y, z) in
 (let '(x0, y0) := x in x0 ● y0, y)) =
(let (x, y) :=
   let (y, z) :=
     let (x, y) :=
       let (x, p0) :=
         let '(e, a) := f (w, a) in (e, g (w ● e, a)) in
       let (y, z) := p0 in (x, y, z) in
     (let '(x0, y0) := x in x0 ● y0, y) in
   (w, y, z) in
 (let '(x0, y0) := x in x0 ● y0, y))
        destruct (f (w, a)).W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> W * C
f: W * A -> W * B
w: W
a: A
w0: W
b: B
(let (x, y) :=
   let (y, z) := g (w ● w0, b) in (w ● w0, y, z) in
 (let '(x0, y0) := x in x0 ● y0, y)) =
(let (x, y) :=
   let (y, z) :=
     let (x, y) :=
       let (y, z) := g (w ● w0, b) in (w0, y, z) in
     (let '(x0, y0) := x in x0 ● y0, y) in
   (w, y, z) in
 (let '(x0, y0) := x in x0 ● y0, y))
        destruct (g (w ● w0, b)).W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> W * C
f: W * A -> W * B
w: W
a: A
w0: W
b: B
w1: W
c: C
((w ● w0) ● w1, c) = (w ● (w0 ● w1), c)
        rewrite monoid_assoc.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> W * C
f: W * A -> W * B
w: W
a: A
w0: W
b: B
w1: W
c: C
(w ● (w0 ● w1), c) = (w ● (w0 ● w1), c)
        reflexivity.
    -W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : W * A -> W * B),
bindd f ∘ ret = f ∘ ret intros.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> W * B
bindd f ∘ ret = f ∘ ret ext a.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> W * B
a: A
(bindd f ∘ ret) a = (f ∘ ret) a
      unfold ret, Return_Writer.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> W * B
a: A
(bindd f ∘ (fun a : A => (Ƶ, a))) a =
(f ∘ (fun a : A => (Ƶ, a))) a
      unfold bindd, Bindd_Writer.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> W * B
a: A
(join ∘ cobind f ∘ (fun a : A => (Ƶ, a))) a =
(f ∘ (fun a : A => (Ƶ, a))) a
      unfold join, Join_writer.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> W * B
a: A
(map_fst (uncurry monoid_op) ○ α^-1 ∘ cobind f
 ∘ (fun a : A => (Ƶ, a))) a =
(f ∘ (fun a : A => (Ƶ, a))) a
      unfold compose.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> W * B
a: A
map_fst (uncurry monoid_op) (α^-1 (cobind f (Ƶ, a))) =
f (Ƶ, a)
      cbn.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> W * B
a: A
map_fst (uncurry monoid_op)
  (let (y, z) := f (Ƶ, a) in (Ƶ, y, z)) = f (Ƶ, a)
      destruct (f (Ƶ, a)).W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> W * B
a: A
w: W
b: B
map_fst (uncurry monoid_op) (Ƶ, w, b) = (w, b)
      cbn.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> W * B
a: A
w: W
b: B
(Ƶ ● w, id b) = (w, b)
      rewrite monoid_id_l.W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> W * B
a: A
w: W
b: B
(w, id b) = (w, b)
      reflexivity.
  Qed.

End decorated_functor_reader.

(** * Notations *)
(**********************************************************************)
Module Notations.
  Infix "⋆5" := (kc5) (at level 60): tealeaves_scope.
  Include Monoid.Notations.
End Notations.