- (* but in fact strict (meaning the functor's coherence maps are identities) *)
- ; fc_strict : forall a, iso_forward (mf_coherence fc_mf_J a) ~~ id _
+ (* and strict (meaning the functor's coherence maps are identities) *)
+ ; fc_strict_first : forall a b, #(mf_first(PreMonoidalFunctor:=fc_mf_J) a b) ~~ id _ (* mf_consistent gives us mf_second *)
+(* ; fc_strict_id : #(mf_i(PreMonoidalFunctor:=fc_mf_J)) ~~ id _*)