apply ni_inv.
apply mc1.
apply ni_id.
- Qed.
+ Defined.
Instance MonoidalFunctorsCompose : MonoidalFunctor m1 m3 (f1 >>>> f2) :=
{ mf_id := id_comp (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
; mf_coherence := mf_compose_coherence
}.
- Admitted.
+ admit.
+ admit.
+ admit.
+ Defined.
End MonoidalFunctorsCompose.