********************************************************** Contents:

• "maybe" monad (binary coproduct with a fixed object) maybe_monad
• distributive laws for pairs of monads monad_dist_laws
  • in particular: the distributive law for the maybe monad and any monad deriv_dist
• composition of two monads with a distributive law monad_comp
  • in particular: derivative of a monad (composing with maybe) monad_deriv
• monad morphism from the first composand to the composition of monads monad_to_comp
  • in particular: monad morphism from a monad to its derivative monad_to_deriv
• 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)

Definition of distributive laws for Monads and composition of Monads

cf. Beck "Distributive laws" (1969)

distributivity law for a pair of monads

composition of monads with a distributive law

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 ------------------------------------------------

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 ------------------------------------------------

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.

morphism from the factor T to the composite S ∙ T of two monads

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)

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

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

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

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

the morphism from a monad to its derivative

derivative of a left module over a monad

Derivation on modules commutes with the pullback: if m is a monad morphism, then m*(M') is isomorphic to m*(M)'

Pointwise equality of the involved multiplication