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

(** * Comonad to Kleisli comonad *)
(**********************************************************************)

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

  #[export] Instance Cobind_Categorical (W: Type -> Type)
    `{Map W} `{Cojoin W}: Cobind W :=
  fun {A B} (f: W A -> B) => map (F := W) f ∘ cojoin.

End DerivedOperations.

Class Compat_Cobind_Categorical
    (W: Type -> Type)
    `{Map_W: Map W}
    `{Cojoin_W: Cojoin W}
    `{Cobind_W: Cobind W} :=
  compat_cobind_categorical:
    Cobind_W = @DerivedOperations.Cobind_Categorical W Map_W Cojoin_W.

#[export] Instance Cobind_Categorical_Self {W} `{Map W} `{Cojoin W}:
  @Compat_Cobind_Categorical W _ _ (@DerivedOperations.Cobind_Categorical W _ _).
W: Type -> Type
H: Map W
H0: Cojoin W
Compat_Cobind_Categorical W
Proof.
W: Type -> Type
H: Map W
H0: Cojoin W
Compat_Cobind_Categorical W
  reflexivity.
Qed.

Lemma cobind_to_categorical {W}
    `{Map_W: Map W}
    `{Cojoin_W: Cojoin W}
    `{Cobind_W: Cobind W}
    `{Compat: Compat_Cobind_Categorical W}:
  forall (A B: Type)
      (f: W A -> B),
      cobind (W := W) f = map (F := W) f ∘ cojoin.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Cobind_W: Cobind W
Map_W0: Map W
Cojoin_W0: Cojoin W
Cobind_W0: Cobind W
Compat: Compat_Cobind_Categorical W
forall (A B : Type) (f : W A -> B),
cobind f = map f ∘ cojoin
Proof.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Cobind_W: Cobind W
Map_W0: Map W
Cojoin_W0: Cojoin W
Cobind_W0: Cobind W
Compat: Compat_Cobind_Categorical W
forall (A B : Type) (f : W A -> B),
cobind f = map f ∘ cojoin
  now rewrite compat_cobind_categorical.
Qed.

Module DerivedInstances.
  (* Alectryon doesn't like this
     Import CategoricalToKleisli.Comonad.DerivedOperations.
   *)
  Import DerivedOperations.
  Import Tealeaves.Classes.Kleisli.Comonad.
  Import Kleisli.Comonad.Notations.

  #[local] Generalizable All Variables.
  #[local] Arguments cobind W%function_scope {Cobind}
    (A B)%type_scope _%function_scope _.


  (** ** <<cojoin>> as <<id ⋆1 id>> *)
  (********************************************************************)
  Lemma cojoin_to_kc `{Categorical.Comonad.Comonad W}: forall (A: Type),
      cojoin (W := W) (A := A) = id ⋆1 id.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
forall A : Type, cojoin = id ⋆1 id
  Proof.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
forall A : Type, cojoin = id ⋆1 id
    intros.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A: Type
cojoin = id ⋆1 id unfold kc1, cobind, Cobind_Categorical.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A: Type
cojoin = id ∘ (map id ∘ cojoin)
    rewrite fun_map_id.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A: Type
cojoin = id ∘ (id ∘ cojoin)
    reflexivity.
  Qed.

  (** ** Derived co-Kleisli Laws *)
  (********************************************************************)
  Section with_monad.

    Context
      `{Categorical.Comonad.Comonad W}.

    (** *** Identity law *)
    (******************************************************************)
    Lemma kcom_bind_id:
      `(@cobind W _ A A (@extract W _ A) = @id (W A)).
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
forall A : Type, cobind W A A extract = id
    Proof.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
forall A : Type, cobind W A A extract = id
      intros.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A: Type
cobind W A A extract = id unfold_ops @DerivedOperations.Cobind_Categorical.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A: Type
map extract ∘ cojoin = id
      rewrite com_map_extr_cojoin.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A: Type
id = id
      reflexivity.
    Qed.

    (** *** Composition law *)
    (******************************************************************)
    Lemma kcom_bind_bind:
      forall (A B C: Type) (g: W B -> C) (f: W A -> B),
        cobind W B C g ∘ cobind W A B f = cobind W A C (g ⋆1 f).
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
forall (A B C : Type) (g : W B -> C) (f : W A -> B),
cobind W B C g ∘ cobind W A B f =
cobind W A C (g ⋆1 f)
    Proof.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
forall (A B C : Type) (g : W B -> C) (f : W A -> B),
cobind W B C g ∘ cobind W A B f =
cobind W A C (g ⋆1 f)
      introv.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
cobind W B C g ∘ cobind W A B f =
cobind W A C (g ⋆1 f) unfold transparent tcs.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
map g ∘ cojoin ∘ (map f ∘ cojoin) =
map (g ⋆1 f) ∘ cojoin
      unfold kc1.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
map g ∘ cojoin ∘ (map f ∘ cojoin) =
map (g ∘ cobind W A B f) ∘ cojoin
      unfold_ops @Cobind_Categorical.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
map g ∘ cojoin ∘ (map f ∘ cojoin) =
map (g ∘ (map f ∘ cojoin)) ∘ cojoin
      reassociate <- on left.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
map g ∘ cojoin ∘ map f ∘ cojoin =
map (g ∘ (map f ∘ cojoin)) ∘ cojoin
      reassociate -> near (map f).
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
map g ∘ (cojoin ∘ map f) ∘ cojoin =
map (g ∘ (map f ∘ cojoin)) ∘ cojoin
      rewrite <- (natural (ϕ := @cojoin W _)).
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
map g ∘ (map f ∘ cojoin) ∘ cojoin =
map (g ∘ (map f ∘ cojoin)) ∘ cojoin
      unfold_ops @Map_compose.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
map g ∘ (map (map f) ∘ cojoin) ∘ cojoin =
map (g ∘ (map f ∘ cojoin)) ∘ cojoin
      reassociate -> on left.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
map g ∘ (map (map f) ∘ cojoin ∘ cojoin) =
map (g ∘ (map f ∘ cojoin)) ∘ cojoin
      reassociate -> on left.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
map g ∘ (map (map f) ∘ (cojoin ∘ cojoin)) =
map (g ∘ (map f ∘ cojoin)) ∘ cojoin
      rewrite (com_cojoin_cojoin (W := W)).
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
map g ∘ (map (map f) ∘ (map cojoin ∘ cojoin)) =
map (g ∘ (map f ∘ cojoin)) ∘ cojoin
      do 2 reassociate <- on left.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
map g ∘ map (map f) ∘ map cojoin ∘ cojoin =
map (g ∘ (map f ∘ cojoin)) ∘ cojoin
      unfold_compose_in_compose.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
map g ∘ map (map f) ∘ map cojoin ∘ cojoin =
map (g ∘ (map f ∘ cojoin)) ∘ cojoin
      do 2 rewrite fun_map_map.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B, C: Type
g: W B -> C
f: W A -> B
map (g ∘ map f ∘ cojoin) ∘ cojoin =
map (g ∘ (map f ∘ cojoin)) ∘ cojoin
      reflexivity.
    Qed.

    (** *** Unit law *)
    (******************************************************************)
    Lemma kcom_bind_comp_ret:
      forall (A B: Type) (f: W A -> B),
        extract ∘ cobind W A B f = f.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
forall (A B : Type) (f : W A -> B),
extract ∘ cobind W A B f = f
    Proof.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
forall (A B : Type) (f : W A -> B),
extract ∘ cobind W A B f = f
      intros.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B: Type
f: W A -> B
extract ∘ cobind W A B f = f unfold transparent tcs.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B: Type
f: W A -> B
extract ∘ (map f ∘ cojoin) = f
      reassociate <- on left.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B: Type
f: W A -> B
extract ∘ map f ∘ cojoin = f
      rewrite <- (natural (ϕ := @extract W _)).
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B: Type
f: W A -> B
map f ∘ extract ∘ cojoin = f
      reassociate -> on left.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B: Type
f: W A -> B
map f ∘ (extract ∘ cojoin) = f
      rewrite com_extract_cojoin.
W: Type -> Type
Map_W: Map W
Cojoin_W: Cojoin W
Extract_W: Extract W
H: Categorical.Comonad.Comonad W
A, B: Type
f: W A -> B
map f ∘ id = f
      reflexivity.
    Qed.

    (** ** Typeclass Instance *)
    (******************************************************************)
    #[export] Instance KleisliComonad_CategoricalComonad:
      Kleisli.Comonad.Comonad W :=
      {| kcom_cobind0 := @kcom_bind_comp_ret;
         kcom_cobind1 := @kcom_bind_id;
         kcom_cobind2 := @kcom_bind_bind;
      |}.

  End with_monad.

End DerivedInstances.