- (* 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 _
+ (* 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 *)