Definition cat_with_enrichment_weq_alt (V : monoidal_cat) : cat_with_enrichment V ≃ cat_with_enrichment_alt V. Proof. use weq_iso. - exact cat_with_enrichment_to_alt. - exact cat_with_enrichment_from_alt. - intro E. apply idpath. - intro E. apply idpath. 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.