From Tealeaves Require Import
  Classes.Categorical.DecoratedMonad
  Classes.Kleisli.DecoratedMonad
  Classes.Kleisli.Comonad.

Import DecoratedMonad.Notations.
Import Product.Notations.
Import Monoid.Notations.
Import Functor.Notations.
Import Comonad.Notations.

#[local] Notation "( X  × )" := (prod X): function_scope.
#[local] Generalizable Variables T A B C.

(** * Categorical Decorated monads from Kleisli Decorated Monads *)
(**********************************************************************)

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

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

    (*
      #[export] Instance Map_Bindd: Map T :=
      fun A B f => bindd (ret ∘ f ∘ extract).
     *)

    #[export] Instance Join_Bindd: Join T :=
      fun A => bindd (B := A) (A := T A) (extract (W := (W ×))).

    #[export] Instance Decorate_Bindd: Decorate W T :=
      fun A => bindd (ret (A := W * A)).

  End operations.
End DerivedOperations.

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

  Section with_monad.

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

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

    (** *** Functor Laws *)
    (******************************************************************)
    Lemma map_id: forall (A: Type),
        map (@id A) = @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, map id = 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, map id = id
      intros.
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
A: Type
map id = id unfold_ops @Map_Bindd.
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
A: Type
bindd (ret ∘ id ∘ extract) = id
      change (ret ∘ id) with (ret (A := 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
A: Type
bindd (ret ∘ extract) = id
      now rewrite (kdmod_bindd1 (T := T)).
    Qed.

    Lemma map_map: forall (A B C: Type) (f: A -> B) (g: B -> C),
        map g ∘ map f = map (F := T) (g ∘ 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) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ 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) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
      intros.
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
A, B, C: Type
f: A -> B
g: B -> C
map g ∘ map f = map (g ∘ f) unfold_ops @Map_Bindd.
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
A, B, C: Type
f: A -> B
g: B -> C
bindd (ret ∘ g ∘ extract) ∘ bindd (ret ∘ f ∘ extract) =
bindd (ret ∘ (g ∘ f) ∘ extract)
      rewrite (kdmod_bindd2 (T := T)).
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
A, B, C: Type
f: A -> B
g: B -> C
bindd (ret ∘ g ∘ extract ⋆5 ret ∘ f ∘ extract) =
bindd (ret ∘ (g ∘ f) ∘ extract)
      rewrite kc5_00.
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
A, B, C: Type
f: A -> B
g: B -> C
bindd (ret ∘ g ∘ f ∘ extract) =
bindd (ret ∘ (g ∘ f) ∘ extract)
      reflexivity.
    Qed.

    #[local] Instance: Classes.Functor.Functor T :=
      {| fun_map_id := map_id;
         fun_map_map := map_map;
      |}.

    (** *** Monad Laws *)
    (******************************************************************)
    Lemma ret_natural: Natural (@ret T _).
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
Natural (@ret T Return_T)
    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
Natural (@ret T Return_T)
      constructor.
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
Functor (fun A : Type => 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
Functor T
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 : Type) (f : A -> B),
map f ∘ ret = ret ∘ map 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
Functor (fun A : Type => A) typeclasses eauto.
      -
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
Functor T typeclasses eauto.
      -
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 : Type) (f : A -> B),
map f ∘ ret = ret ∘ map f intros.
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
A, B: Type
f: A -> B
map f ∘ ret = ret ∘ map f unfold_ops @Map_Bindd.
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
A, B: Type
f: A -> B
bindd (ret ∘ f ∘ extract) ∘ ret = ret ∘ map f
        rewrite (kdm_bindd0 (T := T)).
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
A, B: Type
f: A -> B
ret ∘ f ∘ extract ∘ ret = ret ∘ map f
        reflexivity.
    Qed.

    Lemma join_natural: Natural (@join T _).
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
Natural (@join T (Join_Bindd W T))
    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
Natural (@join T (Join_Bindd W T))
      constructor.
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
Functor (T ∘ T)
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
Functor T
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 : Type) (f : A -> B),
map f ∘ join = join ∘ map 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
Functor (T ∘ T) typeclasses eauto.
      -
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
Functor T typeclasses eauto.
      -
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 : Type) (f : A -> B),
map f ∘ join = join ∘ map f intros.
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
A, B: Type
f: A -> B
map f ∘ join = join ∘ map f
        unfold_ops @Map_compose.
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
A, B: Type
f: A -> B
map f ∘ join = join ∘ map (map f)
        unfold_ops @Map_Bindd.
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
A, B: Type
f: A -> B
bindd (ret ∘ f ∘ extract) ∘ join =
join
∘ bindd (ret ∘ bindd (ret ∘ f ∘ extract) ∘ extract)
        unfold_ops @Join_Bindd.
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
A, B: Type
f: A -> B
bindd (ret ∘ f ∘ extract) ∘ bindd extract =
bindd extract
∘ bindd (ret ∘ bindd (ret ∘ f ∘ extract) ∘ extract)
        unfold_compose_in_compose.
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
A, B: Type
f: A -> B
bindd (ret ∘ f ∘ extract) ∘ bindd extract =
bindd extract
∘ bindd (ret ∘ bindd (ret ∘ f ∘ extract) ∘ extract)
        rewrite (kdmod_bindd2 (T := T)). (* left *)
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
A, B: Type
f: A -> B
bindd (ret ∘ f ∘ extract ⋆5 extract) =
bindd extract
∘ bindd (ret ∘ bindd (ret ∘ f ∘ extract) ∘ extract)
        rewrite (kdmod_bindd2 (T := T)). (* right *)
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
A, B: Type
f: A -> B
bindd (ret ∘ f ∘ extract ⋆5 extract) =
bindd
  (extract
   ⋆5 ret ∘ bindd (ret ∘ f ∘ extract) ∘ extract)
        rewrite kc5_05.
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
A, B: Type
f: A -> B
bindd (map f ∘ extract) =
bindd
  (extract
   ⋆5 ret ∘ bindd (ret ∘ f ∘ extract) ∘ extract)
        rewrite kc5_50.
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
A, B: Type
f: A -> B
bindd (map f ∘ extract) =
bindd (extract ∘ map (bindd (ret ∘ f ∘ extract)))
        rewrite (map_to_cobind (W := prod W)).
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
A, B: Type
f: A -> B
bindd (map f ∘ extract) =
bindd
  (extract
   ∘ cobind (bindd (ret ∘ f ∘ extract) ∘ extract))
        rewrite kcom_cobind0.
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
A, B: Type
f: A -> B
bindd (map f ∘ extract) =
bindd (bindd (ret ∘ f ∘ extract) ∘ extract)
        reflexivity.
    Qed.

    Lemma join_ret:
      `(join (T := T) ∘ ret (T := T) = @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, join ∘ ret = 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, join ∘ ret = id
      intros.
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
A: Type
join ∘ ret = id
      unfold_ops @Join_Bindd.
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
A: Type
bindd extract ∘ ret = id
      unfold_compose_in_compose.
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
A: Type
bindd extract ∘ ret = id
      rewrite (kdm_bindd0 (T := T)).
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
A: Type
extract ∘ ret = id
      reflexivity.
    Qed.

    Lemma join_map_ret:
      `(join (T := T) ∘ map (F := T) ret = @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, join ∘ map ret = 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, join ∘ map ret = id
      intros.
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
A: Type
join ∘ map ret = id
      unfold_ops @Map_Bindd.
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
A: Type
join ∘ bindd (ret ∘ ret ∘ extract) = id
      unfold_ops @Join_Bindd.
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
A: Type
bindd extract ∘ bindd (ret ∘ ret ∘ extract) = id
      unfold_compose_in_compose.
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
A: Type
bindd extract ∘ bindd (ret ∘ ret ∘ extract) = id
      rewrite (kdmod_bindd2 (T := T)).
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
A: Type
bindd (extract ⋆5 ret ∘ ret ∘ extract) = id
      rewrite kc5_50.
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
A: Type
bindd (extract ∘ map ret) = id
      rewrite map_to_cobind.
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
A: Type
bindd (extract ∘ cobind (ret ∘ extract)) = id
      rewrite kcom_cobind0.
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
A: Type
bindd (ret ∘ extract) = id
      rewrite (kdmod_bindd1 (T := T)).
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
A: Type
id = id
      reflexivity.
    Qed.

    Lemma join_join:
      `(join ∘ join (T := T) (A := T A) =
          join ∘ map (F := T) join).
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, join ∘ join = join ∘ map join
    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, join ∘ join = join ∘ map join
      intros.
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
A: Type
join ∘ join = join ∘ map join
      (* Merge LHS *)
      unfold_ops @Join_Bindd.
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
A: Type
bindd extract ∘ bindd extract =
bindd extract ∘ map (bindd extract)
      unfold_compose_in_compose.
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
A: Type
bindd extract ∘ bindd extract =
bindd extract ∘ map (bindd extract)
      rewrite (kdmod_bindd2 (T := T)).
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
A: Type
bindd (extract ⋆5 extract) =
bindd extract ∘ map (bindd extract)
      (* Merge RHS *)
      unfold_ops @Map_Bindd.
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
A: Type
bindd (extract ⋆5 extract) =
bindd extract ∘ bindd (ret ∘ bindd extract ∘ extract)
      rewrite (kdmod_bindd2 (T := T)).
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
A: Type
bindd (extract ⋆5 extract) =
bindd (extract ⋆5 ret ∘ bindd extract ∘ extract)
      fequal.
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
A: Type
extract ⋆5 extract =
extract ⋆5 ret ∘ bindd extract ∘ extract
      rewrite kc5_50.
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
A: Type
extract ⋆5 extract = extract ∘ map (bindd extract)
      rewrite map_to_cobind.
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
A: Type
extract ⋆5 extract =
extract ∘ cobind (bindd extract ∘ extract)
      rewrite kcom_cobind0.
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
A: Type
extract ⋆5 extract = bindd extract ∘ extract
      unfold kc5.
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
A: Type
(fun '(w, a) => bindd (extract ⦿ w) (extract (w, a))) =
bindd extract ∘ extract
      cbn.
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
A: Type
(fun '(w, a) => bindd (extract ⦿ w) a) =
bindd extract ∘ extract
      ext [w t].
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
A: Type
w: W
t: T (T A)
bindd (extract ⦿ w) t =
(bindd extract ∘ extract) (w, t)
      setoid_rewrite extract_preincr.
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
A: Type
w: W
t: T (T A)
bindd extract t = (bindd extract ∘ extract) (w, t)
      reflexivity.
    Qed.

    #[local] Instance: Categorical.Monad.Monad T :=
      {| Monad.mon_ret_natural := ret_natural;
         mon_join_natural := join_natural;
         mon_join_ret := join_ret;
         mon_join_map_ret := join_map_ret;
         mon_join_join := join_join;
      |}.

    (** *** Decorated Functor Laws *)
    (******************************************************************)
    Lemma dec_dec: forall (A: Type),
        dec T ∘ dec T =
          map (F := T) (cojoin (W := (W ×))) ∘ dec T (A := 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, dec T ∘ dec T = map cojoin ∘ dec T
    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, dec T ∘ dec T = map cojoin ∘ dec T
      intros.
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
A: Type
dec T ∘ dec T = map cojoin ∘ dec T
      (* Merge LHS *)
      unfold_ops @Decorate_Bindd.
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
A: Type
bindd ret ∘ bindd ret = map cojoin ∘ bindd ret
      rewrite (kdmod_bindd2 (T := T)).
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
A: Type
bindd (ret ⋆5 ret) = map cojoin ∘ bindd ret
      (* Merge RHS *)
      unfold_ops @Map_Bindd.
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
A: Type
bindd (ret ⋆5 ret) =
bindd (ret ∘ cojoin ∘ extract) ∘ bindd ret
      rewrite (kdmod_bindd2 (T := T)).
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
A: Type
bindd (ret ⋆5 ret) =
bindd (ret ∘ cojoin ∘ extract ⋆5 ret)
      fequal.
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
A: Type
ret ⋆5 ret = ret ∘ cojoin ∘ extract ⋆5 ret
      rewrite kc5_05.
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
A: Type
ret ⋆5 ret = map cojoin ∘ ret
      change (ret (T := T) (A := W * A)) with
        (ret (T := T) (A := W * A) ∘ id) at 1.
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
A: Type
ret ⋆5 ret ∘ id = map cojoin ∘ ret
      rewrite kc5_51.
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
A: Type
ret ⋆1 id = map cojoin ∘ ret
      unfold kc1.
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
A: Type
ret ∘ cobind id = map cojoin ∘ ret
      rewrite (natural (ϕ := @ret T _)).
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
A: Type
ret ∘ cobind id = ret ∘ map cojoin
      reflexivity.
    Qed.

    Lemma dec_extract: forall (A: Type),
        map (F := T) (extract (W := (W ×))) ∘ dec T = @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, map extract ∘ dec T = 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, map extract ∘ dec T = id
      intros.
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
A: Type
map extract ∘ dec T = id
      unfold_ops @Decorate_Bindd.
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
A: Type
map extract ∘ bindd ret = id
      unfold_ops @Map_Bindd.
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
A: Type
bindd (ret ∘ extract ∘ extract) ∘ bindd ret = id
      rewrite (kdmod_bindd2 (T := T)).
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
A: Type
bindd (ret ∘ extract ∘ extract ⋆5 ret) = id
      change (ret (A := W * A)) with (ret (A := W * A) ∘ @id (W * 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
A: Type
bindd (ret ∘ extract ∘ extract ⋆5 ret ∘ id) = id
      rewrite kc5_05.
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
A: Type
bindd (map extract ∘ (ret ∘ id)) = id
      change (?f ∘ id) with 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
A: Type
bindd (map extract ∘ ret) = id
      rewrite (natural (ϕ := @ret T _)).
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
A: Type
bindd (ret ∘ map extract) = id
      apply (kdmod_bindd1 (T := T)).
    Qed.

    Lemma dec_natural: Natural (@dec W T _).
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
Natural (@dec W T (Decorate_Bindd W T))
    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
Natural (@dec W T (Decorate_Bindd W T))
      constructor.
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
Functor T
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
Functor (T ○ (W × ))
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 : Type) (f : A -> B),
map f ∘ dec T = dec T ∘ map 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
Functor T typeclasses eauto.
      -
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
Functor (T ○ (W × )) typeclasses eauto.
      -
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 : Type) (f : A -> B),
map f ∘ dec T = dec T ∘ map f intros.
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
A, B: Type
f: A -> B
map f ∘ dec T = dec T ∘ map f unfold_ops @Map_compose.
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
A, B: Type
f: A -> B
map (map f) ∘ dec T = dec T ∘ map f
        unfold_ops @Map_Bindd.
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
A, B: Type
f: A -> B
bindd (ret ∘ map f ∘ extract) ∘ dec T =
dec T ∘ bindd (ret ∘ f ∘ extract)
        unfold_ops @Decorate_Bindd.
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
A, B: Type
f: A -> B
bindd (ret ∘ map f ∘ extract) ∘ bindd ret =
bindd ret ∘ bindd (ret ∘ f ∘ extract)
        rewrite (kdmod_bindd2 (T := T)).
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
A, B: Type
f: A -> B
bindd (ret ∘ map f ∘ extract ⋆5 ret) =
bindd ret ∘ bindd (ret ∘ f ∘ extract)
        rewrite (kdmod_bindd2 (T := T)).
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
A, B: Type
f: A -> B
bindd (ret ∘ map f ∘ extract ⋆5 ret) =
bindd (ret ⋆5 ret ∘ f ∘ extract)
        fequal.
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
A, B: Type
f: A -> B
ret ∘ map f ∘ extract ⋆5 ret =
ret ⋆5 ret ∘ f ∘ extract
        rewrite kc5_05.
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
A, B: Type
f: A -> B
map (map f) ∘ ret = ret ⋆5 ret ∘ f ∘ extract
        rewrite kc5_50.
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
A, B: Type
f: A -> B
map (map f) ∘ ret = ret ∘ map f
        rewrite (natural (ϕ := @ret T _)).
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
A, B: Type
f: A -> B
ret ∘ map (map f) = ret ∘ map f
        reflexivity.
    Qed.

    #[local] Instance:
      Categorical.DecoratedFunctor.DecoratedFunctor W T :=
      {| dfun_dec_natural := dec_natural;
         dfun_dec_dec := dec_dec;
         dfun_dec_extract := dec_extract;
      |}.

    (** *** Decorated Monad Laws *)
    (******************************************************************)
    Lemma dmon_ret_: forall (A: Type),
        dec T ∘ ret (T := T) = ret ∘ pair Ƶ (B := 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, dec T ∘ ret = ret ∘ pair Ƶ
    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, dec T ∘ ret = ret ∘ pair Ƶ
      intros.
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
A: Type
dec T ∘ ret = ret ∘ pair Ƶ
      unfold_ops @Decorate_Bindd.
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
A: Type
bindd ret ∘ ret = ret ∘ pair Ƶ
      now rewrite (kdm_bindd0 (T := T)).
    Qed.

    Lemma dmon_join_: forall (A: Type),
        dec T ∘ join (T := T) (A:=A) =
          join (T := T) ∘ map (F := T)
            (shift T) ∘ dec T ∘ map (F := T) (dec T).
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,
dec T ∘ join =
join ∘ map (shift T) ∘ dec T ∘ map (dec T)
    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,
dec T ∘ join =
join ∘ map (shift T) ∘ dec T ∘ map (dec T)
      intros.
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
A: Type
dec T ∘ join =
join ∘ map (shift T) ∘ dec T ∘ map (dec T)
      unfold shift, strength.
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
A: Type
dec T ∘ join =
join
∘ map
    (map (uncurry incr)
     ∘ (fun '(a, t) => map (pair a) t)) ∘ dec T
∘ map (dec T)
      unfold_ops @Decorate_Bindd.
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
A: Type
bindd ret ∘ join =
join
∘ map
    (map (uncurry incr)
     ∘ (fun '(a, t) => map (pair a) t)) ∘ bindd ret
∘ map (bindd ret)
      unfold_ops @Map_Bindd.
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
A: Type
bindd ret ∘ join =
join
∘ bindd
    (ret
     ∘ (bindd (ret ∘ uncurry incr ∘ extract)
        ∘ (fun '(a, t) =>
           bindd (ret ∘ pair a ∘ extract) t))
     ∘ extract) ∘ bindd ret
∘ bindd (ret ∘ bindd ret ∘ extract)
      unfold_ops @Join_Bindd.
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
A: Type
bindd ret ∘ bindd extract =
bindd extract
∘ bindd
    (ret
     ∘ (bindd (ret ∘ uncurry incr ∘ extract)
        ∘ (fun '(a, t) =>
           bindd (ret ∘ pair a ∘ extract) t))
     ∘ extract) ∘ bindd ret
∘ bindd (ret ∘ bindd ret ∘ extract)
      unfold_compose_in_compose.
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
A: Type
bindd ret ∘ bindd extract =
bindd extract
∘ bindd
    (ret
     ∘ (bindd (ret ∘ uncurry incr ∘ extract)
        ∘ (fun '(a, t) =>
           bindd (ret ∘ pair a ∘ extract) t))
     ∘ extract) ∘ bindd ret
∘ bindd (ret ∘ bindd ret ∘ extract)
      (* Fuse LHS *)
      rewrite kdmod_bindd2 at 1.
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
A: Type
bindd (ret ⋆5 extract) =
bindd extract
∘ bindd
    (ret
     ∘ (bindd (ret ∘ uncurry incr ∘ extract)
        ∘ (fun '(a, t) =>
           bindd (ret ∘ pair a ∘ extract) t))
     ∘ extract) ∘ bindd ret
∘ bindd (ret ∘ bindd ret ∘ extract)
      change (extract (W := (W ×)) (A := T A))
        with (id ∘ extract (W := (W ×)) (A := T A)) at 1.
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
A: Type
bindd (ret ⋆5 id ∘ extract) =
bindd extract
∘ bindd
    (ret
     ∘ (bindd (ret ∘ uncurry incr ∘ extract)
        ∘ (fun '(a, t) =>
           bindd (ret ∘ pair a ∘ extract) t))
     ∘ extract) ∘ bindd ret
∘ bindd (ret ∘ bindd ret ∘ extract)
      try rewrite kc5_54.
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
A: Type
bindd ((fun '(w, t) => bindd (ret ⦿ w) t) ∘ map id) =
bindd extract
∘ bindd
    (ret
     ∘ (bindd (ret ∘ uncurry incr ∘ extract)
        ∘ (fun '(a, t) =>
           bindd (ret ∘ pair a ∘ extract) t))
     ∘ extract) ∘ bindd ret
∘ bindd (ret ∘ bindd ret ∘ extract)
      rewrite fun_map_id.
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
A: Type
bindd ((fun '(w, t) => bindd (ret ⦿ w) t) ∘ id) =
bindd extract
∘ bindd
    (ret
     ∘ (bindd (ret ∘ uncurry incr ∘ extract)
        ∘ (fun '(a, t) =>
           bindd (ret ∘ pair a ∘ extract) t))
     ∘ extract) ∘ bindd ret
∘ bindd (ret ∘ bindd ret ∘ extract)
      change (?f ∘ id) with 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
A: Type
bindd (fun '(w, t) => bindd (ret ⦿ w) t) =
bindd extract
∘ bindd
    (ret
     ∘ (bindd (ret ∘ uncurry incr ∘ extract)
        ∘ (fun '(a, t) =>
           bindd (ret ∘ pair a ∘ extract) t))
     ∘ extract) ∘ bindd ret
∘ bindd (ret ∘ bindd ret ∘ extract)
      (* Fuse RHS *)
      rewrite kdmod_bindd2.
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
A: Type
bindd (fun '(w, t) => bindd (ret ⦿ w) t) =
bindd
  (extract
   ⋆5 ret
      ∘ (bindd (ret ∘ uncurry incr ∘ extract)
         ∘ (fun '(a, t) =>
            bindd (ret ∘ pair a ∘ extract) t))
      ∘ extract) ∘ bindd ret
∘ bindd (ret ∘ bindd ret ∘ extract)
      reassociate -> near (extract (W := (W ×))).
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
A: Type
bindd (fun '(w, t) => bindd (ret ⦿ w) t) =
bindd
  (extract
   ⋆5 ret
      ∘ (bindd (ret ∘ uncurry incr ∘ extract)
         ∘ (fun '(a, t) =>
            bindd (ret ∘ pair a ∘ extract) t)
         ∘ extract)) ∘ bindd ret
∘ bindd (ret ∘ (bindd ret ∘ extract))
      rewrite kc5_51.
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
A: Type
bindd (fun '(w, t) => bindd (ret ⦿ w) t) =
bindd
  (extract
   ⋆1 bindd (ret ∘ uncurry incr ∘ extract)
      ∘ (fun '(a, t) =>
         bindd (ret ∘ pair a ∘ extract) t) ∘ extract)
∘ bindd ret ∘ bindd (ret ∘ (bindd ret ∘ extract))
      rewrite kc1_id_l.
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
A: Type
bindd (fun '(w, t) => bindd (ret ⦿ w) t) =
bindd
  (bindd (ret ∘ uncurry incr ∘ extract)
   ∘ (fun '(a, t) => bindd (ret ∘ pair a ∘ extract) t)
   ∘ extract) ∘ bindd ret
∘ bindd (ret ∘ (bindd ret ∘ extract))
      rewrite kdmod_bindd2.
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
A: Type
bindd (fun '(w, t) => bindd (ret ⦿ w) t) =
bindd
  (bindd (ret ∘ uncurry incr ∘ extract)
   ∘ (fun '(a, t) => bindd (ret ∘ pair a ∘ extract) t)
   ∘ extract ⋆5 ret)
∘ bindd (ret ∘ (bindd ret ∘ extract))
      change (ret (T := T) ( A:= (W ×) (T ((W ×) A))))
        with ((ret (T := T) (A := (W ×) (T ((W ×) A)))) ∘ id).
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
A: Type
bindd (fun '(w, t) => bindd (ret ⦿ w) t) =
bindd
  (bindd (ret ∘ uncurry incr ∘ extract)
   ∘ (fun '(a, t) => bindd (ret ∘ pair a ∘ extract) t)
   ∘ extract ⋆5 ret ∘ id)
∘ bindd (ret ∘ (bindd ret ∘ extract))
      rewrite kc5_51.
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
A: Type
bindd (fun '(w, t) => bindd (ret ⦿ w) t) =
bindd
  (bindd (ret ∘ uncurry incr ∘ extract)
   ∘ (fun '(a, t) => bindd (ret ∘ pair a ∘ extract) t)
   ∘ extract ⋆1 id)
∘ bindd (ret ∘ (bindd ret ∘ extract))
      rewrite kc1_01.
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
A: Type
bindd (fun '(w, t) => bindd (ret ⦿ w) t) =
bindd
  (bindd (ret ∘ uncurry incr ∘ extract)
   ∘ (fun '(a, t) => bindd (ret ∘ pair a ∘ extract) t)
   ∘ id) ∘ bindd (ret ∘ (bindd ret ∘ extract))
      change (?f ∘ id) with 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
A: Type
bindd (fun '(w, t) => bindd (ret ⦿ w) t) =
bindd
  (bindd (ret ∘ uncurry incr ∘ extract)
   ∘ (fun '(a, t) => bindd (ret ∘ pair a ∘ extract) t))
∘ bindd (ret ∘ (bindd ret ∘ extract))
      rewrite kdmod_bindd2.
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
A: Type
bindd (fun '(w, t) => bindd (ret ⦿ w) t) =
bindd
  (bindd (ret ∘ uncurry incr ∘ extract)
   ∘ (fun '(a, t) => bindd (ret ∘ pair a ∘ extract) t)
   ⋆5 ret ∘ (bindd ret ∘ extract))
      rewrite kc5_51.
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
A: Type
bindd (fun '(w, t) => bindd (ret ⦿ w) t) =
bindd
  (bindd (ret ∘ uncurry incr ∘ extract)
   ∘ (fun '(a, t) => bindd (ret ∘ pair a ∘ extract) t)
   ⋆1 bindd ret ∘ extract)
      rewrite kc1_10.
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
A: Type
bindd (fun '(w, t) => bindd (ret ⦿ w) t) =
bindd
  (bindd (ret ∘ uncurry incr ∘ extract)
   ∘ (fun '(a, t) => bindd (ret ∘ pair a ∘ extract) t)
   ∘ map (bindd ret))
      (* Now compare inner functions *)
      fequal.
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
A: Type
(fun '(w, t) => bindd (ret ⦿ w) t) =
bindd (ret ∘ uncurry incr ∘ extract)
∘ (fun '(a, t) => bindd (ret ∘ pair a ∘ extract) t)
∘ map (bindd ret)
      ext [w t].
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
A: Type
w: W
t: T A
bindd (ret ⦿ w) t =
(bindd (ret ∘ uncurry incr ∘ extract)
 ∘ (fun '(a, t) => bindd (ret ∘ pair a ∘ extract) t)
 ∘ map (bindd ret)) (w, t)
      do 2 (unfold compose; cbn).
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
A: Type
w: W
t: T A
bindd (ret ⦿ w) t =
bindd
  (fun a : (W × ) ((W × ) ((W × ) A)) =>
   ret (uncurry incr (extract a)))
  (bindd
     (fun a : (W × ) ((W × ) A) =>
      ret (id w, extract a)) (bindd ret t))
      compose near t on right.
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
A: Type
w: W
t: T A
bindd (ret ⦿ w) t =
bindd
  (fun a : (W × ) ((W × ) ((W × ) A)) =>
   ret (uncurry incr (extract a)))
  ((bindd
      (fun a : (W × ) ((W × ) A) =>
       ret (id w, extract a)) ∘ bindd ret) t)
      rewrite kdmod_bindd2.
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
A: Type
w: W
t: T A
bindd (ret ⦿ w) t =
bindd
  (fun a : (W × ) ((W × ) ((W × ) A)) =>
   ret (uncurry incr (extract a)))
  (bindd
     ((fun a : (W × ) ((W × ) A) =>
       ret (id w, extract a)) ⋆5 ret) t)
      change (ret (A := (W ×) A)) with (ret (A := (W ×) A) ∘ id).
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
A: Type
w: W
t: T A
bindd ((ret ∘ id) ⦿ w) t =
bindd
  (fun a : (W × ) ((W × ) ((W × ) A)) =>
   (ret ∘ id) (uncurry incr (extract a)))
  (bindd
     ((fun a : (W × ) ((W × ) A) =>
       ret (id w, extract a)) ⋆5 ret ∘ id) t)
      rewrite kc5_51.
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
A: Type
w: W
t: T A
bindd ((ret ∘ id) ⦿ w) t =
bindd
  (fun a : (W × ) ((W × ) ((W × ) A)) =>
   (ret ∘ id) (uncurry incr (extract a)))
  (bindd
     ((fun a : (W × ) ((W × ) A) =>
       ret (id w, extract a)) ⋆1 id) t)
      compose near t on right.
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
A: Type
w: W
t: T A
bindd ((ret ∘ id) ⦿ w) t =
(bindd
   (fun a : (W × ) ((W × ) ((W × ) A)) =>
    (ret ∘ id) (uncurry incr (extract a)))
 ∘ bindd
     ((fun a : (W × ) ((W × ) A) =>
       ret (id w, extract a)) ⋆1 id)) t
      rewrite kdmod_bindd2.
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
A: Type
w: W
t: T A
bindd ((ret ∘ id) ⦿ w) t =
bindd
  ((fun a : (W × ) ((W × ) ((W × ) A)) =>
    (ret ∘ id) (uncurry incr (extract a)))
   ⋆5 ((fun a : (W × ) ((W × ) A) =>
        ret (id w, extract a)) ⋆1 id)) t
      (* Now compare inner functions again *)
      fequal.
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
A: Type
w: W
t: T A
(ret ∘ id) ⦿ w =
(fun a : (W × ) ((W × ) ((W × ) A)) =>
 (ret ∘ id) (uncurry incr (extract a)))
⋆5 ((fun a : (W × ) ((W × ) A) =>
     ret (id w, extract a)) ⋆1 id)
      ext [w' 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
A: Type
w: W
t: T A
w': W
a: A
((ret ∘ id) ⦿ w) (w', a) =
((fun a : (W × ) ((W × ) ((W × ) A)) =>
  (ret ∘ id) (uncurry incr (extract a)))
 ⋆5 ((fun a : (W × ) ((W × ) A) =>
      ret (id w, extract a)) ⋆1 id)) (w', a)
      unfold preincr; unfold compose; cbn.
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
A: Type
w: W
t: T A
w': W
a: A
ret (w ● w', a) =
bindd
  ((fun a : (W × ) ((W × ) ((W × ) A)) =>
    ret (id (uncurry incr (extract a)))) ⦿ w')
  (((fun a : (W × ) ((W × ) A) =>
     ret (id w, extract a)) ⋆1 id) (w', a))
      unfold kc1; unfold_ops @Cobind_reader.
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
A: Type
w: W
t: T A
w': W
a: A
ret (w ● w', a) =
bindd
  ((fun a : (W × ) ((W × ) ((W × ) A)) =>
    ret (id (uncurry incr (extract a)))) ⦿ w')
  (((fun a : (W × ) ((W × ) A) =>
     ret (id w, extract a))
    ∘ (fun '(e, a) => (e, id (e, a)))) (w', a))
      unfold compose; cbn.
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
A: Type
w: W
t: T A
w': W
a: A
ret (w ● w', a) =
bindd
  ((fun a : (W × ) ((W × ) ((W × ) A)) =>
    ret (id (uncurry incr (extract a)))) ⦿ w')
  (ret (id w, id (w', a)))
      change (id ?x) with x.
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
A: Type
w: W
t: T A
w': W
a: A
ret (w ● w', a) =
bindd
  ((fun a : (W × ) ((W × ) ((W × ) A)) =>
    ret (uncurry incr (extract a))) ⦿ w')
  (ret (w, (w', a)))
      compose near (w, (w', 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
A: Type
w: W
t: T A
w': W
a: A
ret (w ● w', a) =
(bindd
   ((fun a : (W × ) ((W × ) ((W × ) A)) =>
     ret (uncurry incr (extract a))) ⦿ w') ∘ ret)
  (w, (w', a))
      rewrite kdm_bindd0.
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
A: Type
w: W
t: T A
w': W
a: A
ret (w ● w', a) =
((fun a : (W × ) ((W × ) ((W × ) A)) =>
  ret (uncurry incr (extract a))) ⦿ w' ∘ ret)
  (w, (w', a))
      reflexivity.
    Qed.

    #[local] Instance:
      Categorical.DecoratedMonad.DecoratedMonad W T :=
      {| dmon_ret := dmon_ret_;
         dmon_join := dmon_join_;
      |}.

  End with_monad.

End DerivedInstances.