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.

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.

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}:
  ∀ (A: Type) (t: F A),
    dec F t = mapd id t.
Proof.
  now rewrite compat_dec_kleisli.
Qed.

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: ∀ (A: Type),
        cojoin (W := (E ×)) =
          id (A := E × (E × A)) ⋆1 id (A := E × A).
    Proof.
      intros.
      unfold kc1.
      reflexivity.
    Qed.

    Lemma dec_dec: ∀ (A: Type),
        dec T ∘ dec T = map (cojoin (W := (E ×))) ∘ dec T (A := A).
    Proof.
      intros.
      unfold_ops @Decorate_Mapd.
      rewrite kdf_mapd2.
      rewrite <- cojoin_spec.
      rewrite map_mapd.
      reflexivity.
    Qed.

    Lemma dec_extract: ∀ (A: Type),
        map (F := T) extract ∘ dec T = @id (T A).
    Proof.
      intros.
      unfold_ops @Decorate_Mapd.
      rewrite map_mapd.
      change (?f ∘ id) with f.
      rewrite kdf_mapd1.
      reflexivity.
    Qed.

    Lemma dec_natural: Natural (@dec E T _).
    Proof.
      constructor.
      - typeclasses eauto.
      - typeclasses eauto.
      - intros.
        unfold_ops @Map_compose.
        unfold_ops @Decorate_Mapd.
        rewrite map_mapd.
        rewrite mapd_map.
        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.