From Tealeaves Require Import
  Classes.Categorical.DecoratedFunctor
  Classes.Kleisli.DecoratedFunctor
  Classes.Kleisli.Comonad (kc1, cobind)
  CategoricalToKleisli.Comonad.

#[local] Generalizable Variables E F.

Import Product.Notations.
Import Kleisli.Comonad.Notations.

(** * Categorical Decorated Functors to Kleisli Decorated Functors *)
(**********************************************************************)

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

  #[export] Instance Mapd_Categorical
    (E: Type)
    (F: Type -> Type)
    `{Map_F: Map F}
    `{Decorate_EF: Decorate E F}: Mapd E F :=
  fun A B (f: E * A -> B) => map (F := F) f ∘ dec F.

End DerivedOperations.

(** ** Compatibility Classes *)
(**********************************************************************)
Class Compat_Mapd_Categorical
    (E: Type)
    (F: Type -> Type)
    `{Map_F: Map F}
    `{Decorate_EF: Decorate E F}
    `{Mapd_F: Mapd E F} :=
  compat_mapd_categorical:
    Mapd_F = @DerivedOperations.Mapd_Categorical E F Map_F Decorate_EF.

Lemma mapd_to_categorical {E F}
    `{Map_F: Map F}
    `{Decorate_EF: Decorate E F}
    `{Mapd_F: Mapd E F}
    `{Compat: Compat_Mapd_Categorical E F}:
  forall (A B: Type) (f: E * A -> B) (t: F A),
    mapd f t = map f (dec F t).
E: Type
F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
Map_F0: Map F
Decorate_EF0: Decorate E F
Mapd_F0: Mapd E F
Compat: Compat_Mapd_Categorical E F
forall (A B : Type) (f : E * A -> B) (t : F A),
mapd f t = map f (dec F t)
Proof.
E: Type
F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
Map_F0: Map F
Decorate_EF0: Decorate E F
Mapd_F0: Mapd E F
Compat: Compat_Mapd_Categorical E F
forall (A B : Type) (f : E * A -> B) (t : F A),
mapd f t = map f (dec F t)
  now rewrite compat_mapd_categorical.
Qed.

(** ** Interaction of <<dec>> with <<mapd>> *)
(**********************************************************************)
Section decorate_after_mapd_reasoning.

  Context
    (E: Type)
    (T: Type -> Type)
    `{Map_F: Map F}
    `{Decorate_EF: Decorate E F}
    `{Mapd_F: Mapd E F}
    `{DecFun_EF: ! Categorical.DecoratedFunctor.DecoratedFunctor E F}
    `{Compat: ! Compat_Mapd_Categorical E F}.

  Context {A B: Type} {f: E * A -> B} (t: F A).

  Lemma dec_mapd:
    dec F (mapd f t) =
      (mapd (T := F) (map f) (dec F t)).
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
dec F (mapd f t) = mapd (map f) (dec F t)
  Proof.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
dec F (mapd f t) = mapd (map f) (dec F t)
    intros.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
dec F (mapd f t) = mapd (map f) (dec F t)
    rewrite mapd_to_categorical.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
dec F (map f (dec F t)) = mapd (map f) (dec F t)
    compose near (dec F t) on left.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
(dec F ∘ map f) (dec F t) = mapd (map f) (dec F t)
    inversion DecFun_EF.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
dfun_functor: Functor F
dfun_dec_natural: Natural (@dec E F Decorate_EF)
dfun_dec_dec: forall A : Type,
dec F ∘ dec F = map cojoin ∘ dec F
dfun_dec_extract: forall A : Type,
map extract ∘ dec F = id
(dec F ∘ map f) (dec F t) = mapd (map f) (dec F t)
    rewrite <- (natural (ϕ := @dec E F _)).
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
dfun_functor: Functor F
dfun_dec_natural: Natural (@dec E F Decorate_EF)
dfun_dec_dec: forall A : Type,
dec F ∘ dec F = map cojoin ∘ dec F
dfun_dec_extract: forall A : Type,
map extract ∘ dec F = id
(map f ∘ dec F) (dec F t) = mapd (map f) (dec F t)
    unfold compose.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
dfun_functor: Functor F
dfun_dec_natural: Natural (@dec E F Decorate_EF)
dfun_dec_dec: forall A : Type,
dec F ∘ dec F = map cojoin ∘ dec F
dfun_dec_extract: forall A : Type,
map extract ∘ dec F = id
map f (dec F (dec F t)) = mapd (map f) (dec F t)
    rewrite mapd_to_categorical.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
dfun_functor: Functor F
dfun_dec_natural: Natural (@dec E F Decorate_EF)
dfun_dec_dec: forall A : Type,
dec F ∘ dec F = map cojoin ∘ dec F
dfun_dec_extract: forall A : Type,
map extract ∘ dec F = id
map f (dec F (dec F t)) =
map (map f) (dec F (dec F t))
    reflexivity.
  Qed.

  Lemma dec_mapd2:
    dec F (mapd f t) =
      (map (F := F) (cobind f) (dec F t)).
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
dec F (mapd f t) = map (cobind f) (dec F t)
  Proof.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
dec F (mapd f t) = map (cobind f) (dec F t)
    intros.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
dec F (mapd f t) = map (cobind f) (dec F t)
    rewrite dec_mapd.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
mapd (map f) (dec F t) = map (cobind f) (dec F t)
    rewrite mapd_to_categorical.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
map (map f) (dec F (dec F t)) =
map (cobind f) (dec F t)
    compose near t on left.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
map (map f) ((dec F ∘ dec F) t) =
map (cobind f) (dec F t)
    rewrite dfun_dec_dec.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
map (map f) ((map cojoin ∘ dec F) t) =
map (cobind f) (dec F t)
    unfold compose.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
map (map f) (map cojoin (dec F t)) =
map (cobind f) (dec F t)
    compose near (dec F t) on left.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
(map (map f) ∘ map cojoin) (dec F t) =
map (cobind f) (dec F t)
    rewrite fun_map_map.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
map (map f ∘ cojoin) (dec F t) =
map (cobind f) (dec F t)
    fequal.
E: Type
T, F: Type -> Type
Map_F: Map F
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
DecFun_EF: Categorical.DecoratedFunctor.DecoratedFunctor
  E F
Compat: Compat_Mapd_Categorical E F
A, B: Type
f: E * A -> B
t: F A
map f ∘ cojoin = cobind f
    now ext [e a].
  Qed.

End decorate_after_mapd_reasoning.

(** ** Derived co-Kleisli Laws *)
(**********************************************************************)
Module DerivedInstances.

  (* Alectryon doesn't like this
     Import CategoricalToKleisli.DecoratedFunctor.DerivedOperations.
   *)
  Import DerivedOperations.
  Import CategoricalToKleisli.Comonad.DerivedOperations.

  Section with_functor.

    Context
      (F: Type -> Type)
      `{Classes.Categorical.DecoratedFunctor.DecoratedFunctor E F}.

    Theorem mapd_id {A}:
      @mapd E F _ A A (extract (W := (E ×))) = @id (F A).
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A: Type
mapd extract = id
    Proof.
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A: Type
mapd extract = id
      introv.
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A: Type
mapd extract = id
      unfold mapd.
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A: Type
Mapd_Categorical E F A A extract = id
      unfold Mapd_Categorical.
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A: Type
map extract ∘ dec F = id
      rewrite dfun_dec_extract.
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A: Type
id = id
      reflexivity.
    Qed.

    Theorem mapd_mapd (A B C: Type) (g: E * B -> C) (f: E * A -> B):
      @mapd E F _ B C g ∘ @mapd E F _ A B f = @mapd E F _ A C (kc1 g f).
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
mapd g ∘ mapd f = mapd (g ⋆1 f)
    Proof.
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
mapd g ∘ mapd f = mapd (g ⋆1 f)
      unfold_ops @Mapd_Categorical.
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
map g ∘ dec F ∘ (map f ∘ dec F) = map (g ⋆1 f) ∘ dec F
      reassociate <- on left.
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
map g ∘ dec F ∘ map f ∘ dec F = map (g ⋆1 f) ∘ dec F
      reassociate -> near (map f).
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
map g ∘ (dec F ∘ map f) ∘ dec F = map (g ⋆1 f) ∘ dec F
      rewrite <- (natural (G := F ○ prod E)).
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
map g ∘ (map f ∘ dec F) ∘ dec F = map (g ⋆1 f) ∘ dec F
      reassociate <- on left.
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
map g ∘ map f ∘ dec F ∘ dec F = map (g ⋆1 f) ∘ dec F
      unfold transparent tcs.
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
map g ∘ map (map_snd f) ∘ dec F ∘ dec F =
map (g ⋆1 f) ∘ dec F
      rewrite (fun_map_map (F := F)).
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
map (g ∘ map_snd f) ∘ dec F ∘ dec F =
map (g ⋆1 f) ∘ dec F
      reassociate -> on left.
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
map (g ∘ map_snd f) ∘ (dec F ∘ dec F) =
map (g ⋆1 f) ∘ dec F
      rewrite (dfun_dec_dec).
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
map (g ∘ map_snd f) ∘ (map cojoin ∘ dec F) =
map (g ⋆1 f) ∘ dec F
      reassociate <- on left.
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
map (g ∘ map_snd f) ∘ map cojoin ∘ dec F =
map (g ⋆1 f) ∘ dec F
      rewrite (fun_map_map (F := F)).
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
map (g ∘ map_snd f ∘ cojoin) ∘ dec F =
map (g ⋆1 f) ∘ dec F
      repeat fequal.
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
g ∘ map_snd f ∘ cojoin = g ⋆1 f
      ext [e a].
F: Type -> Type
E: Type
H: Map F
H0: Decorate E F
H1: Categorical.DecoratedFunctor.DecoratedFunctor E F
A, B, C: Type
g: E * B -> C
f: E * A -> B
e: E
a: A
(g ∘ map_snd f ∘ cojoin) (e, a) = (g ⋆1 f) (e, a)
      reflexivity.
    Qed.

    (** ** Typeclass Instance *)
    (******************************************************************)
    #[export] Instance DecoratedFunctor:
      Kleisli.DecoratedFunctor.DecoratedFunctor E F :=
      {| kdf_mapd1 := @mapd_id;
         kdf_mapd2 := @mapd_mapd
      |}.

  End with_functor.

End DerivedInstances.

(** ** Miscellaneous Properties *)
(**********************************************************************)
Section DecoratedFunctor_misc.

  Context
    (T: Type -> Type)
    `{Categorical.DecoratedFunctor.DecoratedFunctor E T}.

  Theorem cobind_dec {A B}: forall (f: E * A -> B),
      map (F := T) (cobind (W := (E ×)) f) ∘ dec T =
        dec T ∘ map (F := T) f ∘ dec T.
T: Type -> Type
E: Type
H: Map T
H0: Decorate E T
H1: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
forall f : E * A -> B,
map (cobind f) ∘ dec T = dec T ∘ map f ∘ dec T
  Proof.
T: Type -> Type
E: Type
H: Map T
H0: Decorate E T
H1: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
forall f : E * A -> B,
map (cobind f) ∘ dec T = dec T ∘ map f ∘ dec T
    intros.
T: Type -> Type
E: Type
H: Map T
H0: Decorate E T
H1: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: E * A -> B
map (cobind f) ∘ dec T = dec T ∘ map f ∘ dec T
    unfold_ops @Cobind_reader.
T: Type -> Type
E: Type
H: Map T
H0: Decorate E T
H1: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: E * A -> B
map (fun '(e, a) => (e, f (e, a))) ∘ dec T =
dec T ∘ map f ∘ dec T
    rewrite <- (natural (ϕ := @dec E T _)).
T: Type -> Type
E: Type
H: Map T
H0: Decorate E T
H1: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: E * A -> B
map (fun '(e, a) => (e, f (e, a))) ∘ dec T =
map f ∘ dec T ∘ dec T
    unfold_ops @Map_compose.
T: Type -> Type
E: Type
H: Map T
H0: Decorate E T
H1: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: E * A -> B
map (fun '(e, a) => (e, f (e, a))) ∘ dec T =
map (map f) ∘ dec T ∘ dec T
    reassociate ->.
T: Type -> Type
E: Type
H: Map T
H0: Decorate E T
H1: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: E * A -> B
map (fun '(e, a) => (e, f (e, a))) ∘ dec T =
map (map f) ∘ (dec T ∘ dec T)
    rewrite  (dfun_dec_dec (E := E) (F := T)).
T: Type -> Type
E: Type
H: Map T
H0: Decorate E T
H1: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: E * A -> B
map (fun '(e, a) => (e, f (e, a))) ∘ dec T =
map (map f) ∘ (map cojoin ∘ dec T)
    reassociate <-.
T: Type -> Type
E: Type
H: Map T
H0: Decorate E T
H1: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: E * A -> B
map (fun '(e, a) => (e, f (e, a))) ∘ dec T =
map (map f) ∘ map cojoin ∘ dec T
    rewrite (fun_map_map (F := T)).
T: Type -> Type
E: Type
H: Map T
H0: Decorate E T
H1: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: E * A -> B
map (fun '(e, a) => (e, f (e, a))) ∘ dec T =
map (map f ∘ cojoin) ∘ dec T
    fequal.
T: Type -> Type
E: Type
H: Map T
H0: Decorate E T
H1: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: E * A -> B
map (fun '(e, a) => (e, f (e, a))) =
map (map f ∘ cojoin) fequal.
T: Type -> Type
E: Type
H: Map T
H0: Decorate E T
H1: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: E * A -> B
(fun '(e, a) => (e, f (e, a))) = map f ∘ cojoin
    now ext [e a].
  Qed.

End DecoratedFunctor_misc.