-Opaque RepresentableFunctor.
-
-Structure MonoidalEnrichment {e:Enrichment} :=
-{ me_enr :=e
-; me_fobj : prod_obj e e -> e
-; me_f : Functor (e ×× e) e me_fobj
-; me_i : e
-; me_mon : MonoidalCat e me_fobj me_f me_i
-; me_mf : MonoidalFunctor me_mon (enr_v_mon e) (RepresentableFunctor e me_i)
-}.
-Implicit Arguments MonoidalEnrichment [ ].
-Coercion me_mon : MonoidalEnrichment >-> MonoidalCat.
-Coercion me_enr : MonoidalEnrichment >-> Enrichment.
-
-(* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *)
-Structure MonicMonoidalEnrichment {e}{me:MonoidalEnrichment e} :=
-{ ffme_enr := me
-; ffme_mf_full : FullFunctor (RepresentableFunctor e (me_i me))
-; ffme_mf_faithful : FaithfulFunctor (RepresentableFunctor e (me_i me))
-; ffme_mf_conservative : ConservativeFunctor (RepresentableFunctor e (me_i me))
-}.
-Implicit Arguments MonicMonoidalEnrichment [ ].
-Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment.
-Transparent RepresentableFunctor.
-
-Lemma CartesianEnrMonoidal (e:Enrichment) `(C:CartesianCat(Ob:= _)(Hom:= _)(C:=Underlying (enr_c e))) : MonoidalEnrichment e.
- admit.
- Defined.
-
-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.