Definition enriched_precat_weq_cat_with_enrichment (V : monoidal_cat) : enriched_precat V ≃ cat_with_enrichment V. Proof. use weq_iso. - exact (underlying_cat_with_enrichment V). - exact make_enriched_cat. - exact enriched_precat_weq_cat_with_enrichment_inv_left. - exact enriched_precat_weq_cat_with_enrichment_inv_right. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enriched.Enriched. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Enriched.UnderlyingCategory. Import MonoidalNotations.