- (MF23 :MonoidalFunctor M2 M3 fobj23)
- : MonoidalFunctor M1 M3 (fobj23 ○ fobj12).
- apply PreMonoidalFunctorsCompose.
- apply MF12.
- apply MF23.
- Defined.
+ {PMFF23:Functor C2 C3 fobj23 }
+ (PMF23 :MonoidalFunctor PM2 PM3 PMFF23)
+ := PreMonoidalFunctorsCompose PMF12 PMF23.