+ (iii.1) unit <=< p = p (here p has to be a natural transformation to M(1C))
+ (iii.2) p = p <=< unit (here p has to be a natural transformation from 1C)
+
+If `p` is a natural transformation from `P` to `M(1C)` and `q` is `(p Q')`, that is, a natural transformation from `PQ` to `MQ`, then we can extend (iii.1) as follows:
+
+ q = (p Q')
+ = ((unit <=< p) Q')
+ = ((join -v- (M unit) -v- p) Q')
+ = (join Q') -v- ((M unit) Q') -v- (p Q')
+ = (join Q') -v- (M (unit Q')) -v- q
+ ??
+ = (unit Q') <=< q
+
+where as we said `q` is a natural transformation from some `PQ'` to `MQ'`.
+
+Similarly, if `p` is a natural transformation from `1C` to `MP'`, and `q` is `(p Q)`, that is, a natural transformation from `Q` to `MP'Q`, then we can extend (iii.2) as follows:
+
+ q = (p Q)
+ = ((p <=< unit) Q)
+ = (((join P') -v- (M p) -v- unit) Q)
+ = ((join P'Q) -v- ((M p) Q) -v- (unit Q))
+ = ((join P'Q) -v- (M (p Q)) -v- (unit Q))
+ ??
+ = q <=< (unit Q)
+
+where as we said `q` is a natural transformation from `Q` to some `MP'Q`.