From Tealeaves Require Import
  Misc.Product
  Misc.Strength
  Classes.Comonoid
  Classes.Kleisli.Comonad
  Classes.Categorical.Comonad.

Export Misc.Product.
Export Misc.Strength.
Export Classes.Comonoid.

Import Product.Notations.

(** * Environment/Reader Comonad *)
(**********************************************************************)

(** ** Functor Instances *)
(**********************************************************************)
#[export] Instance Map_reader (E: Type):
  Map (E ×) := (fun A B => map_snd).

#[program, export] Instance Functor_reader (E: Type):
  Functor (E ×).

Solve All Obligations with (introv; now ext [? ?]).

(** ** Categorical Comonad Instance *)
(**********************************************************************)
Section with_E.

  Context
    (E: Type).

  #[export] Instance Cojoin_reader: Cojoin (E ×) :=
    @dup_left E.

  #[export] Instance Extract_reader: Extract (E ×) :=
    @snd E.

  #[export] Instance Natural_extract_reader: Natural (@extract (E ×) _).
E: Type
Natural (@extract (prod E) Extract_reader)
  Proof.
E: Type
Natural (@extract (prod E) Extract_reader)
    constructor; try typeclasses eauto.
E: Type
forall (A B : Type) (f : A -> B),
map f ∘ extract = extract ∘ map f
    introv.
E, A, B: Type
f: A -> B
map f ∘ extract = extract ∘ map f now ext [? ?].
  Qed.

  #[export] Instance Natural_cojoin_reader: Natural (@cojoin (E ×) _).
E: Type
Natural (@cojoin (prod E) Cojoin_reader)
  Proof.
E: Type
Natural (@cojoin (prod E) Cojoin_reader)
    constructor; try typeclasses eauto.
E: Type
forall (A B : Type) (f : A -> B),
map f ∘ cojoin = cojoin ∘ map f
    introv.
E, A, B: Type
f: A -> B
map f ∘ cojoin = cojoin ∘ map f now ext [? ?].
  Qed.

  #[export, program] Instance Comonad_reader: Comonad (E ×).

  Solve All Obligations with (introv; now ext [? ?]).

End with_E.

(** ** Kleisli Comonad Instance *)
(**********************************************************************)
Section with_E.

  Context
    (E: Type).

  (*
    #[export] Instance Extract_reader: Extract (E ×) :=
    fun A '(e, a) => a.
   *)

  #[export] Instance Cobind_reader: Cobind (E ×) :=
    fun A B (f: E * A -> B) '(e, a) => (e, f (e, a)).

  #[export, program] Instance KleisliComonad_reader:
    Kleisli.Comonad.Comonad (E ×).

  Solve All Obligations with (introv; now ext [? ?]).

  (*
    #[export] Instance Map_reader: Map (E ×) :=
    Comonad.Map_Cobind (E ×).

    #[export] Instance Functor_reader: Functor (E ×) :=
    Comonad.Functor_Comonad (E ×).
   *)

  #[export] Instance Map_Cobind_Compat_Reader: Compat_Map_Cobind (E ×).
E: Type
Compat_Map_Cobind (prod E)
  Proof.
E: Type
Compat_Map_Cobind (prod E)
    reflexivity.
  Qed.

End with_E.

(** * Properties of <<strength>>  *)
(**********************************************************************)
From Tealeaves Require Import
  Classes.Categorical.Monad
  Classes.Categorical.RightModule.

(** ** Interaction with Categorical Monad Operations *)
(**********************************************************************)
Section Monad_strength_laws.

  Context
    (T : Type -> Type)
    `{Categorical.Monad.Monad T}
    (A B : Type).

  Import Strength.Notations.
  Import Monad.Notations.

  Lemma strength_ret:
    σ ∘ map (F := (A ×)) ret = ret (T := T) (A := A * B).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
σ ∘ map (η) = η
  Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
σ ∘ map (η) = η
    intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
σ ∘ map (η) = η ext [a b].
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
b: B
(σ ∘ map (η)) (a, b) = η (a, b) cbn.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
b: B
map (pair (id a)) (η b) = η (a, b)
    unfold compose; cbn.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
b: B
map (pair (id a)) (η b) = η (a, b)
    compose near b on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
b: B
(map (pair (id a)) ∘ η) b = η (a, b)
    now rewrite (natural (G := T) (F := fun A => A)).
  Qed.

  Lemma strength_join:
    σ ∘ map (F := (A ×)) (μ (A := B)) =
      μ (A := A * B) ∘
        map (F := T) (strength (F := T)) ∘
        strength (F := T).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
σ ∘ map (μ) = μ ∘ map (σ) ∘ σ
  Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
σ ∘ map (μ) = μ ∘ map (σ) ∘ σ
    intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
σ ∘ map (μ) = μ ∘ map (σ) ∘ σ ext [a t].
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
t: (T ∘ T) B
(σ ∘ map (μ)) (a, t) = (μ ∘ map (σ) ∘ σ) (a, t)
    unfold compose at 1.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
t: (T ∘ T) B
σ (map (μ) (a, t)) = (μ ∘ map (σ) ∘ σ) (a, t)
    change_left (σ (a, μ t)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
t: (T ∘ T) B
σ (a, μ t) = (μ ∘ map (σ) ∘ σ) (a, t)
    unfold strength, compose at 1 4.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
t: (T ∘ T) B
map (pair a) (μ t) =
(μ ∘ map (fun '(a, t) => map (pair a) t))
  (map (pair a) t)
    compose near t.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
t: (T ∘ T) B
(map (pair a) ∘ μ) t =
(μ ∘ map (fun '(a, t) => map (pair a) t)
 ∘ map (pair a)) t
    unfold_compose_in_compose.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
t: (T ∘ T) B
(map (pair a) ∘ μ) t =
(μ ∘ map (fun '(a, t) => map (pair a) t)
 ∘ map (pair a)) t
    rewrite (natural (A := B) (B := A * B) (ϕ := @join T _)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
t: (T ∘ T) B
(μ ∘ map (pair a)) t =
(μ ∘ map (fun '(a, t) => map (pair a) t)
 ∘ map (pair a)) t
    unfold compose; cbn.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
t: (T ∘ T) B
μ (map (pair a) t) =
μ
  (map (fun '(a, t) => map (pair a) t)
     (map (pair a) t))
    compose near t.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
t: (T ∘ T) B
(μ ∘ map (pair a)) t =
μ
  ((map (fun '(a, t) => map (pair a) t) ∘ map (pair a))
     t)
    rewrite (fun_map_map (F := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
a: A
t: (T ∘ T) B
(μ ∘ map (pair a)) t =
μ (map ((fun '(a, t) => map (pair a) t) ∘ pair a) t)
    reflexivity.
  Qed.

  Context
    (F : Type -> Type)
    `{Categorical.RightModule.RightModule F T}.

  Lemma strength_right_action:
    σ ∘ map (F := (A ×)) (right_action F) =
      right_action F (A := A * B) ∘ map σ ∘ σ.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
σ ∘ map (right_action F) =
right_action F ∘ map (σ) ∘ σ
  Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
σ ∘ map (right_action F) =
right_action F ∘ map (σ) ∘ σ
    intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
σ ∘ map (right_action F) =
right_action F ∘ map (σ) ∘ σ ext [a t].
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: (F ∘ T) B
(σ ∘ map (right_action F)) (a, t) =
(right_action F ∘ map (σ) ∘ σ) (a, t) change_left (σ (a, right_action F t)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: (F ∘ T) B
σ (a, right_action F t) =
(right_action F ∘ map (σ) ∘ σ) (a, t)
    unfold strength, compose in *.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
map (pair a) (right_action F t) =
right_action F
  (map (fun '(a, t) => map (pair a) t)
     (map (pair a) t))
    unfold_ops @Map_I.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
map (pair a) (right_action F t) =
right_action F
  (map (fun '(a, t) => (a, t)) (map (pair a) t))
    inversion H8.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
map (pair a) (right_action F t) =
right_action F
  (map (fun '(a, t) => (a, t)) (map (pair a) t))
    compose near t on right.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
map (pair a) (right_action F t) =
right_action F
  ((map (fun '(a, t) => (a, t)) ∘ map (pair a)) t)
    unfold_ops @Map_compose.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
map (pair a) (right_action F t) =
right_action F
  ((map (map (fun '(a, t) => (a, t)))
    ∘ map (map (pair a))) t)
    rewrite (fun_map_map (F := F)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
map (pair a) (right_action F t) =
right_action F
  (map (map (fun '(a, t) => (a, t)) ∘ map (pair a)) t)
    unfold compose.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
map (pair a) (right_action F t) =
right_action F
  (map (map (fun '(a, t) => (a, t)) ○ map (pair a)) t) cbn.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
map (pair a) (right_action F t) =
right_action F
  (map (map (fun '(a, t) => (a, t)) ○ map (pair a)) t)
    compose near t on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
(map (pair a) ∘ right_action F) t =
right_action F
  (map (map (fun '(a, t) => (a, t)) ○ map (pair a)) t)
    compose near t on right.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
(map (pair a) ∘ right_action F) t =
(right_action F
 ∘ map (map (fun '(a, t) => (a, t)) ○ map (pair a))) t
    replace (fun '(a1, t0) => (a1, t0)) with (@id (A * B)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
(map (pair a) ∘ right_action F) t =
(right_action F ∘ map (map id ○ map (pair a))) t
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
id = (fun '(a1, t0) => (a1, t0))
    rewrite (fun_map_id).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
(map (pair a) ∘ right_action F) t =
(right_action F ∘ map (id ○ map (pair a))) t
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
id = (fun '(a1, t0) => (a1, t0))
    rewrite (natural (F := F ∘ T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
(right_action F ∘ map (pair a)) t =
(right_action F ∘ map (id ○ map (pair a))) t
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
id = (fun '(a1, t0) => (a1, t0))
    reflexivity.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Monad T
A, B: Type
F: Type -> Type
H3: Map T
H4: Return T
H5: Join T
H6: Map F
H7: RightAction F T
H8: RightModule F T
a: A
t: F (T B)
mod_object: Functor F
mon_monoid: Monad T
mod_natural: Natural (@right_action F T H7)
mod_action_map_ret: forall A : Type,
right_action F ∘ map (η) = id
mod_action_action: forall A : Type,
right_action F ∘ right_action F =
right_action F ∘ map (μ)
id = (fun '(a1, t0) => (a1, t0))
    now ext [a' b'].
  Qed.

End Monad_strength_laws.


(** ** Interaction with Reader Comonad Operations *)
(**********************************************************************)
Section Comonad_strength_laws.

  Context
    (E: Type)
    (F: Type -> Type).

  Theorem strength_extract `{Functor F} {A: Type}:
    map extract ∘ strength = extract (W := (E ×)) (A := F A).
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
map extract ∘ strength = extract
  Proof.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
map extract ∘ strength = extract
    intros.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
map extract ∘ strength = extract unfold strength, compose.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
(fun a : E * F A =>
 map extract (let '(a0, t) := a in map (pair a0) t)) =
extract ext [w a].
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
w: E
a: F A
map extract (map (pair w) a) = extract (w, a)
    reflexivity.
  Qed.

  Theorem strength_cojoin `{Functor F} {A: Type}:
    `(map (F := F) (cojoin (W := (E ×)) (A := A)) ∘ strength =
        strength ∘ map (F := (E ×)) strength ∘ cojoin (W := (E ×))).
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
map cojoin ∘ strength =
strength ∘ map strength ∘ cojoin
  Proof.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
map cojoin ∘ strength =
strength ∘ map strength ∘ cojoin
    intros.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
map cojoin ∘ strength =
strength ∘ map strength ∘ cojoin unfold strength, compose.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
(fun a : E * F A =>
 map cojoin (let '(a0, t) := a in map (pair a0) t)) =
(fun a : E * F A =>
 let
 '(a0, t) :=
  map (fun '(a0, t) => map (pair a0) t) (cojoin a) in
  map (pair a0) t) ext [w a].
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
w: E
a: F A
map cojoin (map (pair w) a) =
(let
 '(a, t) :=
  map (fun '(a, t) => map (pair a) t) (cojoin (w, a))
  in map (pair a) t) cbn.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
w: E
a: F A
map cojoin (map (pair w) a) =
map (pair (id w)) (map (pair w) a)
    compose_near a.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
w: E
a: F A
(map cojoin ∘ map (pair w)) a =
(map (pair (id w)) ∘ map (pair w)) a now rewrite 2(fun_map_map).
  Qed.

  Lemma map_strength_cobind_spec {G} `{Functor G}:
    forall (A B C: Type) (f: E * A -> G B) (g: E * B -> C),
      map g ∘ strength ∘ cobind (W := (E ×)) f =
        (fun '(e, a) => map (g ∘ pair e) (f (e, a))).
E: Type
F, G: Type -> Type
Map_F: Map G
H: Functor G
forall (A B C : Type) (f : E * A -> G B)
  (g : E * B -> C),
map g ∘ strength ∘ cobind f =
(fun '(e, a) => map (g ∘ pair e) (f (e, a)))
  Proof.
E: Type
F, G: Type -> Type
Map_F: Map G
H: Functor G
forall (A B C : Type) (f : E * A -> G B)
  (g : E * B -> C),
map g ∘ strength ∘ cobind f =
(fun '(e, a) => map (g ∘ pair e) (f (e, a)))
    intros.
E: Type
F, G: Type -> Type
Map_F: Map G
H: Functor G
A, B, C: Type
f: E * A -> G B
g: E * B -> C
map g ∘ strength ∘ cobind f =
(fun '(e, a) => map (g ∘ pair e) (f (e, a))) ext [w a].
E: Type
F, G: Type -> Type
Map_F: Map G
H: Functor G
A, B, C: Type
f: E * A -> G B
g: E * B -> C
w: E
a: A
(map g ∘ strength ∘ cobind f) (w, a) =
map (g ∘ pair w) (f (w, a))
    unfold strength, compose; cbn.
E: Type
F, G: Type -> Type
Map_F: Map G
H: Functor G
A, B, C: Type
f: E * A -> G B
g: E * B -> C
w: E
a: A
map g (map (pair w) (f (w, a))) =
map (g ○ pair w) (f (w, a))
    compose near (f (w, a)) on left.
E: Type
F, G: Type -> Type
Map_F: Map G
H: Functor G
A, B, C: Type
f: E * A -> G B
g: E * B -> C
w: E
a: A
(map g ∘ map (pair w)) (f (w, a)) =
map (g ○ pair w) (f (w, a))
    rewrite fun_map_map.
E: Type
F, G: Type -> Type
Map_F: Map G
H: Functor G
A, B, C: Type
f: E * A -> G B
g: E * B -> C
w: E
a: A
map (g ∘ pair w) (f (w, a)) =
map (g ○ pair w) (f (w, a))
    reflexivity.
  Qed.

End Comonad_strength_laws.

(** ** Miscellaneous Properties *)
(**********************************************************************)
Section with_E.

  Context
    (E: Type)
    (F: Type -> Type).

  #[export] Instance Natural_strength
    `{Functor F}: Natural (F := prod E ∘ F) (@strength F _ E).
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
Natural (@strength F Map_F E)
  Proof.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
Natural (@strength F Map_F E)
    constructor; try typeclasses eauto.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
forall (A B : Type) (f : A -> B),
map f ∘ strength = strength ∘ map f
    intros.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
f: A -> B
map f ∘ strength = strength ∘ map f unfold_ops @Map_compose.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
f: A -> B
map (map f) ∘ strength = strength ∘ map (map f) ext [a t].
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
f: A -> B
a: E
t: F A
(map (map f) ∘ strength) (a, t) =
(strength ∘ map (map f)) (a, t)
    unfold compose; cbn.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
f: A -> B
a: E
t: F A
map (map f) (map (pair a) t) =
map (pair (id a)) (map f t)
    compose near t on left.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
f: A -> B
a: E
t: F A
(map (map f) ∘ map (pair a)) t =
map (pair (id a)) (map f t)
    compose near t on right.
E: Type
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
f: A -> B
a: E
t: F A
(map (map f) ∘ map (pair a)) t =
(map (pair (id a)) ∘ map f) t
    now rewrite 2(fun_map_map).
  Qed.

  Theorem product_map_commute
    {E1 E2 A B: Type} (g: E1 -> E2) (f: A -> B):
    map (F := (E2 ×)) f ∘ map_fst g = map_fst g ∘ map (F := (E1 ×)) f.
E: Type
F: Type -> Type
E1, E2, A, B: Type
g: E1 -> E2
f: A -> B
map f ∘ map_fst g = map_fst g ∘ map f
  Proof.
E: Type
F: Type -> Type
E1, E2, A, B: Type
g: E1 -> E2
f: A -> B
map f ∘ map_fst g = map_fst g ∘ map f
    now ext [w a].
  Qed.

  Lemma dup_left_spec {A B}:
    @dup_left A B  = α ∘ map_fst comonoid_comult.
E: Type
F: Type -> Type
A, B: Type
dup_left = α ∘ map_fst comonoid_comult
  Proof.
E: Type
F: Type -> Type
A, B: Type
dup_left = α ∘ map_fst comonoid_comult
    now ext [? ?].
  Qed.


End with_E.