From Tealeaves Require Import
  Classes.Categorical.DecoratedMonad
  Classes.Kleisli.DecoratedMonad
  CategoricalToKleisli.DecoratedFunctor (cobind_dec).

#[local] Generalizable Variables W T.

Import Monoid.Notations.
Import Product.Notations.
Import Kleisli.DecoratedMonad.Notations.

(** * Categorical Decorated Monad to Kleisli Decorated Monad *)
(**********************************************************************)

(** ** Derived <<bindd>> Operation *)
(**********************************************************************)
Module DerivedOperations.

  #[export] Instance Bindd_Categorical
    (W: Type)
    (T: Type -> Type)
    `{Map_T: Map T}
    `{Join_T: Join T}
    `{Decorate_WT: Decorate W T}: Bindd W T T :=
  fun A B f => join (T := T) ∘ map (F := T) f ∘ dec T.

End DerivedOperations.

(** ** Derived Laws *)
(**********************************************************************)
Module DerivedInstances.

  (* Alectryon doesn't like this
     Import CategoricalToKleisli.DecoratedMonad.DerivedOperations.
   *)
  Import DerivedOperations.

  #[local] Generalizable Variables A B C.

  Section with_monad.

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

    (** *** Identity law *)
    (******************************************************************)
    Lemma bindd_id: forall (A: Type),
        bindd (ret (T := T) ∘ extract) = @id (T A).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
forall A : Type, bindd (ret ∘ extract) = id
    Proof.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
forall A : Type, bindd (ret ∘ extract) = id
      intros.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A: Type
bindd (ret ∘ extract) = id unfold_ops @Bindd_Categorical.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A: Type
join ∘ map (ret ∘ extract) ∘ dec T = id
      rewrite <- (fun_map_map (F := T)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A: Type
join ∘ (map ret ∘ map extract) ∘ dec T = id
      reassociate <-.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A: Type
join ∘ map ret ∘ map extract ∘ dec T = id
      rewrite (mon_join_map_ret (T := T)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A: Type
id ∘ map extract ∘ dec T = id
      reassociate ->.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A: Type
id ∘ (map extract ∘ dec T) = id
      rewrite (dfun_dec_extract (E := W) (F := T)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A: Type
id ∘ id = id
      reflexivity.
    Qed.

    (** *** Composition law *)
    (******************************************************************)
    Lemma bindd_bindd:
      forall (A B C: Type) (g: W * B -> T C) (f: W * A -> T B),
        bindd g ∘ bindd f = bindd (g ⋆5 f).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.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.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.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)
      intros.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
bindd g ∘ bindd f = bindd (g ⋆5 f) unfold bindd at 1 2, Bindd_Categorical.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map g ∘ dec T ∘ (join ∘ map f ∘ dec T) =
bindd (g ⋆5 f)
      (* change (join T ∘ map T ?f) with (bind T f).*)
      do 2 reassociate <-.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map g ∘ dec T ∘ join ∘ map f ∘ dec T =
bindd (g ⋆5 f)
      reassociate -> near join.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map g ∘ (dec T ∘ join) ∘ map f ∘ dec T =
bindd (g ⋆5 f)
      rewrite (dmon_join (W := W) (T := T)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map g
∘ (join ∘ map (shift T) ∘ dec T ∘ map (dec T)) ∘ map f
∘ dec T = bindd (g ⋆5 f)
      repeat reassociate <-.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map g ∘ join ∘ map (shift T) ∘ dec T
∘ map (dec T) ∘ map f ∘ dec T = bindd (g ⋆5 f)
      reassociate -> near (map f).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map g ∘ join ∘ map (shift T) ∘ dec T
∘ (map (dec T) ∘ map f) ∘ dec T = bindd (g ⋆5 f)
      rewrite (fun_map_map (F := T)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map g ∘ join ∘ map (shift T) ∘ dec T
∘ map (dec T ∘ f) ∘ dec T = bindd (g ⋆5 f)
      change (?rest ∘ dec T ∘ map (F := T) (dec T ∘ f) ∘ dec T)
        with (rest ∘ (dec T ∘ map (F := T) (dec T ∘ f) ∘ dec T)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map g ∘ join ∘ map (shift T)
∘ (dec T ∘ map (dec T ∘ f) ∘ dec T) = bindd (g ⋆5 f)
      rewrite <- (cobind_dec T).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map g ∘ join ∘ map (shift T)
∘ (map (cobind (dec T ∘ f)) ∘ dec T) = bindd (g ⋆5 f)
      reassociate <-.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map g ∘ join ∘ map (shift T)
∘ map (cobind (dec T ∘ f)) ∘ dec T = bindd (g ⋆5 f)
      change (?g ∘ map (shift T) ∘ map (cobind (W := prod W) (dec T ∘ f)) ∘ ?h)
        with (g ∘ (map (shift T) ∘ map (cobind (W := prod W) (dec T ∘ f))) ∘ h).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map g ∘ join
∘ (map (shift T) ∘ map (cobind (dec T ∘ f))) ∘ dec T =
bindd (g ⋆5 f)
      rewrite (fun_map_map (F := T)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map g ∘ join
∘ map (shift T ∘ cobind (dec T ∘ f)) ∘ dec T =
bindd (g ⋆5 f)
      unfold bindd.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map g ∘ join
∘ map (shift T ∘ cobind (dec T ∘ f)) ∘ dec T =
join ∘ map (g ⋆5 f) ∘ dec T
      change (?h ∘ map g ∘ join ∘ map (shift T ∘ cobind (W := prod W) (dec T ∘ f)) ∘ ?i)
        with (h ∘ (map g ∘ join ∘ map (shift T ∘ cobind (W := prod W) (dec T ∘ f))) ∘ i).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join
∘ (map g ∘ join ∘ map (shift T ∘ cobind (dec T ∘ f)))
∘ dec T = join ∘ map (g ⋆5 f) ∘ dec T
      fequal.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join
∘ (map g ∘ join ∘ map (shift T ∘ cobind (dec T ∘ f))) =
join ∘ map (g ⋆5 f)
      unfold kc5, bindd, preincr.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join
∘ (map g ∘ join ∘ map (shift T ∘ cobind (dec T ∘ f))) =
join
∘ map
    (fun '(w, a) =>
     (join ∘ map (g ∘ incr w) ∘ dec T) (f (w, a)))
      rewrite natural.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join
∘ (join ∘ map g ∘ map (shift T ∘ cobind (dec T ∘ f))) =
join
∘ map
    (fun '(w, a) =>
     (join ∘ map (g ∘ incr w) ∘ dec T) (f (w, a)))
      reassociate ->.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join
∘ (join ∘ (map g ∘ map (shift T ∘ cobind (dec T ∘ f)))) =
join
∘ map
    (fun '(w, a) =>
     (join ∘ map (g ∘ incr w) ∘ dec T) (f (w, a))) unfold_ops @Map_compose.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join
∘ (join
   ∘ (map (map g) ∘ map (shift T ∘ cobind (dec T ∘ f)))) =
join
∘ map
    (fun '(w, a) =>
     (join ∘ map (g ∘ incr w) ∘ dec T) (f (w, a))) unfold_compose_in_compose.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join
∘ (join
   ∘ (map (map g) ∘ map (shift T ∘ cobind (dec T ∘ f)))) =
join
∘ map
    (fun '(w, a) =>
     (join ∘ map (g ∘ incr w) ∘ dec T) (f (w, a)))
      rewrite (fun_map_map (F := T)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join
∘ (join ∘ map (map g ∘ (shift T ∘ cobind (dec T ∘ f)))) =
join
∘ map
    (fun '(w, a) =>
     (join ∘ map (g ∘ incr w) ∘ dec T) (f (w, a)))
      replace (fun '(w, a) => (join (T := T) ∘ map (F := T) (g ∘ incr w) ∘ dec T) (f (w, a)))
        with (join (T := T) ∘ (fun '(w, a) => (map (F := T) (g ∘ incr w) ∘ dec T) (f (w, a))))
        by (ext [? ?]; reflexivity).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join
∘ (join ∘ map (map g ∘ (shift T ∘ cobind (dec T ∘ f)))) =
join
∘ map
    (join
     ∘ (fun '(w, a) =>
        (map (g ∘ incr w) ∘ dec T) (f (w, a))))
      reassociate <-.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ join
∘ map (map g ∘ (shift T ∘ cobind (dec T ∘ f))) =
join
∘ map
    (join
     ∘ (fun '(w, a) =>
        (map (g ∘ incr w) ∘ dec T) (f (w, a))))
      #[local] Set Keyed Unification.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ join
∘ map (map g ∘ (shift T ∘ cobind (dec T ∘ f))) =
join
∘ map
    (join
     ∘ (fun '(w, a) =>
        (map (g ∘ incr w) ∘ dec T) (f (w, a))))
      rewrite (mon_join_join (T := T)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map join
∘ map (map g ∘ (shift T ∘ cobind (dec T ∘ f))) =
join
∘ map
    (join
     ∘ (fun '(w, a) =>
        (map (g ∘ incr w) ∘ dec T) (f (w, a))))
      #[local] Unset Keyed Unification.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ map join
∘ map (map g ∘ (shift T ∘ cobind (dec T ∘ f))) =
join
∘ map
    (join
     ∘ (fun '(w, a) =>
        (map (g ∘ incr w) ∘ dec T) (f (w, a))))
      reassociate ->.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join
∘ (map join
   ∘ map (map g ∘ (shift T ∘ cobind (dec T ∘ f)))) =
join
∘ map
    (join
     ∘ (fun '(w, a) =>
        (map (g ∘ incr w) ∘ dec T) (f (w, a))))
      fequal.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
map join
∘ map (map g ∘ (shift T ∘ cobind (dec T ∘ f))) =
map
  (join
   ∘ (fun '(w, a) =>
      (map (g ∘ incr w) ∘ dec T) (f (w, a)))) unfold_compose_in_compose.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
map join
∘ map (map g ∘ (shift T ∘ cobind (dec T ∘ f))) =
map
  (join
   ∘ (fun '(w, a) =>
      (map (g ∘ incr w) ∘ dec T) (f (w, a))))
      rewrite (fun_map_map (F := T)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
map (join ∘ (map g ∘ (shift T ∘ cobind (dec T ∘ f)))) =
map
  (join
   ∘ (fun '(w, a) =>
      (map (g ∘ incr w) ∘ dec T) (f (w, a))))
      fequal.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
join ∘ (map g ∘ (shift T ∘ cobind (dec T ∘ f))) =
join
∘ (fun '(w, a) =>
   (map (g ∘ incr w) ∘ dec T) (f (w, a))) fequal.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
map g ∘ (shift T ∘ cobind (dec T ∘ f)) =
(fun '(w, a) => (map (g ∘ incr w) ∘ dec T) (f (w, a))) ext [w a].
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
w: W
a: A
(map g ∘ (shift T ∘ cobind (dec T ∘ f))) (w, a) =
(map (g ∘ incr w) ∘ dec T) (f (w, a))
      unfold shift, compose; cbn.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
w: W
a: A
map g
  (map (uncurry incr)
     (map (pair w) (dec T (f (w, a))))) =
map (g ○ incr w) (dec T (f (w, a)))
      compose near (dec T (f (w, a))) on left.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
w: W
a: A
map g
  ((map (uncurry incr) ∘ map (pair w))
     (dec T (f (w, a)))) =
map (g ○ incr w) (dec T (f (w, a)))
      rewrite (fun_map_map (F := T)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
w: W
a: A
map g (map (uncurry incr ∘ pair w) (dec T (f (w, a)))) =
map (g ○ incr w) (dec T (f (w, a)))
      compose near (dec T (f (w, a))) on left.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
w: W
a: A
(map g ∘ map (uncurry incr ∘ pair w))
  (dec T (f (w, a))) =
map (g ○ incr w) (dec T (f (w, a)))
      rewrite (fun_map_map (F := T)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B, C: Type
g: W * B -> T C
f: W * A -> T B
w: W
a: A
map (g ∘ (uncurry incr ∘ pair w)) (dec T (f (w, a))) =
map (g ○ incr w) (dec T (f (w, a)))
      reflexivity.
    Qed.

    (** *** Unit law *)
    (******************************************************************)
    Lemma bindd_comp_ret `(f: W * A -> T B):
      bindd f ∘ ret = f ∘ pair Ƶ.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B: Type
f: W * A -> T B
bindd f ∘ ret = f ∘ pair Ƶ
    Proof.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B: Type
f: W * A -> T B
bindd f ∘ ret = f ∘ pair Ƶ
      intros.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B: Type
f: W * A -> T B
bindd f ∘ ret = f ∘ pair Ƶ unfold_ops Bindd_Categorical.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B: Type
f: W * A -> T B
join ∘ map f ∘ dec T ∘ ret = f ∘ pair Ƶ
      reassociate -> on left.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B: Type
f: W * A -> T B
join ∘ map f ∘ (dec T ∘ ret) = f ∘ pair Ƶ
      rewrite (dmon_ret (W := W) (T := T)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B: Type
f: W * A -> T B
join ∘ map f ∘ (ret ∘ pair Ƶ) = f ∘ pair Ƶ
      reassociate <- on left.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B: Type
f: W * A -> T B
join ∘ map f ∘ ret ∘ pair Ƶ = f ∘ pair Ƶ
      reassociate -> near (ret (A := W * A)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B: Type
f: W * A -> T B
join ∘ (map f ∘ ret) ∘ pair Ƶ = f ∘ pair Ƶ
      rewrite (natural (G := T) (ϕ := @ret T _)).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B: Type
f: W * A -> T B
join ∘ (ret ∘ map f) ∘ pair Ƶ = f ∘ pair Ƶ
      reassociate <-.
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B: Type
f: W * A -> T B
join ∘ ret ∘ map f ∘ pair Ƶ = f ∘ pair Ƶ rewrite (mon_join_ret _).
T: Type -> Type
W: Type
H: Map T
H0: Return T
H1: Join T
H2: Decorate W T
H3: Monoid_op W
H4: Monoid_unit W
H5: Categorical.DecoratedMonad.DecoratedMonad W T
A, B: Type
f: W * A -> T B
id ∘ map f ∘ pair Ƶ = f ∘ pair Ƶ
      reflexivity.
    Qed.

    (** ** Typeclass Instances *)
    (**************************************************************** **)
    #[export] Instance:
      Kleisli.DecoratedMonad.DecoratedRightPreModule W T T :=
      {| kdmod_bindd1 := @bindd_id;
         kdmod_bindd2 := @bindd_bindd;
      |}.

    #[export] Instance:
      Kleisli.DecoratedMonad.DecoratedMonad W T
      :=
      {| kdm_bindd0 := @bindd_comp_ret;
         kdm_monoid := dmon_monoid;
      |}.

  End with_monad.

End DerivedInstances.