- (* but in fact strict (meaning the functor's coherence maps are identities) *)
- (*; fc_strict : forall a b, #(mf_first a b) ~~ id _
- FIXME - I will need to separate Subcategory from FullSubCategory in order to fix this *)
+ (* 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 _*)