+Transparent HomFunctor.
+
+Structure SurjectiveMonicMonoidalEnrichment (e:Enrichment) :=
+{ smme_se : SurjectiveEnrichment e
+; smme_monoidal : MonoidalEnrichment e
+; smme_me : MonicMonoidalEnrichment _ smme_monoidal
+}.
+Coercion smme_se : SurjectiveMonicMonoidalEnrichment >-> SurjectiveEnrichment.
+Coercion smme_me : SurjectiveMonicMonoidalEnrichment >-> MonicMonoidalEnrichment.
+
+(* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
+Structure SMME :=
+{ smme_e : Enrichment
+; smme_see : SurjectiveEnrichment smme_e
+; smme_mon : MonoidalEnrichment smme_e
+; smme_mee : MonicMonoidalEnrichment _ smme_mon
+}.
+Coercion smme_e : SMME >-> Enrichment.
+Coercion smme_see : SMME >-> SurjectiveEnrichment.
+Coercion smme_mon : SMME >-> MonoidalEnrichment.
+Coercion smme_mee : SMME >-> MonicMonoidalEnrichment.