Equivalent definitions of "decide" for comonads (comonads are (some kind of) monoidal functors)

comonad_decide.v

(* Let f be a comonad... *)
Parameter f : Type -> Type.

Parameter fmap : forall {a b}, (a -> b) -> f a -> f b.
Parameter extract : forall {a}, f a -> a.
Parameter duplicate : forall {a}, f a -> f (f a).

Parameter extract_fmap : forall a b (g : a -> b) (u : f a),
    extract (fmap g u) = g (extract u).
Parameter extract_duplicate : forall a (u : f a),
    extract (duplicate u) = u.
Parameter fmap_fmap : forall a b c (g : a -> b) (h : b -> c) (u : f a),
    fmap h (fmap g u) = fmap (fun x => h (g x)) u.
Parameter fmap_extract_duplicate : forall a (u : f a),
    fmap extract (duplicate u) = u.

(* Definitions *)

Definition either {a b c} (f : a -> c) (g : b -> c) (x : a + b) : c :=
  match x with
  | inl u => f u
  | inr v => g v
  end.

Definition const {a b} (x : a) (_ : b) : a := x.
Definition id {a} (x : a) : a := x.

Definition decide {a b} : f (a + b) -> f a + f b :=
  fun fx =>
    match extract fx with
    | inl a => inl (fmap (either id (const a)) fx)
    | inr b => inr (fmap (either (const b) id) fx)
    end.

Definition symm {a b} : a + b -> b + a :=
  either inr inl.

Definition lcostrength {a b} : f (a + b) -> a + f b :=
  fun fab =>
    match extract fab with
    | inl a => inl a
    | inr b => inr (fmap (either (const b) id) fab)
    end.

Definition rcostrength {a b} : f (a + b) -> (f a) + b :=
  fun fab => symm (lcostrength (fmap symm fab)).

Definition decide1 {a b} : f (a + b) -> f a + f b :=
  fun fab => lcostrength (fmap rcostrength (duplicate fab)).

Definition decide2 {a b} : f (a + b) -> f a + f b :=
  fun fab => rcostrength (fmap lcostrength (duplicate fab)).

Lemma either_symm {a b c} (g : a -> c) (h : b -> c) (u : a + b)
  : either h g (symm u) = either g h u.
Proof.
  destruct u; reflexivity.
Qed.

Require Import FunctionalExtensionality.

Theorem d1 {a b} (u : f (a + b)) :
  decide u = decide1 u.
Proof.
  unfold decide, decide1.
  destruct (extract u) eqn:E_eu.
  - unfold lcostrength.
    rewrite extract_fmap, extract_duplicate.
    unfold rcostrength, lcostrength.
    rewrite extract_fmap, E_eu.
    cbn.
    rewrite fmap_fmap.
    repeat f_equal.
    apply functional_extensionality; intros.
    rewrite either_symm.
    reflexivity.
  - unfold lcostrength, rcostrength.
    rewrite extract_fmap, extract_duplicate.
    unfold lcostrength.
    rewrite extract_fmap, E_eu.
    cbn.
    rewrite fmap_fmap.
    repeat f_equal.
    replace (fun x =>
               _) with (fun x : f (a + b) => either (const b0) id (extract x)).
    + rewrite <- (fmap_fmap (f (a + b))).
      rewrite fmap_extract_duplicate.
      reflexivity.
    + apply functional_extensionality; intros.
      rewrite extract_fmap.
      destruct (extract x) eqn:E_ex.
      * reflexivity.
      * reflexivity.
Qed.