From Tealeaves Require Export
  Functors.Early.Reader.
From Tealeaves Require Import
  Classes.Kleisli.Comonad.

Import Kleisli.Comonad.Notations.

#[local] Generalizable Variables E T.

(** * Decorated Functors *)
(**********************************************************************)

(** ** <<mapd>> Operation *)
(**********************************************************************)
Class Mapd (E: Type) (T: Type -> Type) :=
  mapd: forall (A B: Type), (E * A -> B) -> T A -> T B.

#[global] Arguments mapd {E}%type_scope {T}%function_scope
  {Mapd} {A B}%type_scope _%function_scope _.

(** ** Kleisli Composition *)
(** Kleisli composition is [kc1] *)
(**********************************************************************)

(** ** Typeclasses *)
(**********************************************************************)
Class DecoratedFunctor (E: Type) (T: Type -> Type) `{Mapd E T} :=
  { kdf_mapd1: forall (A: Type),
      mapd (extract (A := A)) = @id (T A);
    kdf_mapd2: forall (A B C: Type) (g: E * B -> C) (f: E * A -> B),
      mapd g ∘ mapd f = mapd (g ⋆1 f);
  }.

(** ** Homomorphisms between Decorated Functors *)
(**********************************************************************)
Class DecoratedHom
  (E: Type) (T1 T2: Type -> Type)
  (ϕ: forall A: Type, T1 A -> T2 A)
  `{Mapd E T1} `{Mapd E T2} :=
  { dhom_natural:
    forall (A B: Type) (f: E * A -> B), mapd f ∘ ϕ A = ϕ B ∘ mapd f;
  }.

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

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

  #[export] Instance Map_Mapd
    (E: Type)
    (T: Type -> Type)
    `{Mapd_ET: Mapd E T}: Map T :=
  fun (A B: Type) (f: A -> B) => mapd (f ∘ extract).

End DerivedOperations.

Class Compat_Map_Mapd (E: Type) (T: Type -> Type)
  `{Map_T: Map T}
  `{Mapd_ET: Mapd E T}: Prop :=
  compat_map_mapd:
    Map_T = @DerivedOperations.Map_Mapd E T Mapd_ET.

#[export] Instance Compat_Map_Mapd_Self
  `{Mapd_ET: Mapd E T}:
  Compat_Map_Mapd E T (Map_T := DerivedOperations.Map_Mapd E T).
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
Compat_Map_Mapd E T
Proof.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
Compat_Map_Mapd E T
  reflexivity.
Qed.

Corollary map_to_mapd
  `{Compat_Map_Mapd E T}: forall (A B: Type) (f: A -> B),
    map f = mapd (f ∘ extract).
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
H: Compat_Map_Mapd E T
forall (A B : Type) (f : A -> B),
map f = mapd (f ∘ extract)
Proof.
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
H: Compat_Map_Mapd E T
forall (A B : Type) (f : A -> B),
map f = mapd (f ∘ extract)
  rewrite compat_map_mapd.
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
H: Compat_Map_Mapd E T
forall (A B : Type) (f : A -> B),
DerivedOperations.Map_Mapd E T A B f =
mapd (f ∘ extract)
  reflexivity.
Qed.

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

  Context
    `{DecoratedFunctor E T}
    `{Map_T: Map T}
    `{! Compat_Map_Mapd E T}.

  Lemma map_mapd:
    forall (A B C: Type)
      (g: B -> C)
      (f: E * A -> B),
      map g ∘ mapd f = mapd (g ∘ f).
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
forall (A B C : Type) (g : B -> C) (f : E * A -> B),
map g ∘ mapd f = mapd (g ∘ f)
  Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
forall (A B C : Type) (g : B -> C) (f : E * A -> B),
map g ∘ mapd f = mapd (g ∘ f)
    intros.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
g: B -> C
f: E * A -> B
map g ∘ mapd f = mapd (g ∘ f)
    rewrite map_to_mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
g: B -> C
f: E * A -> B
mapd (g ∘ extract) ∘ mapd f = mapd (g ∘ f)
    rewrite kdf_mapd2.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
g: B -> C
f: E * A -> B
mapd (g ∘ extract ⋆1 f) = mapd (g ∘ f)
    rewrite kc1_01.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
g: B -> C
f: E * A -> B
mapd (g ∘ f) = mapd (g ∘ f)
    reflexivity.
  Qed.

  Lemma mapd_map:
    forall (A B C: Type) (g: E * B -> C) (f: A -> B),
      mapd g ∘ map f = mapd (g ∘ map f).
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
forall (A B C : Type) (g : E * B -> C) (f : A -> B),
mapd g ∘ map f = mapd (g ∘ map f)
  Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
forall (A B C : Type) (g : E * B -> C) (f : A -> B),
mapd g ∘ map f = mapd (g ∘ map f)
    intros.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
g: E * B -> C
f: A -> B
mapd g ∘ map f = mapd (g ∘ map f)
    rewrite map_to_mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
g: E * B -> C
f: A -> B
mapd g ∘ mapd (f ∘ extract) = mapd (g ∘ map f)
    rewrite kdf_mapd2.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
g: E * B -> C
f: A -> B
mapd (g ⋆1 f ∘ extract) = mapd (g ∘ map f)
    rewrite kc1_10.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
g: E * B -> C
f: A -> B
mapd (g ∘ map f) = mapd (g ∘ map f)
    reflexivity.
  Qed.

  Lemma map_map: forall (A B C: Type) (f: A -> B) (g: B -> C),
      map g ∘ map f = map (F := T) (g ∘ f).
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
  Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
    intros.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
f: A -> B
g: B -> C
map g ∘ map f = map (g ∘ f)
    rewrite map_to_mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
f: A -> B
g: B -> C
mapd (g ∘ extract) ∘ map f = map (g ∘ f)
    rewrite map_to_mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
f: A -> B
g: B -> C
mapd (g ∘ extract) ∘ mapd (f ∘ extract) = map (g ∘ f)
    rewrite kdf_mapd2.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
f: A -> B
g: B -> C
mapd (g ∘ extract ⋆1 f ∘ extract) = map (g ∘ f)
    rewrite kc1_00.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
f: A -> B
g: B -> C
mapd (g ∘ f ∘ extract) = map (g ∘ f)
    rewrite map_to_mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A, B, C: Type
f: A -> B
g: B -> C
mapd (g ∘ f ∘ extract) = mapd (g ∘ f ∘ extract)
    reflexivity.
  Qed.

  Lemma map_id: forall (A: Type),
      map (@id A) = @id (T A).
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
forall A : Type, map id = id
  Proof.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
forall A : Type, map id = id
    intros.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A: Type
map id = id
    rewrite map_to_mapd.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A: Type
mapd (id ∘ extract) = id
    change (id ∘ ?f) with f.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A: Type
mapd extract = id
    rewrite kdf_mapd1.
E: Type
T: Type -> Type
H: Mapd E T
H0: DecoratedFunctor E T
Map_T: Map T
Compat_Map_Mapd0: Compat_Map_Mapd E T
A: Type
id = id
    reflexivity.
  Qed.

End derived_instances.

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

  #[export] Instance Functor_DecoratedFunctor
    (E: Type) (T: Type -> Type)
    `{DecoratedFunctor_ET: DecoratedFunctor E T}
    `{Map_T: Map T}
    `{! Compat_Map_Mapd E T}:
  Classes.Functor.Functor T :=
  {| fun_map_id := map_id;
     fun_map_map := map_map;
  |}.

  Include DerivedOperations.

End DerivedInstances.

(** * Instance for Reader *)
(**********************************************************************)
Import Product.Notations.

Section decorated_functor_reader.

  Context {E: Type}.

  #[export] Instance Mapd_Reader: Mapd E (E ×) :=
    @cobind (E ×) (Cobind_reader E).

  #[export] Instance DecoratedFunctor_Reader:
    DecoratedFunctor E (E ×).
E: Type
DecoratedFunctor E (prod E)
  Proof.
E: Type
DecoratedFunctor E (prod E)
    constructor;
      unfold_ops @Mapd_Reader; intros.
E, A: Type
cobind extract = id
E, A, B, C: Type
g: E * B -> C
f: E * A -> B
cobind g ∘ cobind f = cobind (g ⋆1 f)
    -
E, A: Type
cobind extract = id apply kcom_cobind1.
    -
E, A, B, C: Type
g: E * B -> C
f: E * A -> B
cobind g ∘ cobind f = cobind (g ⋆1 f) apply kcom_cobind2.
  Qed.

End decorated_functor_reader.