Definition cat_with_enrichment_alt_data_enrichment {V : monoidal_cat} (E : cat_with_enrichment_alt_data V) : enrichment_data (cat_with_enrichment_alt_data_precategory_data E) V. Proof. simple refine (_ ,, _ ,, _ ,, _ ,, _). - exact (pr12 E). - exact (pr122 E). - exact (pr1 (pr222 E)). - exact (pr12 (pr222 (pr222 E))). - exact (pr22 (pr222 (pr222 E))). 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.