Library SSProve.Relational.RelativeMonads
From Coq Require Import ssreflect ssrfun.
From SSProve.Mon Require Export Base.
From Coq.Classes Require Import RelationClasses Morphisms.
From SSProve.Relational Require Import Category.
Set Primitive Projections.
Set Universe Polymorphism.
(*********************************************************)
From SSProve.Mon Require Export Base.
From Coq.Classes Require Import RelationClasses Morphisms.
From SSProve.Relational Require Import Category.
Set Primitive Projections.
Set Universe Polymorphism.
(*********************************************************)
Monad relative to a functor, morphisms underlying functor, monads as relative monads
Section RelativeMonad.
Context {C D : category} {J : functor C D}.
Cumulative Record relativeMonad :=
mkRelativeMonad
{ relmonObj :> C → D
; relmon_unit : ∀ A, D⦅J A; relmonObj A⦆
; relmon_bind : ∀ {A B}, D⦅J A; relmonObj B⦆ → D⦅relmonObj A; relmonObj B⦆
; relmon_bind_proper : ∀ A B,
Proper (@sim D (J A) (relmonObj B) ==> sim D) relmon_bind
; relmon_law1 : ∀ A, relmon_bind (relmon_unit A) ∼ Id _
; relmon_law2 : ∀ A B (f : D⦅J A; relmonObj B⦆),
relmon_bind f ∙ relmon_unit A ∼ f
; relmon_law3 : ∀ A B C (f : D⦅J B; relmonObj C⦆) (g:D⦅J A; relmonObj B⦆),
relmon_bind (relmon_bind f ∙ g) ∼ relmon_bind f ∙ relmon_bind g
}.
Global Existing Instance relmon_bind_proper.
End RelativeMonad.
Arguments relativeMonad {_ _} J.
Section RelativeMonadMorphism.
Context {C D1 D2 : category} {J1 : functor C D1} (J12 : functor D1 D2) {J2 : functor C D2}
(phi : natIso J2 (functor_comp J1 J12)) (psi := ni_inv phi)
(M1 : relativeMonad J1) (M2: relativeMonad J2).
Notation η := relmon_unit.
Notation rbind := relmon_bind.
Cumulative Record relativeMonadMorphism :=
mkRelMonMorph
{ rmm_map :> ∀ {A}, D2⦅J12 (M1 A); M2 A⦆
; rmm_law1 : ∀ A, rmm_map ∙ fmap J12 (η M1 A) ∼ η M2 A ∙ psi _
; rmm_law2 : ∀ A B (f : D1⦅J1 A; M1 B⦆),
rmm_map ∙ fmap J12 (rbind M1 f) ∼
rbind M2 (rmm_map ∙ fmap J12 f ∙ phi _) ∙ rmm_map
}.
End RelativeMonadMorphism.
Section RelativeMonadToFunctor.
Context {C D:category} {J:functor C D} (M : relativeMonad J).
Program Definition rmon_to_functor : functor C D :=
mkFunctor M (fun A B f ⇒ relmon_bind M (relmon_unit M _ ∙ fmap J f)) _ _ _.
Next Obligation. cbv ; intuition. rewrite H ; reflexivity. Qed.
Next Obligation. rewrite functor_law1 cat_law2 relmon_law1 ; reflexivity. Qed.
Next Obligation.
rewrite functor_law2 cat_law3.
rewrite -relmon_law3 cat_law3 relmon_law2.
reflexivity.
Qed.
End RelativeMonadToFunctor.
Section RmonadUnit.
Context {I C:category} {J:functor I C}
(M0 : relativeMonad J) (M := rmon_to_functor M0).
Program Definition rmon_unit : natTrans J M :=
mkNatTrans _ _ (relmon_unit M0) _.
Next Obligation. rewrite (relmon_law2 M0) ; reflexivity. Qed.
End RmonadUnit.
Section RMonadAsMonad.
Context {C:category} (M0 : relativeMonad (functor_id C)) (M := rmon_to_functor M0).
Program Definition rmon_id_mult : natTrans (functor_comp M M) M :=
mkNatTrans _ _ (fun⇒ relmon_bind M0 (Id _)) _.
Next Obligation.
rewrite -!relmon_law3 cat_law3 (relmon_law2 M0) cat_law1 cat_law2.
reflexivity.
Qed.
Notation η := (@rmon_unit C C (functor_id C) _ _).
Notation μ := (rmon_id_mult _).
Lemma rmon_id_law1 {A} : μ ∙ (fmap M η) ∼ Id (M A).
Proof. cbv. rewrite -relmon_law3 cat_law3 (relmon_law2 M0) cat_law1 relmon_law1. reflexivity. Qed.
Lemma rmon_id_law2 {A} : μ ∙ η ∼ Id (M A).
Proof. cbv. rewrite (relmon_law2 M0). reflexivity. Qed.
Lemma rmon_id_law3 {A} : μ ∙ μ ∼ μ ∙ fmap M (rmon_id_mult A).
Proof.
cbv. rewrite -!relmon_law3 !cat_law3 (relmon_law2 M0) cat_law2 cat_law1.
reflexivity.
Qed.
End RMonadAsMonad.
(* transport a J1-relative monad into a J2-relative monad along a natural isomorphism *)
Section RelativeMonadIso.
Context {I C} {J1 J2 : functor I C} (M : relativeMonad J1)
(phi : natIso J1 J2).
Program Definition rmon_transp_natIso : relativeMonad J2 :=
mkRelativeMonad M (fun A ⇒ relmon_unit M A ∙ ni_inv phi A)
(fun A B f ⇒ relmon_bind M (f ∙ phi A))
_ _ _ _.
Next Obligation. cbv ; intuition ; rewrite H ; reflexivity. Qed.
Next Obligation.
rewrite -cat_law3 ni_leftinv cat_law2 relmon_law1 ; reflexivity.
Qed.
Next Obligation.
rewrite cat_law3 relmon_law2 -cat_law3 ni_rightinv cat_law2 ; reflexivity.
Qed.
Next Obligation.
rewrite -cat_law3 relmon_law3 ; reflexivity.
Qed.
(* Surprisingly, we never use naturality... *)
End RelativeMonadIso.
(* Given functors
J1 : I1 -> C1
J2 : I2 -> C2,
J1-relative monad M1 and
J2-relative monad M2
builds a J1×J2-relative monad I1 × I2 -> C1 × C2
*)
Section ProductRelativeMonad.
Context {I1 I2 C1 C2} {J1 : functor I1 C1} {J2 : functor I2 C2}
(M1 : relativeMonad J1) (M2 : relativeMonad J2).
Program Definition product_rmon : relativeMonad (prod_functor J1 J2) :=
mkRelativeMonad (fun A ⇒ ⟨M1 (nfst A), M2 (nsnd A)⟩)
(fun A ⇒ ⟨relmon_unit M1 (nfst A), relmon_unit M2 (nsnd A)⟩)
(fun _ _ f ⇒ ⟨relmon_bind M1 (nfst f), relmon_bind M2 (nsnd f)⟩) _ _ _ _.
Next Obligation.
cbv ; intuition ; [rewrite H0 | rewrite H1] ; reflexivity.
Qed.
Next Obligation. intuition; rewrite relmon_law1; reflexivity. Qed.
Next Obligation. intuition; rewrite relmon_law2; reflexivity. Qed.
Next Obligation. intuition; rewrite relmon_law3; reflexivity. Qed.
End ProductRelativeMonad.
(*********************************************************)
Context {C D : category} {J : functor C D}.
Cumulative Record relativeMonad :=
mkRelativeMonad
{ relmonObj :> C → D
; relmon_unit : ∀ A, D⦅J A; relmonObj A⦆
; relmon_bind : ∀ {A B}, D⦅J A; relmonObj B⦆ → D⦅relmonObj A; relmonObj B⦆
; relmon_bind_proper : ∀ A B,
Proper (@sim D (J A) (relmonObj B) ==> sim D) relmon_bind
; relmon_law1 : ∀ A, relmon_bind (relmon_unit A) ∼ Id _
; relmon_law2 : ∀ A B (f : D⦅J A; relmonObj B⦆),
relmon_bind f ∙ relmon_unit A ∼ f
; relmon_law3 : ∀ A B C (f : D⦅J B; relmonObj C⦆) (g:D⦅J A; relmonObj B⦆),
relmon_bind (relmon_bind f ∙ g) ∼ relmon_bind f ∙ relmon_bind g
}.
Global Existing Instance relmon_bind_proper.
End RelativeMonad.
Arguments relativeMonad {_ _} J.
Section RelativeMonadMorphism.
Context {C D1 D2 : category} {J1 : functor C D1} (J12 : functor D1 D2) {J2 : functor C D2}
(phi : natIso J2 (functor_comp J1 J12)) (psi := ni_inv phi)
(M1 : relativeMonad J1) (M2: relativeMonad J2).
Notation η := relmon_unit.
Notation rbind := relmon_bind.
Cumulative Record relativeMonadMorphism :=
mkRelMonMorph
{ rmm_map :> ∀ {A}, D2⦅J12 (M1 A); M2 A⦆
; rmm_law1 : ∀ A, rmm_map ∙ fmap J12 (η M1 A) ∼ η M2 A ∙ psi _
; rmm_law2 : ∀ A B (f : D1⦅J1 A; M1 B⦆),
rmm_map ∙ fmap J12 (rbind M1 f) ∼
rbind M2 (rmm_map ∙ fmap J12 f ∙ phi _) ∙ rmm_map
}.
End RelativeMonadMorphism.
Section RelativeMonadToFunctor.
Context {C D:category} {J:functor C D} (M : relativeMonad J).
Program Definition rmon_to_functor : functor C D :=
mkFunctor M (fun A B f ⇒ relmon_bind M (relmon_unit M _ ∙ fmap J f)) _ _ _.
Next Obligation. cbv ; intuition. rewrite H ; reflexivity. Qed.
Next Obligation. rewrite functor_law1 cat_law2 relmon_law1 ; reflexivity. Qed.
Next Obligation.
rewrite functor_law2 cat_law3.
rewrite -relmon_law3 cat_law3 relmon_law2.
reflexivity.
Qed.
End RelativeMonadToFunctor.
Section RmonadUnit.
Context {I C:category} {J:functor I C}
(M0 : relativeMonad J) (M := rmon_to_functor M0).
Program Definition rmon_unit : natTrans J M :=
mkNatTrans _ _ (relmon_unit M0) _.
Next Obligation. rewrite (relmon_law2 M0) ; reflexivity. Qed.
End RmonadUnit.
Section RMonadAsMonad.
Context {C:category} (M0 : relativeMonad (functor_id C)) (M := rmon_to_functor M0).
Program Definition rmon_id_mult : natTrans (functor_comp M M) M :=
mkNatTrans _ _ (fun⇒ relmon_bind M0 (Id _)) _.
Next Obligation.
rewrite -!relmon_law3 cat_law3 (relmon_law2 M0) cat_law1 cat_law2.
reflexivity.
Qed.
Notation η := (@rmon_unit C C (functor_id C) _ _).
Notation μ := (rmon_id_mult _).
Lemma rmon_id_law1 {A} : μ ∙ (fmap M η) ∼ Id (M A).
Proof. cbv. rewrite -relmon_law3 cat_law3 (relmon_law2 M0) cat_law1 relmon_law1. reflexivity. Qed.
Lemma rmon_id_law2 {A} : μ ∙ η ∼ Id (M A).
Proof. cbv. rewrite (relmon_law2 M0). reflexivity. Qed.
Lemma rmon_id_law3 {A} : μ ∙ μ ∼ μ ∙ fmap M (rmon_id_mult A).
Proof.
cbv. rewrite -!relmon_law3 !cat_law3 (relmon_law2 M0) cat_law2 cat_law1.
reflexivity.
Qed.
End RMonadAsMonad.
(* transport a J1-relative monad into a J2-relative monad along a natural isomorphism *)
Section RelativeMonadIso.
Context {I C} {J1 J2 : functor I C} (M : relativeMonad J1)
(phi : natIso J1 J2).
Program Definition rmon_transp_natIso : relativeMonad J2 :=
mkRelativeMonad M (fun A ⇒ relmon_unit M A ∙ ni_inv phi A)
(fun A B f ⇒ relmon_bind M (f ∙ phi A))
_ _ _ _.
Next Obligation. cbv ; intuition ; rewrite H ; reflexivity. Qed.
Next Obligation.
rewrite -cat_law3 ni_leftinv cat_law2 relmon_law1 ; reflexivity.
Qed.
Next Obligation.
rewrite cat_law3 relmon_law2 -cat_law3 ni_rightinv cat_law2 ; reflexivity.
Qed.
Next Obligation.
rewrite -cat_law3 relmon_law3 ; reflexivity.
Qed.
(* Surprisingly, we never use naturality... *)
End RelativeMonadIso.
(* Given functors
J1 : I1 -> C1
J2 : I2 -> C2,
J1-relative monad M1 and
J2-relative monad M2
builds a J1×J2-relative monad I1 × I2 -> C1 × C2
*)
Section ProductRelativeMonad.
Context {I1 I2 C1 C2} {J1 : functor I1 C1} {J2 : functor I2 C2}
(M1 : relativeMonad J1) (M2 : relativeMonad J2).
Program Definition product_rmon : relativeMonad (prod_functor J1 J2) :=
mkRelativeMonad (fun A ⇒ ⟨M1 (nfst A), M2 (nsnd A)⟩)
(fun A ⇒ ⟨relmon_unit M1 (nfst A), relmon_unit M2 (nsnd A)⟩)
(fun _ _ f ⇒ ⟨relmon_bind M1 (nfst f), relmon_bind M2 (nsnd f)⟩) _ _ _ _.
Next Obligation.
cbv ; intuition ; [rewrite H0 | rewrite H1] ; reflexivity.
Qed.
Next Obligation. intuition; rewrite relmon_law1; reflexivity. Qed.
Next Obligation. intuition; rewrite relmon_law2; reflexivity. Qed.
Next Obligation. intuition; rewrite relmon_law3; reflexivity. Qed.
End ProductRelativeMonad.
(*********************************************************)
Precomposition is functorial on relative monads
Section RelativeMonadPrecomposition.
Context {I I'} (J : functor I I').
Section OnObjects.
Context {C : category} {JC : functor I' C} (J' := functor_comp J JC)
(M : relativeMonad JC).
Program Definition relativeMonad_precomposition
: relativeMonad J' :=
mkRelativeMonad (fun A ⇒ M (J A))
(fun A ⇒ relmon_unit M (J A))
(fun A B f ⇒ relmon_bind M f)
_ _ _ _.
Next Obligation. cbv ; intuition. rewrite H; reflexivity. Qed.
Next Obligation. rewrite relmon_law1 ; reflexivity. Qed.
Next Obligation. rewrite relmon_law2 ; reflexivity. Qed.
Next Obligation. rewrite relmon_law3 ; reflexivity. Qed.
End OnObjects.
Local Notation "J*" := relativeMonad_precomposition.
Section OnMorphism.
Context {C1 C2 : category} {JC1 : functor I' C1} {JC2 : functor I' C2}.
Context {M1 : relativeMonad JC1} {M2 : relativeMonad JC2}
{JC12 : functor C1 C2} (phi : natIso _ _)
(θ : relativeMonadMorphism JC12 phi M1 M2).
Program Definition relativeMonad_precomposition_morph
: relativeMonadMorphism JC12
(natIso_comp (natIso_whisker_left phi J)
(functor_assoc _ _ _))
(J× M1) (J× M2) :=
mkRelMonMorph _ _ _ _ (fun A ⇒ θ (J A)) _ _.
Next Obligation. rewrite rmm_law1 cat_law2 ; reflexivity. Qed.
Next Obligation. rewrite rmm_law2 cat_law1 ; reflexivity. Qed.
End OnMorphism.
(* TODO : show the functorial laws *)
End RelativeMonadPrecomposition.
(*********************************************************)
Context {I I'} (J : functor I I').
Section OnObjects.
Context {C : category} {JC : functor I' C} (J' := functor_comp J JC)
(M : relativeMonad JC).
Program Definition relativeMonad_precomposition
: relativeMonad J' :=
mkRelativeMonad (fun A ⇒ M (J A))
(fun A ⇒ relmon_unit M (J A))
(fun A B f ⇒ relmon_bind M f)
_ _ _ _.
Next Obligation. cbv ; intuition. rewrite H; reflexivity. Qed.
Next Obligation. rewrite relmon_law1 ; reflexivity. Qed.
Next Obligation. rewrite relmon_law2 ; reflexivity. Qed.
Next Obligation. rewrite relmon_law3 ; reflexivity. Qed.
End OnObjects.
Local Notation "J*" := relativeMonad_precomposition.
Section OnMorphism.
Context {C1 C2 : category} {JC1 : functor I' C1} {JC2 : functor I' C2}.
Context {M1 : relativeMonad JC1} {M2 : relativeMonad JC2}
{JC12 : functor C1 C2} (phi : natIso _ _)
(θ : relativeMonadMorphism JC12 phi M1 M2).
Program Definition relativeMonad_precomposition_morph
: relativeMonadMorphism JC12
(natIso_comp (natIso_whisker_left phi J)
(functor_assoc _ _ _))
(J× M1) (J× M2) :=
mkRelMonMorph _ _ _ _ (fun A ⇒ θ (J A)) _ _.
Next Obligation. rewrite rmm_law1 cat_law2 ; reflexivity. Qed.
Next Obligation. rewrite rmm_law2 cat_law1 ; reflexivity. Qed.
End OnMorphism.
(* TODO : show the functorial laws *)
End RelativeMonadPrecomposition.
(*********************************************************)
Postcomposition by a *full and faithful* functor is functorial on relative monads
Section FullyFaithfulFunctor.
Context {C D : category} (F : functor C D).
Record ff_struct :=
{ ff_invmap :> ∀ {X Y}, D⦅F X;F Y⦆ → C⦅X;Y⦆
; ff_inv_proper : ∀ {X Y}, Proper (sim D ==> sim C) (@ff_invmap X Y)
; ff_section : ∀ {X Y} (f : D⦅F X;F Y⦆), fmap F (ff_invmap f) ∼ f
; ff_retraction : ∀ {X Y} (f : C⦅X;Y⦆), ff_invmap (fmap F f) ∼ f
}.
Global Existing Instance ff_inv_proper.
Lemma invert_comp (Fff : ff_struct) {X Y Z}
(f:D⦅F Y;F Z⦆) (g:D⦅F X;F Y⦆): Fff _ _ (f ∙ g) ∼ Fff _ _ f ∙ Fff _ _ g.
Proof.
rewrite -{1}(ff_section Fff f) -{1}(ff_section Fff g) -functor_law2 ff_retraction ; reflexivity.
Qed.
End FullyFaithfulFunctor.
Section RelativeMonadPostcomposition.
Context {I C D} {J: functor I C} (M:relativeMonad J)
(F : functor C D) (Fff : ff_struct F).
Let FJ := functor_comp J F.
Program Definition relativeMonad_postcomposition : relativeMonad FJ :=
mkRelativeMonad (fun A ⇒ F (M A))
(fun A ⇒ fmap F (relmon_unit M A))
(fun A B f ⇒ fmap F (relmon_bind M (Fff _ _ f)))
_ _ _ _.
Next Obligation. cbv ; intuition ; rewrite H; reflexivity. Qed.
Next Obligation.
rewrite ff_retraction relmon_law1 functor_law1 ; reflexivity.
Qed.
Next Obligation.
rewrite -functor_law2 relmon_law2 ff_section ; reflexivity.
Qed.
Next Obligation.
rewrite invert_comp ff_retraction relmon_law3 functor_law2 ; reflexivity.
Qed.
End RelativeMonadPostcomposition.
(*********************************************************)
Right module on a relative monad
Section RightModule.
Context {I C D : category} {J : functor I C} {M : relativeMonad J}
{F0 : functor C D} (F := functor_comp J F0).
Cumulative Record rightModuleStructure :=
mkRightModule
{ rm_bind :> ∀ {X Y}, C⦅J X ; M Y⦆ → D⦅F X ; F Y⦆
; rm_bind_proper : ∀ {X Y}, Proper (sim C ==> sim D) (@rm_bind X Y)
; rm_law1 : ∀ {X}, rm_bind (relmon_unit M X) ∼ Id (F X)
; rm_law2 : ∀ {X Y Z} (f : C⦅J X ; M Y⦆) (g:C⦅J Y; M Z⦆),
rm_bind (relmon_bind M g ∙ f) ∼ rm_bind g ∙ rm_bind f
; rm_law3 : ∀ {X X' Y} (f : C⦅J X ; J X'⦆) (g : C⦅J X'; M Y⦆),
rm_bind (g ∙ f) ∼ rm_bind g ∙ fmap F0 f
}.
Global Existing Instance rm_bind_proper.
End RightModule.
Arguments rightModuleStructure {_ _ _ _} M F0.
(* When the relative monad is actually a monad
we recover the usual notion of right module *)
Section RightModuleId.
Context {C D : category} (J := functor_id C) {M : relativeMonad J}
{F0 : functor C D} (F := functor_comp J F0).
Context (rmF : rightModuleStructure M F0).
Lemma rm_law2_id {A B} (g : C⦅A ; M B⦆) :
rm_bind rmF (relmon_bind M g) ∼ rm_bind rmF g ∙ rm_bind rmF (Id (M A)).
Proof. rewrite -(cat_law2 _ _ _ (relmon_bind M g)) rm_law2 ; reflexivity. Qed.
Let FM := (functor_comp (rmon_to_functor M) F).
Program Definition right_module_nattrans : natTrans FM F :=
mkNatTrans FM F (fun A ⇒ rm_bind rmF (Id (M A))) _.
Next Obligation.
rewrite -(rm_law3 rmF) cat_law1 rm_law2_id rm_law3 rm_law1 cat_law1 ; reflexivity.
Qed.
Notation η := (@rmon_unit C C (functor_id C) _ _).
Notation μ := (rmon_id_mult M).
Notation α := (right_module_nattrans _).
Lemma right_module_law1 {A} : α ∙ fmap F η ∼ Id (F A).
Proof. cbv. rewrite -(rm_law3 rmF) cat_law1 rm_law1. reflexivity. Qed.
Lemma right_module_law2 {A} : α ∙ fmap F (μ A) ∼ α ∙ α.
Proof. cbv. rewrite -(rm_law3 rmF) cat_law1 rm_law2_id; reflexivity. Qed.
End RightModuleId.
(* Monad morphisms yield right modules, generalizing the codomain
to a relative monads *)
Section RelativeMonadMorphismToRightModule.
Context {C D:category} {M0 : relativeMonad (functor_id C)}
{J:functor C D} (W0 : relativeMonad J) {phi}
(θ : relativeMonadMorphism J phi M0 W0).
Let W := rmon_to_functor W0.
Program Definition rmon_morph_right_module : rightModuleStructure M0 W :=
mkRightModule (fun _ _ f ⇒ relmon_bind W0 (θ _ ∙ fmap J f∙ phi _)) _ _ _ _.
Next Obligation. cbv ; intuition ; rewrite H; reflexivity. Qed.
Next Obligation.
rewrite (rmm_law1 _ _ _ _ θ) ; cbv .
rewrite -cat_law3 (ni_leftinv _ _ phi) -(functor_law1 _ _ J _).
move: (functor_law1 _ _ W X) ⇒ /= → ; reflexivity.
Qed.
Next Obligation.
rewrite functor_law2 cat_law3 (rmm_law2 _ _ _ _ θ) ; cbv.
rewrite -!cat_law3 relmon_law3 ; reflexivity.
Qed.
Next Obligation.
rewrite -relmon_law3 functor_law2 !cat_law3 relmon_law2.
rewrite -cat_law3 -(ni_natural _ _ phi) cat_law3 ; reflexivity.
Qed.
End RelativeMonadMorphismToRightModule.
(* Taking phi = natIso_id _ would make the following go through *)
(* Another solution is to ask that J is full and faithful *)
(* Section RelativeMonadMorphismToRightModule. *)
(* Context {I C D:category} {J:functor I C} {M0 : relativeMonad J} *)
(* {J':functor C D} (W0 : relativeMonad J') *)
(* phi *)
(* (W1 := relativeMonad_precomposition J W0) *)
(* (θ : relativeMonadMorphism J' phi M0 W1). *)
(* Let W := rmon_to_functor W0. *)
(* Program Definition rmon_morph_right_module : rightModuleStructure M0 W := *)
(* mkRightModule (fun _ _ f => relmon_bind W0 (θ _ ∙ fmap J' f∙ phi _)) _ _ _ _. *)
(* Next Obligation. cbv ; intuition ; rewrite H; reflexivity. Qed. *)
(* Next Obligation. *)
(* rewrite (rmm_law1 _ _ _ _ θ) ; cbv . *)
(* rewrite -cat_law3 (ni_leftinv _ _ phi) -(functor_law1 _ _ J' _). *)
(* move: (functor_law1 _ _ W (J X)) => /= -> ; reflexivity. *)
(* Qed. *)
(* Next Obligation. *)
(* rewrite functor_law2 cat_law3 (rmm_law2 _ _ _ _ θ) ; cbv. *)
(* rewrite -!cat_law3 relmon_law3 ; reflexivity. *)
(* Qed. *)
(* Next Obligation. *)
(* rewrite -relmon_law3 functor_law2 !cat_law3 relmon_law2. ; reflexivity. *)
(* Qed. *)
(* End RelativeMonadMorphismToRightModule. *)
Section RightModuleHomomorphism.
Context {I C D : category}
{J : functor I C} {M : relativeMonad J}
{F G : functor C D}
(rmF : rightModuleStructure M F) (rmG : rightModuleStructure M G)
(σ : natTrans F G).
(* Notation αF := (right_module_nattrans rmF _). *)
(* Notation αG := (right_module_nattrans rmG _). *)
Class rightModuleHomomorphism : Prop :=
rm_homo : ∀ {A B} (f:C⦅J A; M B⦆),
σ _ ∙ rm_bind rmF f ∼ rm_bind rmG f ∙ σ _.
(* Class rightModuleHomomorphism : Prop := rm_homo : forall {A}, σ A ∙ αF ∼ αG ∙ σ _. *)
End RightModuleHomomorphism.
Section RightModulePostcomposition.
Context {I C D1 D2 : category}
{J : functor I C} (M : relativeMonad J)
(F : functor C D1) (G : functor D1 D2)
(rmF : rightModuleStructure M F).
Let GF := functor_comp F G.
Program Definition rightModule_postcomp : rightModuleStructure M GF :=
mkRightModule (fun _ _ f ⇒ fmap G (rm_bind rmF f)) _ _ _ _.
Next Obligation. cbv ; intuition ; rewrite H ; reflexivity. Qed.
Next Obligation. rewrite rm_law1 functor_law1 ; reflexivity. Qed.
Next Obligation. rewrite rm_law2 functor_law2 ; reflexivity. Qed.
Next Obligation. rewrite rm_law3 functor_law2 ; reflexivity. Qed.
End RightModulePostcomposition.
Section FreeRightModule.
Context {C D : category} {M : relativeMonad (functor_id C)} (J : functor C D).
Let JM := functor_comp (rmon_to_functor M) J.
Program Definition free_right_module : rightModuleStructure M JM :=
mkRightModule (fun _ _ f ⇒ fmap J (relmon_bind M f)) _ _ _ _.
Next Obligation. cbv ; intuition. rewrite H. reflexivity. Qed.
Next Obligation. rewrite relmon_law1 functor_law1 ; reflexivity. Qed.
Next Obligation. rewrite relmon_law3 functor_law2 ; reflexivity. Qed.
Next Obligation.
rewrite -functor_law2 -relmon_law3 cat_law3 (relmon_law2 M) ; reflexivity.
Qed.
Context {F : functor C D} (rmF : rightModuleStructure M F).
Notation "F ▷ ν" := (natTrans_whisker_left ν F) (at level 65).
Notation "ν ◁ F" := (natTrans_whisker_right F ν) (at level 65).
Notation "ν ⋅ θ" := (natTrans_comp ν θ) (at level 70).
Section PointToHomomorphism.
Context (η : natTrans J F).
Definition point_to_homomorphism : natTrans JM F :=
rmon_to_functor M ▷ (η ⋅ iso_to_natTrans_inv (functor_unit_left _))
⋅ right_module_nattrans rmF
⋅ iso_to_natTrans (functor_unit_left _).
(* natTrans_comp (natTrans_whisker_left η (rmon_to_functor M)) *)
(* (). *)
Global Instance : rightModuleHomomorphism free_right_module rmF point_to_homomorphism.
Proof.
move⇒ ? ? ? /= ; rewrite !cat_law1 -cat_law3 nt_natural !cat_law3 -(rm_law2 rmF).
rewrite -(rm_law3 rmF) cat_law1 cat_law2 ; reflexivity.
Qed.
End PointToHomomorphism.
Section HomomorphismToPoint.
Context (σ : natTrans JM F) `{!rightModuleHomomorphism free_right_module rmF σ}.
Definition homomorphism_to_point : natTrans J F :=
natTrans_comp (iso_to_natTrans_inv (functor_unit_left _)) (natTrans_comp (natTrans_whisker_right J (rmon_unit M)) σ).
End HomomorphismToPoint.
Lemma point_to_homomorphism_to_point η A :
homomorphism_to_point (point_to_homomorphism η) A ∼ η A.
Proof.
cbv.
rewrite !cat_law1 cat_law2 -cat_law3 nt_natural cat_law3
-(rm_law3 rmF) cat_law1 rm_law1 cat_law1; reflexivity. Qed.
Lemma homo_to_point_to_homo σ
`{H:!rightModuleHomomorphism free_right_module rmF σ} A :
point_to_homomorphism (homomorphism_to_point σ) A ∼ σ A.
Proof.
cbv.
rewrite !cat_law3 cat_law1 !cat_law2.
move: (@rm_homo _ _ _ _ _ _ _ _ _ σ H _ _ (Id (M A)))=> /= <-.
rewrite -!cat_law3 -functor_law2 (relmon_law2 M).
rewrite functor_law1 cat_law2 ; reflexivity.
Qed.
End FreeRightModule.
Arguments free_right_module {_ _} _ _.
Context {I C D : category} {J : functor I C} {M : relativeMonad J}
{F0 : functor C D} (F := functor_comp J F0).
Cumulative Record rightModuleStructure :=
mkRightModule
{ rm_bind :> ∀ {X Y}, C⦅J X ; M Y⦆ → D⦅F X ; F Y⦆
; rm_bind_proper : ∀ {X Y}, Proper (sim C ==> sim D) (@rm_bind X Y)
; rm_law1 : ∀ {X}, rm_bind (relmon_unit M X) ∼ Id (F X)
; rm_law2 : ∀ {X Y Z} (f : C⦅J X ; M Y⦆) (g:C⦅J Y; M Z⦆),
rm_bind (relmon_bind M g ∙ f) ∼ rm_bind g ∙ rm_bind f
; rm_law3 : ∀ {X X' Y} (f : C⦅J X ; J X'⦆) (g : C⦅J X'; M Y⦆),
rm_bind (g ∙ f) ∼ rm_bind g ∙ fmap F0 f
}.
Global Existing Instance rm_bind_proper.
End RightModule.
Arguments rightModuleStructure {_ _ _ _} M F0.
(* When the relative monad is actually a monad
we recover the usual notion of right module *)
Section RightModuleId.
Context {C D : category} (J := functor_id C) {M : relativeMonad J}
{F0 : functor C D} (F := functor_comp J F0).
Context (rmF : rightModuleStructure M F0).
Lemma rm_law2_id {A B} (g : C⦅A ; M B⦆) :
rm_bind rmF (relmon_bind M g) ∼ rm_bind rmF g ∙ rm_bind rmF (Id (M A)).
Proof. rewrite -(cat_law2 _ _ _ (relmon_bind M g)) rm_law2 ; reflexivity. Qed.
Let FM := (functor_comp (rmon_to_functor M) F).
Program Definition right_module_nattrans : natTrans FM F :=
mkNatTrans FM F (fun A ⇒ rm_bind rmF (Id (M A))) _.
Next Obligation.
rewrite -(rm_law3 rmF) cat_law1 rm_law2_id rm_law3 rm_law1 cat_law1 ; reflexivity.
Qed.
Notation η := (@rmon_unit C C (functor_id C) _ _).
Notation μ := (rmon_id_mult M).
Notation α := (right_module_nattrans _).
Lemma right_module_law1 {A} : α ∙ fmap F η ∼ Id (F A).
Proof. cbv. rewrite -(rm_law3 rmF) cat_law1 rm_law1. reflexivity. Qed.
Lemma right_module_law2 {A} : α ∙ fmap F (μ A) ∼ α ∙ α.
Proof. cbv. rewrite -(rm_law3 rmF) cat_law1 rm_law2_id; reflexivity. Qed.
End RightModuleId.
(* Monad morphisms yield right modules, generalizing the codomain
to a relative monads *)
Section RelativeMonadMorphismToRightModule.
Context {C D:category} {M0 : relativeMonad (functor_id C)}
{J:functor C D} (W0 : relativeMonad J) {phi}
(θ : relativeMonadMorphism J phi M0 W0).
Let W := rmon_to_functor W0.
Program Definition rmon_morph_right_module : rightModuleStructure M0 W :=
mkRightModule (fun _ _ f ⇒ relmon_bind W0 (θ _ ∙ fmap J f∙ phi _)) _ _ _ _.
Next Obligation. cbv ; intuition ; rewrite H; reflexivity. Qed.
Next Obligation.
rewrite (rmm_law1 _ _ _ _ θ) ; cbv .
rewrite -cat_law3 (ni_leftinv _ _ phi) -(functor_law1 _ _ J _).
move: (functor_law1 _ _ W X) ⇒ /= → ; reflexivity.
Qed.
Next Obligation.
rewrite functor_law2 cat_law3 (rmm_law2 _ _ _ _ θ) ; cbv.
rewrite -!cat_law3 relmon_law3 ; reflexivity.
Qed.
Next Obligation.
rewrite -relmon_law3 functor_law2 !cat_law3 relmon_law2.
rewrite -cat_law3 -(ni_natural _ _ phi) cat_law3 ; reflexivity.
Qed.
End RelativeMonadMorphismToRightModule.
(* Taking phi = natIso_id _ would make the following go through *)
(* Another solution is to ask that J is full and faithful *)
(* Section RelativeMonadMorphismToRightModule. *)
(* Context {I C D:category} {J:functor I C} {M0 : relativeMonad J} *)
(* {J':functor C D} (W0 : relativeMonad J') *)
(* phi *)
(* (W1 := relativeMonad_precomposition J W0) *)
(* (θ : relativeMonadMorphism J' phi M0 W1). *)
(* Let W := rmon_to_functor W0. *)
(* Program Definition rmon_morph_right_module : rightModuleStructure M0 W := *)
(* mkRightModule (fun _ _ f => relmon_bind W0 (θ _ ∙ fmap J' f∙ phi _)) _ _ _ _. *)
(* Next Obligation. cbv ; intuition ; rewrite H; reflexivity. Qed. *)
(* Next Obligation. *)
(* rewrite (rmm_law1 _ _ _ _ θ) ; cbv . *)
(* rewrite -cat_law3 (ni_leftinv _ _ phi) -(functor_law1 _ _ J' _). *)
(* move: (functor_law1 _ _ W (J X)) => /= -> ; reflexivity. *)
(* Qed. *)
(* Next Obligation. *)
(* rewrite functor_law2 cat_law3 (rmm_law2 _ _ _ _ θ) ; cbv. *)
(* rewrite -!cat_law3 relmon_law3 ; reflexivity. *)
(* Qed. *)
(* Next Obligation. *)
(* rewrite -relmon_law3 functor_law2 !cat_law3 relmon_law2. ; reflexivity. *)
(* Qed. *)
(* End RelativeMonadMorphismToRightModule. *)
Section RightModuleHomomorphism.
Context {I C D : category}
{J : functor I C} {M : relativeMonad J}
{F G : functor C D}
(rmF : rightModuleStructure M F) (rmG : rightModuleStructure M G)
(σ : natTrans F G).
(* Notation αF := (right_module_nattrans rmF _). *)
(* Notation αG := (right_module_nattrans rmG _). *)
Class rightModuleHomomorphism : Prop :=
rm_homo : ∀ {A B} (f:C⦅J A; M B⦆),
σ _ ∙ rm_bind rmF f ∼ rm_bind rmG f ∙ σ _.
(* Class rightModuleHomomorphism : Prop := rm_homo : forall {A}, σ A ∙ αF ∼ αG ∙ σ _. *)
End RightModuleHomomorphism.
Section RightModulePostcomposition.
Context {I C D1 D2 : category}
{J : functor I C} (M : relativeMonad J)
(F : functor C D1) (G : functor D1 D2)
(rmF : rightModuleStructure M F).
Let GF := functor_comp F G.
Program Definition rightModule_postcomp : rightModuleStructure M GF :=
mkRightModule (fun _ _ f ⇒ fmap G (rm_bind rmF f)) _ _ _ _.
Next Obligation. cbv ; intuition ; rewrite H ; reflexivity. Qed.
Next Obligation. rewrite rm_law1 functor_law1 ; reflexivity. Qed.
Next Obligation. rewrite rm_law2 functor_law2 ; reflexivity. Qed.
Next Obligation. rewrite rm_law3 functor_law2 ; reflexivity. Qed.
End RightModulePostcomposition.
Section FreeRightModule.
Context {C D : category} {M : relativeMonad (functor_id C)} (J : functor C D).
Let JM := functor_comp (rmon_to_functor M) J.
Program Definition free_right_module : rightModuleStructure M JM :=
mkRightModule (fun _ _ f ⇒ fmap J (relmon_bind M f)) _ _ _ _.
Next Obligation. cbv ; intuition. rewrite H. reflexivity. Qed.
Next Obligation. rewrite relmon_law1 functor_law1 ; reflexivity. Qed.
Next Obligation. rewrite relmon_law3 functor_law2 ; reflexivity. Qed.
Next Obligation.
rewrite -functor_law2 -relmon_law3 cat_law3 (relmon_law2 M) ; reflexivity.
Qed.
Context {F : functor C D} (rmF : rightModuleStructure M F).
Notation "F ▷ ν" := (natTrans_whisker_left ν F) (at level 65).
Notation "ν ◁ F" := (natTrans_whisker_right F ν) (at level 65).
Notation "ν ⋅ θ" := (natTrans_comp ν θ) (at level 70).
Section PointToHomomorphism.
Context (η : natTrans J F).
Definition point_to_homomorphism : natTrans JM F :=
rmon_to_functor M ▷ (η ⋅ iso_to_natTrans_inv (functor_unit_left _))
⋅ right_module_nattrans rmF
⋅ iso_to_natTrans (functor_unit_left _).
(* natTrans_comp (natTrans_whisker_left η (rmon_to_functor M)) *)
(* (). *)
Global Instance : rightModuleHomomorphism free_right_module rmF point_to_homomorphism.
Proof.
move⇒ ? ? ? /= ; rewrite !cat_law1 -cat_law3 nt_natural !cat_law3 -(rm_law2 rmF).
rewrite -(rm_law3 rmF) cat_law1 cat_law2 ; reflexivity.
Qed.
End PointToHomomorphism.
Section HomomorphismToPoint.
Context (σ : natTrans JM F) `{!rightModuleHomomorphism free_right_module rmF σ}.
Definition homomorphism_to_point : natTrans J F :=
natTrans_comp (iso_to_natTrans_inv (functor_unit_left _)) (natTrans_comp (natTrans_whisker_right J (rmon_unit M)) σ).
End HomomorphismToPoint.
Lemma point_to_homomorphism_to_point η A :
homomorphism_to_point (point_to_homomorphism η) A ∼ η A.
Proof.
cbv.
rewrite !cat_law1 cat_law2 -cat_law3 nt_natural cat_law3
-(rm_law3 rmF) cat_law1 rm_law1 cat_law1; reflexivity. Qed.
Lemma homo_to_point_to_homo σ
`{H:!rightModuleHomomorphism free_right_module rmF σ} A :
point_to_homomorphism (homomorphism_to_point σ) A ∼ σ A.
Proof.
cbv.
rewrite !cat_law3 cat_law1 !cat_law2.
move: (@rm_homo _ _ _ _ _ _ _ _ _ σ H _ _ (Id (M A)))=> /= <-.
rewrite -!cat_law3 -functor_law2 (relmon_law2 M).
rewrite functor_law1 cat_law2 ; reflexivity.
Qed.
End FreeRightModule.
Arguments free_right_module {_ _} _ _.