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

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

#[local] Generalizable Variables T E A B C.

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

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

  #[export] Instance Decorate_Mapd
    (E: Type) (T: Type -> Type) `{Mapd_ET: Mapd E T}:
  Decorate E T := fun A => mapd (@id ((E ×) A)).

End DerivedOperations.

(** ** Compatibility Classes *)
(**********************************************************************)
Class Compat_Decorate_Mapd
    (E: Type)
    (F: Type -> Type)
    `{Decorate_EF: Decorate E F}
    `{Mapd_F: Mapd E F} :=
  compat_dec_kleisli:
    Decorate_EF = @DerivedOperations.Decorate_Mapd E F Mapd_F.

Lemma dec_to_mapd {E F}
    `{Decorate_EF: Decorate E F}
    `{Mapd_F: Mapd E F}
    `{Compat: Compat_Decorate_Mapd E F}:
  forall (A: Type) (t: F A),
    dec F t = mapd id t.
E: Type
F: Type -> Type
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
Decorate_EF0: Decorate E F
Mapd_F0: Mapd E F
Compat: Compat_Decorate_Mapd E F
forall (A : Type) (t : F A), dec F t = mapd id t
Proof.
E: Type
F: Type -> Type
Decorate_EF: Decorate E F
Mapd_F: Mapd E F
Decorate_EF0: Decorate E F
Mapd_F0: Mapd E F
Compat: Compat_Decorate_Mapd E F
forall (A : Type) (t : F A), dec F t = mapd id t
  now rewrite compat_dec_kleisli.
Qed.

(** ** Derived Decorated Functor Laws *)
(**********************************************************************)
Module DerivedInstances.

  Section properties.

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

    (* Alectryon doesn't like this
       Import KleisliToCategorical.DecoratedFunctor.DerivedOperations.
     *)
    Import DerivedOperations.
    Import Kleisli.DecoratedFunctor.DerivedOperations.
    Import Kleisli.DecoratedFunctor.DerivedInstances.

    Lemma cojoin_spec: forall (A: Type),
        cojoin (W := (E ×)) =
          id (A := E * (E * A)) ⋆1 id (A := E * A).
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
forall A : Type, cojoin = id ⋆1 id
    Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
forall A : Type, cojoin = id ⋆1 id
      intros.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A: Type
cojoin = id ⋆1 id
      unfold kc1.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A: Type
cojoin = id ∘ cobind id
      reflexivity.
    Qed.

    Lemma dec_dec: forall (A: Type),
        dec T ∘ dec T = map (cojoin (W := (E ×))) ∘ dec T (A := A).
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
forall A : Type, dec T ∘ dec T = map cojoin ∘ dec T
    Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
forall A : Type, dec T ∘ dec T = map cojoin ∘ dec T
      intros.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A: Type
dec T ∘ dec T = map cojoin ∘ dec T
      unfold_ops @Decorate_Mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A: Type
mapd id ∘ mapd id = map cojoin ∘ mapd id
      rewrite kdf_mapd2.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A: Type
mapd (id ⋆1 id) = map cojoin ∘ mapd id
      rewrite <- cojoin_spec.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A: Type
mapd cojoin = map cojoin ∘ mapd id
      rewrite map_mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A: Type
mapd cojoin = mapd (cojoin ∘ id)
      reflexivity.
    Qed.

    Lemma dec_extract: forall (A: Type),
        map (F := T) extract ∘ dec T = @id (T A).
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
forall A : Type, map extract ∘ dec T = id
    Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
forall A : Type, map extract ∘ dec T = id
      intros.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A: Type
map extract ∘ dec T = id
      unfold_ops @Decorate_Mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A: Type
map extract ∘ mapd id = id
      rewrite map_mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A: Type
mapd (extract ∘ id) = id
      change (?f ∘ id) with f.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A: Type
mapd extract = id
      rewrite kdf_mapd1.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A: Type
id = id
      reflexivity.
    Qed.

    Lemma dec_natural: Natural (@dec E T _).
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
Natural (@dec E T (Decorate_Mapd E T))
    Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
Natural (@dec E T (Decorate_Mapd E T))
      constructor.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
Functor T
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
Functor (T ○ prod E)
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
forall (A B : Type) (f : A -> B),
map f ∘ dec T = dec T ∘ map f
      -
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
Functor T typeclasses eauto.
      -
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
Functor (T ○ prod E) typeclasses eauto.
      -
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
forall (A B : Type) (f : A -> B),
map f ∘ dec T = dec T ∘ map f intros.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: A -> B
map f ∘ dec T = dec T ∘ map f
        unfold_ops @Map_compose.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: A -> B
map (map f) ∘ dec T = dec T ∘ map f
        unfold_ops @Decorate_Mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: A -> B
map (map f) ∘ mapd id = mapd id ∘ map f
        rewrite map_mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: A -> B
mapd (map f ∘ id) = mapd id ∘ map f
        rewrite mapd_map.
E: Type
T: Type -> Type
H: Mapd E T
H0: Kleisli.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: A -> B
mapd (map f ∘ id) = mapd (id ∘ map f)
        reflexivity.
    Qed.

    #[export] Instance CategoricalDecoratedFunctor_Kleisli:
      Categorical.DecoratedFunctor.DecoratedFunctor E T :=
      {| dfun_dec_natural := dec_natural;
         dfun_dec_dec := dec_dec;
         dfun_dec_extract := dec_extract;
      |}.

  End properties.

End DerivedInstances.