From Tealeaves Require Export
  Classes.Functor
  Classes.Categorical.Monad.

Import Functor.Notations.

#[local] Generalizable Variables T U A.
#[local] Arguments map F%function_scope {Map}
  {A B}%type_scope f%function_scope _.
#[local] Arguments join T%function_scope {Join}
  {A}%type_scope _.
#[local] Arguments ret T%function_scope {Return}
  (A)%type_scope _.

(** * Right modules *)
(**********************************************************************)

(** ** Operation *)
(**********************************************************************)
Class RightAction (T U: Type -> Type) :=
  right_action: T ∘ U ⇒ T.

#[global] Arguments right_action (T)%function_scope {U}
  {RightAction} {A}%type_scope _.
#[local] Arguments right_action (T U)%function_scope
  {RightAction} A%type_scope _.

(** ** Typeclass *)
(**********************************************************************)
Class RightModule
  (T U: Type -> Type)
  `{Map U} `{Return U} `{Join U}
  `{Map T} `{RightAction T U} :=
  { mod_object :> Functor T;
    mon_monoid :> Monad U;
    mod_natural :> Natural (right_action T U);
    mod_action_map_ret:
    `(right_action T U A ∘ map T (ret U A) = @id (T A));
    mod_action_action:
    `(right_action T U A ∘ right_action T U (U A) =
        right_action T U A ∘ map T (join U));
  }.

(** * Coercing Monads into Right Modules *)
(**********************************************************************)
Module MonadToModule.

  #[export] Instance RightAction_Join `{Join T}:
  RightAction T T := @join T _.

  #[export] Instance RightModule_Monad `{Monad T}: RightModule T T :=
    {| mod_action_map_ret := mon_join_map_ret (T := T);
       mod_action_action := mon_join_join (T := T);
    |}.

End MonadToModule.

(** ** Right Modules Compose with Functors *)
(**********************************************************************)
Section functor_module_composition.

  #[local] Generalizable Variables F G.

  Context
    `{Functor T1}
    `{RightModule T2 U}.

  #[global] Instance RightAction_compose: RightAction (T1 ∘ T2) U :=
    fun A => @map T1 _ (T2 (U A)) (T2 A) (right_action T2 U A).

  #[local] Set Keyed Unification.

  (** It does not seem to be a good idea to add this globally. It is
      better to use it explicitly. *)
  Instance RightModule_compose: RightModule (T1 ∘ T2) U.
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
RightModule (T1 ∘ T2) U
  Proof.
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
RightModule (T1 ∘ T2) U
    constructor; try typeclasses eauto.
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
Natural (right_action (T1 ∘ T2) U)
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
forall A : Type,
right_action (T1 ∘ T2) U A ∘ map (T1 ∘ T2) (ret U A) =
id
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
forall A : Type,
right_action (T1 ∘ T2) U A
∘ right_action (T1 ∘ T2) U (U A) =
right_action (T1 ∘ T2) U A ∘ map (T1 ∘ T2) (join U)
    -
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
Natural (right_action (T1 ∘ T2) U) constructor; try typeclasses eauto.
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
forall (A B : Type) (f : A -> B),
map (T1 ∘ T2) f ∘ right_action (T1 ∘ T2) U A =
right_action (T1 ∘ T2) U B ∘ map (T1 ∘ T2 ∘ U) f
      introv.
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
A, B: Type
f: A -> B
map (T1 ∘ T2) f ∘ right_action (T1 ∘ T2) U A =
right_action (T1 ∘ T2) U B ∘ map (T1 ∘ T2 ∘ U) f unfold transparent tcs.
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
A, B: Type
f: A -> B
map T1 (map T2 f) ∘ map T1 (right_action T2 U A) =
map T1 (right_action T2 U B)
∘ map T1 (map T2 (map U f))
      unfold_compose_in_compose.
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
A, B: Type
f: A -> B
map T1 (map T2 f) ∘ map T1 (right_action T2 U A) =
map T1 (right_action T2 U B)
∘ map T1 (map T2 (map U f))
      rewrite 2(fun_map_map (F := T1)).
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
A, B: Type
f: A -> B
map T1 (map T2 f ∘ right_action T2 U A) =
map T1 (right_action T2 U B ∘ map T2 (map U f))
      now rewrite (natural (G := T2) (F := T2 ∘ U)).
    -
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
forall A : Type,
right_action (T1 ∘ T2) U A ∘ map (T1 ∘ T2) (ret U A) =
id intros.
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
A: Type
right_action (T1 ∘ T2) U A ∘ map (T1 ∘ T2) (ret U A) =
id unfold_ops @RightAction_compose @Map_compose.
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
A: Type
map T1 (right_action T2 U A)
∘ map T1 (map T2 (ret U A)) = id
      rewrite (fun_map_map (F := T1)).
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
A: Type
map T1 (right_action T2 U A ∘ map T2 (ret U A)) = id
      rewrite (mod_action_map_ret (T := T2) (U := U)).
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
A: Type
map T1 id = id
      now rewrite (fun_map_id (F := T1)).
    -
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
forall A : Type,
right_action (T1 ∘ T2) U A
∘ right_action (T1 ∘ T2) U (U A) =
right_action (T1 ∘ T2) U A ∘ map (T1 ∘ T2) (join U) intros.
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
A: Type
right_action (T1 ∘ T2) U A
∘ right_action (T1 ∘ T2) U (U A) =
right_action (T1 ∘ T2) U A ∘ map (T1 ∘ T2) (join U) unfold_ops @RightAction_compose @Map_compose.
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
A: Type
map T1 (right_action T2 U A)
∘ map T1 (right_action T2 U (U A)) =
map T1 (right_action T2 U A)
∘ map T1 (map T2 (join U))
      rewrite 2(fun_map_map (F := T1)).
T1: Type -> Type
Map_F: Map T1
H: Functor T1
T2, U: Type -> Type
H0: Map U
H1: Return U
H2: Join U
H3: Map T2
H4: RightAction T2 U
H5: RightModule T2 U
A: Type
map T1 (right_action T2 U A ∘ right_action T2 U (U A)) =
map T1 (right_action T2 U A ∘ map T2 (join U))
      now rewrite (mod_action_action (T := T2) (U := U)).
  Qed.

End functor_module_composition.