From Tealeaves Require Export
  Classes.Monoid
  Functors.Early.Reader.

From Tealeaves Require Import
  Classes.Kleisli.Monad
  Classes.Kleisli.Comonad
  Classes.Categorical.Monad
  Classes.Categorical.Comonad
  Classes.Categorical.Bimonad.

Import Product.Notations.
Import Functor.Notations.
Import Monoid.Notations.
Import Categorical.Monad.Notations.
Import Categorical.Comonad.Notations.
Import Kleisli.Monad.Notations.
Import Kleisli.Comonad.Notations.

#[local] Generalizable Variables W T F A M.

(** * Writer monad *)
(**********************************************************************)

(** ** Categorical instance *)
(** In the even that [A] is a monoid, the product functor forms a
    monad. The return operation maps <<b>> to <<(1, b)>> where <<1>>
    is the monoid unit.  The join operation monoidally combines the
    two monoid values. *)
(**********************************************************************)
Section writer_monad.

  Context
    `{Monoid M}.

  #[export] Instance Join_writer: Join (prod M) :=
    fun (A: Type) (p: M * (M * A)) =>
      map_fst (uncurry (@monoid_op M _)) (α^-1 p).

  #[export] Instance Return_writer: Return (prod M) :=
    fun A (a: A) => (Ƶ, a).

  #[export] Instance Natural_ret_writer:
    Natural (@ret (prod M) Return_writer).
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
Natural (@ret (prod M) Return_writer)
  Proof.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
Natural (@ret (prod M) Return_writer)
    constructor; try typeclasses eauto.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (A B : Type) (f : A -> B),
map f ∘ η = η ∘ map f
    intros A B f.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A, B: Type
f: A -> B
map f ∘ η = η ∘ map f now ext a.
  Qed.

  #[export] Instance Natural_join_writer:
    Natural (@join (prod M) Join_writer).
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
Natural (@join (prod M) Join_writer)
  Proof.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
Natural (@join (prod M) Join_writer)
    constructor; try typeclasses eauto.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (A B : Type) (f : A -> B),
map f ∘ μ = μ ∘ map f
    introv.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A, B: Type
f: A -> B
map f ∘ μ = μ ∘ map f now ext [x [x' a]].
  Qed.

  #[export, program] Instance Monad_Categorical_writer:
    Monad (prod M).

  Solve Obligations with
    (intros; unfold transparent tcs; ext p;
     unfold compose in *; destruct_all_pairs;
     cbn; now simpl_monoid).

End writer_monad.

(** ** Tensor Strength Makes any <<T ∘ (W ×)>> a Monad *)
(**********************************************************************)
#[export] Instance BeckDistribution_strength
  (W: Type) (T: Type -> Type)
  `{Map_T: Map T}:
  BeckDistribution (W ×) T := (@strength T _ W).

Section strength_as_writer_distributive_law.

  Import Strength.Notations.

  Context
    `{Monoid W}.

  Lemma strength_ret_l `{Functor F}: forall A: Type,
      σ ∘ ret (T := (W ×)) (A := F A) =
        map (F := F) (ret (T := (W ×)) (A := A)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
forall A : Type, σ ∘ η = map (η)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
forall A : Type, σ ∘ η = map (η)
    reflexivity.
  Qed.

  Lemma strength_join_l `{Functor F}: forall A: Type,
      σ ∘ join (T := (W ×)) (A := F A) =
        map (F := F) (join (T := (W ×)) (A := A)) ∘
          σ ∘ map (F := (W ×)) σ.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
forall A : Type, σ ∘ μ = map (μ) ∘ σ ∘ map (σ)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
forall A : Type, σ ∘ μ = map (μ) ∘ σ ∘ map (σ)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
σ ∘ μ = map (μ) ∘ σ ∘ map (σ) ext [w1 [w2 t]].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
w1, w2: W
t: F A
(σ ∘ μ) (w1, (w2, t)) =
(map (μ) ∘ σ ∘ map (σ)) (w1, (w2, t)) unfold compose; cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
w1, w2: W
t: F A
map (pair (w1 ● w2)) (id t) =
map (μ) (map (pair (id w1)) (map (pair w2) t))
    compose near t.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
w1, w2: W
t: F A
(map (pair (w1 ● w2)) ∘ id) t =
map (μ) ((map (pair (id w1)) ∘ map (pair w2)) t) rewrite fun_map_map.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
w1, w2: W
t: F A
(map (pair (w1 ● w2)) ∘ id) t =
map (μ) (map (pair (id w1) ∘ pair w2) t)
    compose near t on right.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
w1, w2: W
t: F A
(map (pair (w1 ● w2)) ∘ id) t =
(map (μ) ∘ map (pair (id w1) ∘ pair w2)) t rewrite fun_map_map.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
w1, w2: W
t: F A
(map (pair (w1 ● w2)) ∘ id) t =
map (μ ∘ (pair (id w1) ∘ pair w2)) t
    reflexivity.
  Qed.

  Context
    `{Categorical.Monad.Monad T}.

  #[export, program] Instance BeckDistributiveLaw_strength:
    BeckDistributiveLaw (W ×) T :=
    {| bdist_join_r := strength_join T W;
       bdist_unit_r := strength_ret T W;
       bdist_join_l := strength_join_l;
       bdist_unit_l := strength_ret_l;
    |}.

  #[export] Instance Monad_Compose_Writer:
    Monad (T ∘ (W ×)) := Monad_Beck.

End strength_as_writer_distributive_law.

(** ** Writer Bimonad Instances *)
(**********************************************************************)

Section writer_bimonad_instance.

  Context
    `{Monoid W}.

  Lemma writer_dist_involution: forall (A: Type),
      bdist (prod W) (prod W) ∘ bdist (prod W) (prod W) =
        @id (W * (W * A)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type,
bdist (prod W) (prod W) ∘ bdist (prod W) (prod W) = id
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type,
bdist (prod W) (prod W) ∘ bdist (prod W) (prod W) = id
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
bdist (prod W) (prod W) ∘ bdist (prod W) (prod W) = id now ext [? [? ?]].
  Qed.

  Lemma bimonad_dist_counit_l: forall A,
      extract (W := (W ×)) (A := W * A) ∘ bdist (W ×) (W ×) =
        map (F := (W ×)) (extract (W := (W ×)) (A := A)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type,
extract ∘ bdist (prod W) (prod W) = map extract
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type,
extract ∘ bdist (prod W) (prod W) = map extract
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
extract ∘ bdist (prod W) (prod W) = map extract now ext [w1 [w2 a]].
  Qed.

  Lemma bimonad_dist_counit_r: forall A,
      map (F := (W ×))
        (extract (W := (W ×)) (A := A)) ∘ bdist (W ×) (W ×) =
        extract (W := (W ×)) (A := W * A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type,
map extract ∘ bdist (prod W) (prod W) = extract
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type,
map extract ∘ bdist (prod W) (prod W) = extract
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
map extract ∘ bdist (prod W) (prod W) = extract now ext [w1 [w2 a]].
  Qed.

  Lemma bimonad_baton: forall A,
      extract (W := (W ×)) (A := A) ∘ ret (T := (W ×)) = @id A.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type, extract ∘ η = id
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type, extract ∘ η = id
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
extract ∘ η = id reflexivity.
  Qed.

  Lemma bimonad_cup: forall A,
      cojoin (W := (W ×)) ∘ ret (T := (W ×)) =
        ret (T := (W ×)) (A := W * A) ∘ ret (T := (W ×)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type, coμ ∘ η = η ∘ η
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type, coμ ∘ η = η ∘ η
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
coμ ∘ η = η ∘ η reflexivity.
  Qed.

  Lemma bimonad_cap: forall A,
      extract (W := (W ×)) (A := A) ∘ join (T := (W ×)) =
        extract (W := (W ×)) (A := A) ∘
          extract (W := (W ×)) (A := W * A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type, extract ∘ μ = extract ∘ extract
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type, extract ∘ μ = extract ∘ extract
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
extract ∘ μ = extract ∘ extract now ext [w1 [w2 a]].
  Qed.

  Lemma bimonad_butterfly: forall (A: Type),
      cojoin (W := (W ×)) ∘ join (T := (W ×)) (A := A) =
        map (F := (W ×)) (join (T := (W ×))) ∘ join ∘
          map (F := (W ×)) (bdist (W ×) (W ×))
          ∘ cojoin (W := (W ×)) ∘
          map (F := (W ×)) (cojoin (W := (W ×))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type,
coμ ∘ μ =
map (μ) ∘ μ ∘ map (bdist (prod W) (prod W)) ∘ coμ
∘ map coμ
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type,
coμ ∘ μ =
map (μ) ∘ μ ∘ map (bdist (prod W) (prod W)) ∘ coμ
∘ map coμ
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
coμ ∘ μ =
map (μ) ∘ μ ∘ map (bdist (prod W) (prod W)) ∘ coμ
∘ map coμ now ext [w1 [w2 a]].
  Qed.

  #[export] Instance Bimonad_Writer: Bimonad (W ×) :=
    {| bimonad_monad := Monad_Categorical_writer;
       bimonad_comonad := Comonad_reader W;
       Bimonad.bimonad_dist_counit_l := @bimonad_dist_counit_l;
       Bimonad.bimonad_dist_counit_r := @bimonad_dist_counit_r;
       Bimonad.bimonad_distributive_law := BeckDistributiveLaw_strength;
       Bimonad.bimonad_cup := @bimonad_cup;
       Bimonad.bimonad_cap := @bimonad_cap;
       Bimonad.bimonad_baton := @bimonad_baton;
       Bimonad.bimonad_butterfly := @bimonad_butterfly;
    |}.

End writer_bimonad_instance.

(** ** Kleisli Monad Instance *)
(**********************************************************************)
Section writer_monad.

  Context
    `{Monoid W}.

  #[export] Instance Return_Writer: Return (W ×) :=
    fun A (a: A) => (Ƶ, a).

  #[export] Instance Bind_Writer: Bind (W ×) (W ×) :=
    fun A B (f: A -> W * B) (p: W * A) =>
      map_fst (uncurry (@monoid_op W _)) (α^-1 (map_snd f p)).

  #[export] Instance Natural_ret_Writer:
    Natural (@ret (W ×) Return_Writer).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Natural (@ret (prod W) Return_Writer)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Natural (@ret (prod W) Return_Writer)
    constructor; try typeclasses eauto.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : A -> B),
map f ∘ η = η ∘ map f
    intros A B f.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> B
map f ∘ η = η ∘ map f now ext a.
  Qed.

  Lemma Writer_kmon_bind0:
    forall (A B: Type) (f: A -> W * B),
      bind f ∘ ret = f.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : A -> W * B), bind f ∘ η = f
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : A -> W * B), bind f ∘ η = f
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> W * B
bind f ∘ η = f ext a.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> W * B
a: A
(bind f ∘ η) a = f a
    unfold compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> W * B
a: A
bind f (η a) = f a
    unfold transparent tcs.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> W * B
a: A
map_fst (uncurry monoid_op) (α^-1 (map_snd f (Ƶ, a))) =
f a
    cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> W * B
a: A
map_fst (uncurry monoid_op)
  (let (y, z) := f a in (id Ƶ, y, z)) = f a destruct (f a).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> W * B
a: A
w: W
b: B
map_fst (uncurry monoid_op) (id Ƶ, w, b) = (w, b)
    cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> W * B
a: A
w: W
b: B
(id Ƶ ● w, id b) = (w, b) now simpl_monoid.
  Qed.

  Lemma Writer_kmon_bind1:
    forall (A: Type), bind (ret (A := A)) = id.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type, bind (η) = id
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type, bind (η) = id
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
bind (η) = id ext [m a].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
m: W
a: A
bind (η) (m, a) = id (m, a) unfold transparent tcs.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
m: W
a: A
map_fst (uncurry monoid_op)
  (α^-1 (map_snd (fun a : A => (Ƶ, a)) (m, a))) =
id (m, a)
    cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
m: W
a: A
(id m ● Ƶ, id a) = id (m, a) now simpl_monoid.
  Qed.

  Lemma Writer_kmon_bind2:
    forall (A B C: Type) (g: B -> W * C) (f: A -> W * B),
      bind g ∘ bind f = bind (g ⋆ f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B C : Type) (g : B -> W * C)
  (f : A -> W * B), bind g ∘ bind f = bind (g ⋆ f)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B C : Type) (g : B -> W * C)
  (f : A -> W * B), bind g ∘ bind f = bind (g ⋆ f)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: B -> W * C
f: A -> W * B
bind g ∘ bind f = bind (g ⋆ f) ext [m a].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: B -> W * C
f: A -> W * B
m: W
a: A
(bind g ∘ bind f) (m, a) = bind (g ⋆ f) (m, a) unfold_ops @Bind_Writer.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: B -> W * C
f: A -> W * B
m: W
a: A
((fun p : W * B =>
  map_fst (uncurry monoid_op) (α^-1 (map_snd g p)))
 ∘ (fun p : W * A =>
    map_fst (uncurry monoid_op) (α^-1 (map_snd f p))))
  (m, a) =
map_fst (uncurry monoid_op)
  (α^-1 (map_snd (g ⋆ f) (m, a)))
    unfold kc, bind, compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: B -> W * C
f: A -> W * B
m: W
a: A
map_fst (uncurry monoid_op)
  (α^-1
     (map_snd g
        (map_fst (uncurry monoid_op)
           (α^-1 (map_snd f (m, a)))))) =
map_fst (uncurry monoid_op)
  (α^-1
     (map_snd
        (fun a : A =>
         map_fst (uncurry monoid_op)
           (α^-1 (map_snd g (f a)))) (m, a))) cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: B -> W * C
f: A -> W * B
m: W
a: A
map_fst (uncurry monoid_op)
  (α^-1
     (map_snd g
        (map_fst (uncurry monoid_op)
           (let (y, z) := f a in (id m, y, z))))) =
map_fst (uncurry monoid_op)
  (let (y, z) :=
     map_fst (uncurry monoid_op)
       (α^-1 (map_snd g (f a))) in
   (id m, y, z))
    unfold id.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: B -> W * C
f: A -> W * B
m: W
a: A
map_fst (uncurry monoid_op)
  (α^-1
     (map_snd g
        (map_fst (uncurry monoid_op)
           (let (y, z) := f a in (m, y, z))))) =
map_fst (uncurry monoid_op)
  (let (y, z) :=
     map_fst (uncurry monoid_op)
       (α^-1 (map_snd g (f a))) in
   (m, y, z)) destruct (f a).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: B -> W * C
f: A -> W * B
m: W
a: A
w: W
b: B
map_fst (uncurry monoid_op)
  (α^-1
     (map_snd g
        (map_fst (uncurry monoid_op) (m, w, b)))) =
map_fst (uncurry monoid_op)
  (let (y, z) :=
     map_fst (uncurry monoid_op)
       (α^-1 (map_snd g (w, b))) in
   (m, y, z)) cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: B -> W * C
f: A -> W * B
m: W
a: A
w: W
b: B
map_fst (uncurry monoid_op)
  (let (y, z) := g (id b) in (m ● w, y, z)) =
map_fst (uncurry monoid_op)
  (let (y, z) :=
     map_fst (uncurry monoid_op)
       (let (y, z) := g b in (id w, y, z)) in
   (m, y, z)) unfold id.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: B -> W * C
f: A -> W * B
m: W
a: A
w: W
b: B
map_fst (uncurry monoid_op)
  (let (y, z) := g b in (m ● w, y, z)) =
map_fst (uncurry monoid_op)
  (let (y, z) :=
     map_fst (uncurry monoid_op)
       (let (y, z) := g b in (w, y, z)) in
   (m, y, z)) destruct (g b).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: B -> W * C
f: A -> W * B
m: W
a: A
w: W
b: B
w0: W
c: C
map_fst (uncurry monoid_op) (m ● w, w0, c) =
map_fst (uncurry monoid_op)
  (let (y, z) :=
     map_fst (uncurry monoid_op) (w, w0, c) in
   (m, y, z))
    cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: B -> W * C
f: A -> W * B
m: W
a: A
w: W
b: B
w0: W
c: C
((m ● w) ● w0, id c) = (m ● (w ● w0), id (id c)) unfold id.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: B -> W * C
f: A -> W * B
m: W
a: A
w: W
b: B
w0: W
c: C
((m ● w) ● w0, c) = (m ● (w ● w0), c)
    now simpl_monoid.
  Qed.

  #[export] Instance RightPreModule_writer:
    Kleisli.Monad.RightPreModule (W ×) (W ×) :=
    {| kmod_bind1 := Writer_kmon_bind1;
       kmod_bind2 := Writer_kmon_bind2;
    |}.

  #[export] Instance Monad_writer: Kleisli.Monad.Monad (W ×) :=
    {| kmon_bind0 := Writer_kmon_bind0;
    |}.

  (** ** Miscellaneous Properties *)
  (********************************************************************)
  Lemma extract_pair {A: Type}:
    forall (w: W), extract ∘ pair w = @id A.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
forall w : W, extract ∘ pair w = id
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
forall w : W, extract ∘ pair w = id
    reflexivity.
  Qed.

  Lemma extract_incr {A: Type}:
    forall (w: W), extract ∘ incr w (A := A) = extract.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
forall w : W, extract ∘ incr w = extract
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
forall w : W, extract ∘ incr w = extract
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
extract ∘ incr w = extract now ext [w' a].
  Qed.

  Lemma extract_preincr {A: Type}:
    forall (w: W), extract ⦿ w = extract (A := A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
forall w : W, extract ⦿ w = extract
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
forall w : W, extract ⦿ w = extract
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
extract ⦿ w = extract now ext [w' a].
  Qed.

  Lemma extract_preincr2 {A B: Type} (f: A -> B):
    forall (w: W), (f ∘ extract) ⦿ w = f ∘ extract.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> B
forall w : W, (f ∘ extract) ⦿ w = f ∘ extract
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> B
forall w : W, (f ∘ extract) ⦿ w = f ∘ extract
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> B
w: W
(f ∘ extract) ⦿ w = f ∘ extract now ext [w' a].
  Qed.

  Lemma preincr_ret {A B: Type}:
    forall (f: W * A -> B) (w: W),
      (f ⦿ w) ∘ ret = f ∘ pair w.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
forall (f : W * A -> B) (w : W),
f ⦿ w ∘ η = f ∘ pair w
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
forall (f : W * A -> B) (w : W),
f ⦿ w ∘ η = f ∘ pair w
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
w: W
f ⦿ w ∘ η = f ∘ pair w ext a.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
w: W
a: A
(f ⦿ w ∘ η) a = (f ∘ pair w) a cbv.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
w: W
a: A
f (op w unit0, a) = f (w, a)
    change (op w unit0) with (w ● Ƶ).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
w: W
a: A
f (w ● Ƶ, a) = f (w, a)
    now simpl_monoid.
  Qed.

  Lemma incr_spec `{Monoid W}:
    forall A, uncurry incr = join (T := (W ×)) (A := A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit1: Monoid_unit W
H0: Monoid W
forall A : Type, uncurry incr = μ
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit1: Monoid_unit W
H0: Monoid W
forall A : Type, uncurry incr = μ
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit1: Monoid_unit W
H0: Monoid W
A: Type
uncurry incr = μ ext [w1 [w2 a]].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
op0: Monoid_op W
unit1: Monoid_unit W
H0: Monoid W
A: Type
w1, w2: W
a: A
uncurry incr (w1, (w2, a)) = μ (w1, (w2, a)) reflexivity.
  Qed.

End writer_monad.