From Tealeaves Require Export
  Classes.Functor
  Classes.Categorical.Comonad (Extract, extract).

Import Functor.Notations.

#[local] Generalizable Variables W A B C D.

(** * Comonads *)
(**********************************************************************)

(** ** Operations *)
(**********************************************************************)
Class Cobind (W : Type -> Type) :=
  cobind : forall (A B : Type), (W A -> B) -> W A -> W B.

#[global] Arguments cobind {W}%function_scope {Cobind}
  {A B}%type_scope _%function_scope _.

(** ** Co-Kleisli Composition *)
(**********************************************************************)
Definition kc1 {W : Type -> Type} `{Cobind W}
  {A B C : Type} `(g : W B -> C) `(f : W A -> B) : (W A -> C) :=
  g ∘ @cobind W _ A B f.

#[local] Infix "⋆1" := (kc1) (at level 60) : tealeaves_scope.

(** ** Typeclasses *)
(**********************************************************************)
Class Comonad `(W : Type -> Type) `{Cobind W} `{Extract W} :=
  { kcom_cobind0 : forall `(f : W A -> B),
      @extract W _ B ∘ @cobind W _ A B f = f;
    kcom_cobind1 : forall (A : Type),
      @cobind W _ A A (@extract W _ A) = @id (W A);
    kcom_cobind2 : 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)
  }.


(** ** Kleisli Category Laws *)
(**********************************************************************)
Section Kleisli_category_laws.

  Context
    `{Comonad W}.

  Lemma kc1_id_r {B C} : forall (g : W B -> C),
      g ⋆1 (@extract W _ B) = g.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
B, C: Type
forall g : W B -> C, g ⋆1 extract = g
  Proof.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
B, C: Type
forall g : W B -> C, g ⋆1 extract = g
    intros.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
B, C: Type
g: W B -> C
g ⋆1 extract = g
    unfold kc1.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
B, C: Type
g: W B -> C
g ∘ cobind extract = g
    rewrite kcom_cobind1.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
B, C: Type
g: W B -> C
g ∘ id = g
    reflexivity.
  Qed.

  Lemma kc1_id_l {A B} : forall  (f : W A -> B),
      (@extract W _ B) ⋆1 f = f.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
A, B: Type
forall f : W A -> B, extract ⋆1 f = f
  Proof.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
A, B: Type
forall f : W A -> B, extract ⋆1 f = f
    intros.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
A, B: Type
f: W A -> B
extract ⋆1 f = f
    unfold kc1.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
A, B: Type
f: W A -> B
extract ∘ cobind f = f
    rewrite kcom_cobind0.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
A, B: Type
f: W A -> B
f = f
    reflexivity.
  Qed.

  Lemma kc1_assoc {A B C D}:
    forall (h : W C -> D) (g : W B -> C) (f : W A -> B),
      h ⋆1 g ⋆1 f = h ⋆1 (g ⋆1 f).
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
A, B, C, D: Type
forall (h : W C -> D) (g : W B -> C) (f : W A -> B),
(h ⋆1 g) ⋆1 f = h ⋆1 (g ⋆1 f)
  Proof.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
A, B, C, D: Type
forall (h : W C -> D) (g : W B -> C) (f : W A -> B),
(h ⋆1 g) ⋆1 f = h ⋆1 (g ⋆1 f)
    intros.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
A, B, C, D: Type
h: W C -> D
g: W B -> C
f: W A -> B
(h ⋆1 g) ⋆1 f = h ⋆1 (g ⋆1 f)
    unfold kc1.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
A, B, C, D: Type
h: W C -> D
g: W B -> C
f: W A -> B
h ∘ cobind g ∘ cobind f = h ∘ cobind (g ∘ cobind f)
    reassociate ->.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
A, B, C, D: Type
h: W C -> D
g: W B -> C
f: W A -> B
h ∘ (cobind g ∘ cobind f) = h ∘ cobind (g ∘ cobind f)
    rewrite kcom_cobind2.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
A, B, C, D: Type
h: W C -> D
g: W B -> C
f: W A -> B
h ∘ cobind (g ⋆1 f) = h ∘ cobind (g ∘ cobind f)
    reflexivity.
  Qed.

End Kleisli_category_laws.

(** ** Comonad Homomorphisms *)
(** TODO *)
(**********************************************************************)

(** * Derived Structures *)
(**********************************************************************)

(** ** Derived Operations *)
(**********************************************************************)
Module DerivedOperations.

  #[export] Instance Map_Cobind (W: Type -> Type)
    `{Extract_W: Extract W} `{Cobind_W: Cobind W}: Map W :=
  fun A B (f : A -> B) =>
    @cobind W Cobind_W A B (f ∘ @extract W Extract_W A).

End DerivedOperations.

Class Compat_Map_Cobind
  (W: Type -> Type)
  `{Extract_W: Extract W}
  `{Cobind_W: Cobind W}
  `{Map_W: Map W}: Prop :=
  compat_map_cobind:
    @Map_W = @DerivedOperations.Map_Cobind W Extract_W Cobind_W.

#[export] Instance Compat_Map_Cobind_Comonad (W: Type -> Type)
  `{Extract_W: Extract W} `{Cobind_W: Cobind W}:
  @Compat_Map_Cobind W Extract_W Cobind_W
    (@DerivedOperations.Map_Cobind W Extract_W Cobind_W).
W: Type -> Type
Extract_W: Extract W
Cobind_W: Cobind W
Compat_Map_Cobind W
Proof.
W: Type -> Type
Extract_W: Extract W
Cobind_W: Cobind W
Compat_Map_Cobind W
  reflexivity.
Qed.

Lemma map_to_cobind {W: Type -> Type}
  `{Extract_W: Extract W}
  `{Combind_W: Cobind W}
  `{Map_W: Map W}
  `{! Compat_Map_Cobind W}: forall {A B: Type} (f: A -> B),
    map (F := W) f = cobind (f ∘ extract).
W: Type -> Type
Extract_W: Extract W
Combind_W: Cobind W
Map_W: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
forall (A B : Type) (f : A -> B),
map f = cobind (f ∘ extract)
Proof.
W: Type -> Type
Extract_W: Extract W
Combind_W: Cobind W
Map_W: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
forall (A B : Type) (f : A -> B),
map f = cobind (f ∘ extract)
  intros.
W: Type -> Type
Extract_W: Extract W
Combind_W: Cobind W
Map_W: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B: Type
f: A -> B
map f = cobind (f ∘ extract)
  rewrite compat_map_cobind.
W: Type -> Type
Extract_W: Extract W
Combind_W: Cobind W
Map_W: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B: Type
f: A -> B
DerivedOperations.Map_Cobind W A B f =
cobind (f ∘ extract)
  reflexivity.
Qed.

(** ** Derived Kleisli Composition Laws *)
(**********************************************************************)
Section derived_instances.

  Context `{Comonad W} `{Map W} `{! Compat_Map_Cobind W}.

  (** *** Special cases for Kleisli composition *)
  (********************************************************************)
  Lemma kc1_10 {A B C} : forall (g : W B -> C) (f : A -> B),
      g ⋆1 (f ∘ extract) = g ∘ map f.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
forall (g : W B -> C) (f : A -> B),
g ⋆1 f ∘ extract = g ∘ map f
  Proof.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
forall (g : W B -> C) (f : A -> B),
g ⋆1 f ∘ extract = g ∘ map f
    intros.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
g: W B -> C
f: A -> B
g ⋆1 f ∘ extract = g ∘ map f
    unfold kc1.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
g: W B -> C
f: A -> B
g ∘ cobind (f ∘ extract) = g ∘ map f
    rewrite map_to_cobind.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
g: W B -> C
f: A -> B
g ∘ cobind (f ∘ extract) = g ∘ cobind (f ∘ extract)
    reflexivity.
  Qed.

  Lemma kc1_01 {A B C} : forall (g : B -> C) (f : W A -> B),
      (g ∘ extract) ⋆1 f = g ∘ f.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
forall (g : B -> C) (f : W A -> B),
g ∘ extract ⋆1 f = g ∘ f
  Proof.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
forall (g : B -> C) (f : W A -> B),
g ∘ extract ⋆1 f = g ∘ f
    intros.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
g: B -> C
f: W A -> B
g ∘ extract ⋆1 f = g ∘ f
    unfold kc1.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
g: B -> C
f: W A -> B
g ∘ extract ∘ cobind f = g ∘ f
    reassociate ->.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
g: B -> C
f: W A -> B
g ∘ (extract ∘ cobind f) = g ∘ f
    rewrite kcom_cobind0.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
g: B -> C
f: W A -> B
g ∘ f = g ∘ f
    reflexivity.
  Qed.

  Lemma kc1_00 {A B C} : forall (g : B -> C) (f : A -> B),
      (g ∘ extract) ⋆1 (f ∘ extract) = (g ∘ f) ∘ extract.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
forall (g : B -> C) (f : A -> B),
g ∘ extract ⋆1 f ∘ extract = g ∘ f ∘ extract
  Proof.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
forall (g : B -> C) (f : A -> B),
g ∘ extract ⋆1 f ∘ extract = g ∘ f ∘ extract
    intros.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
g: B -> C
f: A -> B
g ∘ extract ⋆1 f ∘ extract = g ∘ f ∘ extract
    unfold kc1.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
g: B -> C
f: A -> B
g ∘ extract ∘ cobind (f ∘ extract) = g ∘ f ∘ extract
    reassociate ->.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
g: B -> C
f: A -> B
g ∘ (extract ∘ cobind (f ∘ extract)) = g ∘ f ∘ extract
    rewrite kcom_cobind0.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
g: B -> C
f: A -> B
g ∘ (f ∘ extract) = g ∘ f ∘ extract
    reflexivity.
  Qed.

  (** *** Other rules for Kleisli composition *)
  (********************************************************************)
  Lemma kc1_asc1: forall `(h: W C -> D) `(g: B -> C) `(f: W A -> B),
      h ⋆1 (g ∘ f) = (h ∘ map g) ⋆1 f.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
forall (C D : Type) (h : W C -> D) (B : Type)
  (g : B -> C) (A : Type) (f : W A -> B),
h ⋆1 g ∘ f = h ∘ map g ⋆1 f
  Proof.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
forall (C D : Type) (h : W C -> D) (B : Type)
  (g : B -> C) (A : Type) (f : W A -> B),
h ⋆1 g ∘ f = h ∘ map g ⋆1 f
    intros.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
C, D: Type
h: W C -> D
B: Type
g: B -> C
A: Type
f: W A -> B
h ⋆1 g ∘ f = h ∘ map g ⋆1 f
    unfold kc1.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
C, D: Type
h: W C -> D
B: Type
g: B -> C
A: Type
f: W A -> B
h ∘ cobind (g ∘ f) = h ∘ map g ∘ cobind f
    reassociate ->.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
C, D: Type
h: W C -> D
B: Type
g: B -> C
A: Type
f: W A -> B
h ∘ cobind (g ∘ f) = h ∘ (map g ∘ cobind f)
    rewrite map_to_cobind.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
C, D: Type
h: W C -> D
B: Type
g: B -> C
A: Type
f: W A -> B
h ∘ cobind (g ∘ f) =
h ∘ (cobind (g ∘ extract) ∘ cobind f)
    rewrite kcom_cobind2.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
C, D: Type
h: W C -> D
B: Type
g: B -> C
A: Type
f: W A -> B
h ∘ cobind (g ∘ f) = h ∘ cobind (g ∘ extract ⋆1 f)
    rewrite kc1_01.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
C, D: Type
h: W C -> D
B: Type
g: B -> C
A: Type
f: W A -> B
h ∘ cobind (g ∘ f) = h ∘ cobind (g ∘ f)
    reflexivity.
  Qed.

  Lemma kc1_asc2: forall `(h: C -> D) `(g: W B -> C) `(f: W A -> B),
      (h ∘ g) ⋆1 f = h ∘ (g ⋆1 f).
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
forall (C D : Type) (h : C -> D) (B : Type)
  (g : W B -> C) (A : Type) (f : W A -> B),
h ∘ g ⋆1 f = h ∘ (g ⋆1 f)
  Proof.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
forall (C D : Type) (h : C -> D) (B : Type)
  (g : W B -> C) (A : Type) (f : W A -> B),
h ∘ g ⋆1 f = h ∘ (g ⋆1 f)
    intros.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
C, D: Type
h: C -> D
B: Type
g: W B -> C
A: Type
f: W A -> B
h ∘ g ⋆1 f = h ∘ (g ⋆1 f) unfold kc1.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
C, D: Type
h: C -> D
B: Type
g: W B -> C
A: Type
f: W A -> B
h ∘ g ∘ cobind f = h ∘ (g ∘ cobind f)
    reflexivity.
  Qed.

End derived_instances.

(** ** Derived Typeclass Instances *)
(**********************************************************************)
Module DerivedInstances.

  #[export] Instance Functor_Comonad
    (W : Type -> Type)
    `{Comonad W}
    `{Map W}
    `{! Compat_Map_Cobind W}: Functor W.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
Functor W
  Proof.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
Functor W
    constructor.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
forall A : Type, map id = id
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
    -
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
forall A : Type, map id = id intros.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A: Type
map id = id
      rewrite map_to_cobind.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A: Type
cobind (id ∘ extract) = id
      change (id ∘ ?x) with x.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A: Type
cobind extract = id
      rewrite kcom_cobind1.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A: Type
id = id
      reflexivity.
    -
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f) intros.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
f: A -> B
g: B -> C
map g ∘ map f = map (g ∘ f)
      rewrite map_to_cobind.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
f: A -> B
g: B -> C
cobind (g ∘ extract) ∘ map f = map (g ∘ f)
      rewrite map_to_cobind.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
f: A -> B
g: B -> C
cobind (g ∘ extract) ∘ cobind (f ∘ extract) =
map (g ∘ f)
      rewrite kcom_cobind2.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
f: A -> B
g: B -> C
cobind (g ∘ extract ⋆1 f ∘ extract) = map (g ∘ f)
      rewrite kc1_00.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
f: A -> B
g: B -> C
cobind (g ∘ f ∘ extract) = map (g ∘ f)
      rewrite map_to_cobind.
W: Type -> Type
H: Cobind W
H0: Extract W
H1: Comonad W
H2: Map W
Compat_Map_Cobind0: Compat_Map_Cobind W
A, B, C: Type
f: A -> B
g: B -> C
cobind (g ∘ f ∘ extract) = cobind (g ∘ f ∘ extract)
      reflexivity.
  Qed.

  Include DerivedOperations.

End DerivedInstances.

(** * Notations *)
(**********************************************************************)
Module Notations.
  Infix "⋆1" := (kc1) (at level 60) : tealeaves_scope.
End Notations.