********************************************************** Contents:
• in particular: the distributive law for the maybe monad and any monad deriv_dist
• left module over a monad T obtained by composing a monad having a distributive law with T LModule_comp_laws
• in particular: the derivative of a left module over a monad LModule_deriv
• Commutation of module derivation with pullback pb_LModule_deriv_iso
Written by: Joseph Helfer (May 2017)

cf. Beck "Distributive laws" (1969)
Section comp_def.

Section DistrLaws.
Context {C : precategory_data} {S T : Monad_data C}.

distributivity law for a pair of monads
Definition monad_dist_laws (a : T S S T) :=
((( x : C, η S (T x) · a x = #T (η S x)) ×
( x : C, #S (η T x) · a x = η T (S x))) ×
( x : C, a (T x) · #T (a x) · μ T (S x) = #S (μ T x) · a x)) ×
( x : C, #S (a x) · a (S x) · #T (μ S x) = μ S (T x) · a x).

Definition monad_dist_law1 {a : T S S T} (l : monad_dist_laws a) := (pr1 (pr1 (pr1 l))).
Definition monad_dist_law2 {a : T S S T} (l : monad_dist_laws a) := (pr2 (pr1 (pr1 l))).
Definition monad_dist_law3 {a : T S S T} (l : monad_dist_laws a) := (pr2 (pr1 l)).
Definition monad_dist_law4 {a : T S S T} (l : monad_dist_laws a) := pr2 l.

End DistrLaws.

composition of monads with a distributive law
Definition monad_comp_mu {C : precategory} {S T : Monad_data C} (a : T S S T) :
(S T S T) (S T) :=
nat_trans_comp _ _ _ (post_whisker (pre_whisker S a) T)
(nat_trans_comp _ _ _ (pre_whisker (S S) (μ T)) (post_whisker (μ S) T)).

Definition monad_comp_eta {C : precategory} {S T : Monad_data C} (a : T S S T):
functor_identity C S T :=
nat_trans_comp _ _ _ (η S) (pre_whisker S (η T)).

Definition monad_comp_data {C : precategory} {S T : Monad_data C} (a : T S S T) :

Below are the proofs of the monad laws for the composition of monads. We prove them as separate lemmas not only because they are somewhat lengthy, but also for the following reason: the μ and η for this monad are defined via operations on natural transformations, rather than their value being given explicitly at each object. However, for the proofs, it is desirable to have these explicit expressions; the easiest way to accomplish this is to write out the statements by hand in the desired form (as ugly as they may be).
This is also done for the same reason later in the file, where the proofs of the individual lemmas are not as lengthy.
Here is the diagram corresponding to this proof. The outside of the diagram represents the equation to be proved. The numbers indicate the order in which the sub-diagrams are used. TSTSx ---------------> TTSSx -----------> TSSx ------------> TSx ^ T (a (Sx)) ^ μ T (SSx) ^ T (μ S x) ^ | | / / |η T (STSx) |η T (TSSx) /id / | 1 | 3 / / a (Sx) / / STSx --------------> TSSx ------------ 4 / ^ ^ / | 2 /T (η S (Sx)) / |η S (TSx) / / | _________________/ / |/ id / TSx ------------------------------------------------

Context {C : precategory} {S T : Monad C}.
Local Lemma monad_comp_law1 {a : T S S T} (l : monad_dist_laws a) : x : C,
(η S (T (S x))) · (η T (S (T (S x)))) · (#T (a (S x)) · (μ T (S (S x)) · #T (μ S x))) =
identity (T (S x)).
Proof.
intro x.
rewrite <- assoc.
rewrite !(assoc ((η T) (S (T (S x))))).
rewrite <- (nat_trans_ax (η T) (S (T (S x)))).
simpl.
rewrite !assoc.
etrans.
{ do 3 apply cancel_postcomposition.
}

rewrite <- (assoc (# T ((η S) (S x)))).
etrans.
{ apply cancel_postcomposition.
apply cancel_precomposition.
}

rewrite id_right.
rewrite <- functor_comp.
rewrite <- functor_id.
now etrans;
try apply maponpaths;
Defined.

The diagram for this proof (see above for explanation): TSTSx ---------------> TTSSx -----------> TSSx ------------> TSx ^ T (a (Sx)) ^ μ T (SSx) ^ T (μ S x) ^ | 1 / 2 / / |T S (η T (Sx)) / /id / | /T (η T (SSx)) / / | _______________/ / / | / / / TSSx -------------------------------- 3 / ^ / | / |T S (η S x) / | id / TSx ------------------------------------------------
Local Lemma monad_comp_law2 {a : T S S T} (l : monad_dist_laws a) : x : C,
#T (#S ((η S x) · (η T (S x)))) · (#T (a (S x)) · (μ T (S (S x)) · #T (μ S x))) =
identity (T (S x)).
Proof.
intro x.
rewrite !assoc.
rewrite <- functor_comp.
rewrite (functor_comp S).
rewrite <- !assoc.
etrans.
{ apply cancel_postcomposition.
apply maponpaths.
apply cancel_precomposition.
}

rewrite functor_comp.
rewrite <- assoc.
rewrite (assoc (# T ((η T) (S (S x))))).
rewrite id_left.
rewrite <- functor_comp.
rewrite <- functor_id.
now etrans;
try apply maponpaths;
Defined.

Here, more enlightening than a diagram is just the "strategy" of the proof: each side of the equation consists of some applications of the monad multiplications μ T and μ S and the distributive law 'a'. The strategy is - (1) using repeated applications of the third and fourth axioms for the distributive law and the naturality of μ T, μ S, and 'a' - to arrange for all the applications of 'a' to come first, and then the applications μ T and μ S. Thus, both sides are transformed to a composite TSTSTSx --> TTTSSSx -> TSx; then (2) the first composands are equal by the naturality of 'a', and the second composands are equal by the naturality and associativity of μ T and μ S.
Local Lemma monad_comp_law3 {a : T S S T} (l : monad_dist_laws a) : x : C,
#T (#S (#T (a (S x)) · (μ T (S (S x)) · #T (μ S x)))) ·
(#T (a (S x)) · (μ T (S (S x)) · #T (μ S x))) =
#T (a (S (T (S x)))) · (μ T (S (S (T (S x)))) · #T (μ S (T (S x)))) ·
(#T (a (S x)) · (μ T (S (S x)) · #T (μ S x))).
Proof.
intro x.
rewrite assoc.
rewrite <- functor_comp.
rewrite <- nat_trans_ax.
do 2 rewrite (functor_comp S).
rewrite (assoc _ _ (#S ((μ T) (S x)))).
rewrite <- (assoc _ (#S ((μ T) (S x))) _).
rewrite <- assoc.
rewrite <- (assoc (a (T (S x)))).
rewrite (assoc _ (a (T (S x)))).
simpl.
etrans.
{ apply cancel_postcomposition.
apply maponpaths.
apply cancel_precomposition.
apply cancel_postcomposition.
apply (nat_trans_ax a).
}
rewrite <- assoc.
rewrite (assoc _ (# T (a (S x)))).
etrans.
{ apply cancel_postcomposition.
apply maponpaths.
do 2 apply cancel_precomposition.
apply cancel_postcomposition.
apply (! (functor_comp T _ _)).
}
etrans.
{ apply cancel_postcomposition.
apply maponpaths.
do 2 apply cancel_precomposition.
apply cancel_postcomposition.
apply maponpaths.
apply (nat_trans_ax a).
}
rewrite <- assoc.
rewrite <- (assoc _ (# T ((μ S) (T (S x))))).
rewrite (assoc (# T ((μ S) (T (S x))))).
rewrite <- functor_comp.
rewrite (assoc ((μ T) (S (S (T (S x)))))).
rewrite <- (nat_trans_ax (μ T)).
rewrite !functor_comp.
rewrite !assoc.
rewrite <- functor_comp.
etrans.
{ do 5 apply cancel_postcomposition.
apply maponpaths.
apply (nat_trans_ax a).
}
do 2 rewrite <- assoc.
rewrite (assoc (# T ((μ T) (S (S x))))).
rewrite <- !(functor_comp T ((μ T) (S (S x)))).
rewrite <- (nat_trans_ax (μ T)).
rewrite !functor_comp.
rewrite !assoc.
simpl.
rewrite <- (assoc _ (# T (# T (# T (# S ((μ S) x)))))).
rewrite <- !functor_comp.
rewrite !functor_comp.
rewrite !assoc.
rewrite <- (assoc _ (# T ((μ T) (S x)))).
apply pathsinv0.
rewrite <- (assoc _ ((μ T) (T (S (S x))))).
rewrite <- nat_trans_ax.
now rewrite !assoc.
Defined.

morphism from the factor T to the composite S ∙ T of two monads
Definition monad_to_comp_data {a : T S S T} (l : monad_dist_laws a) :
T monad_comp l := post_whisker (η S) T.

We prove the monad morphism laws as separate lemmas for the reason explained in the comment near the beginning of the file
The diagram for this proof (see above for explanation): TTx------------------------------------------------------------------->Tx | \ μ T x | | ¯¯¯¯¯¯¯¯¯¯¯¯¯\ | |T (η S (Tx)) \T (T (η S x) 5 T (η S x)| | 2 \ | v T (a x) v id μ T (Sx) | TSTx----------------TTSx------------------TTSx--------------------- | | | ^ \ | |T S T (η S x) |T T S (η S x) / \ | | | _____________/ T T (μ S x) 3 \ | | 1 | 4 / \ | v v / v v TSTSx-------------->TTSSx-------------------------->TSSx-------------->TSx T (a (Sx)) μ T (SSx) T (μ S x)
Local Lemma monad_to_comp_law1 {a : T S S T} (l : monad_dist_laws a) :
x : C,
μ T x · #T (η S x) =
#T (η S (T x)) · #T (#S (#T (η S x))) ·
(#T (a (S x)) · (μ T (S (S x)) · #T (μ S x))).
Proof.
intro x.
rewrite <- assoc.
rewrite (assoc (# T (# S (# T ((η S) x))))).
rewrite <- functor_comp.
apply pathsinv0.
etrans.
{ apply cancel_precomposition.
apply cancel_postcomposition.
apply maponpaths.
apply (nat_trans_ax a).
}

rewrite functor_comp.
rewrite !assoc.
rewrite <- functor_comp.
rewrite <- !assoc.
rewrite <- (nat_trans_ax (μ T) (S (S x))).
rewrite (assoc (# T (# T (# S ((η S) x))))).
simpl.
rewrite <- !functor_comp.
etrans.
{ apply cancel_precomposition.
apply cancel_postcomposition.
do 2 apply maponpaths.
}

rewrite !functor_id.
rewrite id_left.
now rewrite <- (nat_trans_ax (μ T) x).
Defined.

Local Definition monad_to_comp_law2 {a : T S S T} (l : monad_dist_laws a) :
x : C, η T x · #T (η S x) = η S x · (η T (S x)).
Proof.
intro x.
now rewrite <- (nat_trans_ax (η T) x ).
Defined.

Definition monad_to_comp {a : T S S T} (l : monad_dist_laws a) :

End comp_def.

# Definition of the "Maybe" monad (coproduct with a fixed object)

Section maybe_def.

Context {C : precategory} (o : C) (co : BinCoproducts C).

Definition maybe_functor : functor C C :=
constcoprod_functor1 co o.
maybe_functor is the same as UniMath.SubstitutionSystems.SignatureExamples.genopt, which is introduced there only by Let, and a different notion of distributive law is studied
We prove the monad laws as separate lemmas for the reason explained in the comment near the beginning of the file

Local Lemma maybe_monad_law1 : c : C,
BinCoproductIn2 C (co o (co o c)) ·
BinCoproductArrow C _ (BinCoproductIn1 C (co o c)) (identity (co o c)) =
identity (co o c).
Proof.
intro c.
now rewrite BinCoproductIn2Commutes.
Defined.

Local Lemma maybe_monad_law2 : c : C,
BinCoproductOfArrows C (co o c) (co o (co o c))
(identity o) (BinCoproductIn2 C (co o c)) ·
BinCoproductArrow C _ (BinCoproductIn1 C (co o c)) (identity (co o c)) =
identity (co o c).
Proof.
intro c.
now rewrite precompWithBinCoproductArrow, id_left,
<- (id_right (BinCoproductIn1 C (co o c))), <- BinCoproductArrowEta.
Defined.

Local Lemma maybe_monad_law3 : c : C,
BinCoproductOfArrows C (co o (co o (co o c))) (co o (co o c))
(identity o)
(BinCoproductArrow C (co o (co o c)) (BinCoproductIn1 C (co o c)) (identity (co o c))) ·
BinCoproductArrow C _ (BinCoproductIn1 C (co o c)) (identity (co o c)) =
BinCoproductArrow C _ (BinCoproductIn1 C (co o (co o c))) (identity (co o (co o c))) ·
BinCoproductArrow C _ (BinCoproductIn1 C (co o c)) (identity (co o c)).
Proof.
intro c.
now rewrite precompWithBinCoproductArrow, postcompWithBinCoproductArrow,
!id_right, postcompWithBinCoproductArrow,
!id_left, BinCoproductIn1Commutes.
Defined.

Definition of the derivative of a monad, i.e. precomposing with the maybe monad
Section deriv_def.

Definition functor_deriv {D : precategory}
(T : functor C D) : functor C D := maybe_monad T.

The distributive law for any monad with the Maybe monad. This is the obvious map (TX + Y) -> T (X + Y) - i.e., T(in1) on the first component and (in2 · η T) on the second component
We prove the distributive law axioms as separate lemmas for the reason explained in the comment near the beginning of the file

Local Lemma deriv_dist_law1 (T : Monad C) : x : C,
BinCoproductIn2 C (co o (T x)) ·
BinCoproductArrow C _ (BinCoproductIn1 C _ · η T _) (#T (BinCoproductIn2 C _)) =
#T (BinCoproductIn2 C (co o x)).
Proof.
intro x.
now rewrite BinCoproductIn2Commutes.
Defined.

Local Lemma deriv_dist_law2 (T : Monad C) : x : C,
BinCoproductOfArrows C (co o x) (co o (T x)) (identity o) (η T x) ·
BinCoproductArrow C _ (BinCoproductIn1 C _ · η T (co o x)) (#T (BinCoproductIn2 C _)) =
η T (co o x).
Proof.
intro x.
rewrite precompWithBinCoproductArrow.
rewrite id_left.
etrans.
{ apply maponpaths.
apply (!(nat_trans_ax (η T) _ _ _)).
}
now rewrite <- BinCoproductArrowEta.
Defined.

Local Lemma deriv_dist_law3 (T : Monad C) : x : C,
BinCoproductArrow C _ (BinCoproductIn1 C _ · η T (co o (T x))) (#T (BinCoproductIn2 C _)) ·
#T (BinCoproductArrow C _ (BinCoproductIn1 C _ · η T (co o x)) (#T (BinCoproductIn2 C _))) ·
μ T (co o x) =
BinCoproductOfArrows C (co o (T (T x))) (co o (T x)) (identity o) (μ T x) ·
BinCoproductArrow C _ (BinCoproductIn1 C _ · η T (co o x)) (#T (BinCoproductIn2 C _)).
Proof.
intro x.
do 2 rewrite postcompWithBinCoproductArrow.
rewrite <- functor_comp.
rewrite BinCoproductIn2Commutes.
rewrite <- (assoc (BinCoproductIn1 C (co o (T x)))).
rewrite <- (nat_trans_ax (η T) (co o (T x))).
rewrite (assoc (BinCoproductIn1 C (co o (T x)))).
rewrite <- (assoc _ ((η T) (T (co o x)))).
simpl.
rewrite BinCoproductIn1Commutes.
rewrite precompWithBinCoproductArrow.
rewrite id_left.
rewrite id_right.
now rewrite <- (nat_trans_ax (μ T) x).
Defined.

Local Lemma deriv_dist_law4 (T : Monad C) : x : C,
BinCoproductOfArrows C (co o (co o (T x))) (co o (T (co o x))) (identity o)
(BinCoproductArrow C _ (BinCoproductIn1 C _ · η T (co o x))
(#T (BinCoproductIn2 C _))) ·
BinCoproductArrow C _ (BinCoproductIn1 C _ · η T (co o (co o x))) (#T (BinCoproductIn2 C _)) ·
#T (BinCoproductArrow C _ (BinCoproductIn1 C _) (identity _)) =
BinCoproductArrow C (co o (co o (T x))) (BinCoproductIn1 C _) (identity (co o (T x))) ·
BinCoproductArrow C (co o (T x)) (BinCoproductIn1 C (co o x) · η T (co o x))
(#T (BinCoproductIn2 C _)).
Proof.
intro x.
rewrite precompWithBinCoproductArrow.
rewrite postcompWithBinCoproductArrow.
rewrite <- (assoc _ (# T (BinCoproductIn2 C (co o (co o x))))).
rewrite <- functor_comp.
rewrite BinCoproductIn2Commutes.
rewrite functor_id.
rewrite id_right.
rewrite id_left.
rewrite <- assoc.
rewrite <- (nat_trans_ax (η T) (co o (co o x))).
simpl.
rewrite assoc.
rewrite BinCoproductIn1Commutes.
rewrite postcompWithBinCoproductArrow.
rewrite id_left.
now rewrite BinCoproductIn1Commutes.
Defined.

make_dirprod (make_dirprod (make_dirprod (deriv_dist_law1 T) (deriv_dist_law2 T))
(deriv_dist_law3 T))
(deriv_dist_law4 T).

the morphism from a monad to its derivative
derivative of a left module over a monad
Lemma LModule_comp_law1 {D : precategory} {T : Monad C} {S : Monad C}
{a : T S S T} (l : monad_dist_laws a) (L : LModule T D) : x : C,
#L (#S (η T x)) · (#L (a x) · lm_mult T L (S x)) = identity (L (S x)).
Proof.
intro x.
now rewrite assoc, <- functor_comp, (monad_dist_law2 l), (LModule_law1 T (S x)).
Defined.

Lemma LModule_comp_law2 {D : precategory} {T : Monad C} {S : Monad C}
{a : T S S T} (l : monad_dist_laws a) (L : LModule T D) : x : C,
#L (#S (μ T x)) · (#L (a x) · lm_mult T L (S x)) =
(#L (a (T x)) · lm_mult T L (S (T x))) · (#L (a x) · lm_mult T L (S x)).
Proof.
intro x.
rewrite assoc.
rewrite <- functor_comp.
rewrite !functor_comp.
rewrite <- assoc.
rewrite (LModule_law2 T (S x)).
rewrite assoc.
rewrite <- (assoc _ (#L (#T (a x)))).
etrans.
{ apply cancel_postcomposition.
apply cancel_precomposition.
apply (nat_trans_ax (lm_mult T L)).
}
now rewrite !assoc.
Defined.

Definition LModule_comp_data {D : precategory} {T : Monad C} {S : Monad C} (a : T S S T)
(L : LModule T D) : LModule_data T D :=
(S L,, nat_trans_comp _ _ _ (post_whisker a L) (pre_whisker S (lm_mult T L))).

Definition LModule_comp_laws {D : precategory} {T : Monad C} {S : Monad C}
{a : T S S T} (l : monad_dist_laws a) (L : LModule T D) :
(LModule_laws T (LModule_comp_data a L)) := make_dirprod (LModule_comp_law1 l L)
(LModule_comp_law2 l L).

Definition LModule_deriv {D : precategory} {T : Monad C} (L : LModule T D) : LModule T D :=
(LModule_comp_data (deriv_dist T) L,, LModule_comp_laws (deriv_dist_is_monad_dist T) L).

End deriv_def.

End maybe_def.

Derivation on modules commutes with the pullback: if m is a monad morphism, then m*(M') is isomorphic to m*(M)'
Section pullback_deriv.
Context {C : precategory}
(o : C)
(bcpC : limits.bincoproducts.BinCoproducts C )
{D : category}.

Let MOD (R : Monad C) := (precategory_LModule R D).
Context {R S : Monad C} (f : Monad_Mor R S) (M : LModule S D).
Local Notation "M '" := (LModule_deriv o bcpC M) (at level 30).

Local Notation pb_d := (pb_LModule f (M ')).
Local Notation d_pb := ((pb_LModule f M ) ').

Pointwise equality of the involved multiplication
Lemma pb_LModule_deriv_eq_mult c :
# M (BinCoproductOfArrows C (bcpC o (R c)) (bcpC o (S c)) (identity o) (pr1 f c)) ·
(# (pr1 M)
(BinCoproductArrow C (bcpC o (S c)) (BinCoproductIn1 C (bcpC o c) · pr1 (η S) (bcpC o c))
(# (pr1 S) (BinCoproductIn2 C (bcpC o c)))) · pr1 (lm_mult S M) (bcpC o c)) =
# (pr1 M)
(BinCoproductArrow C (bcpC o (R c)) (BinCoproductIn1 C (bcpC o c) · pr1 (η R) (bcpC o c))
(# (pr1 R) (BinCoproductIn2 C (bcpC o c)))) · (# (pr1 M) (pr1 f (bcpC o c)) ·
(lm_mult S M) (bcpC o c)).
Proof.
repeat rewrite assoc.
apply cancel_postcomposition.
do 2 rewrite <- functor_comp.
apply maponpaths.
etrans;[ apply precompWithBinCoproductArrow|].
rewrite id_left.
rewrite postcompWithBinCoproductArrow.
apply map_on_two_paths.
- rewrite <- assoc.
apply cancel_precomposition.
apply pathsinv0.