Definition enrichment_data_of_underlying_category : enrichment_data underlying_category_enriched V. Proof. simple refine (_ ,, _ ,, _ ,, _ ,, _). - exact (λ x y, enriched_cat_mor x y). - exact (λ x , enriched_cat_identity x). - exact (λ x y z, enriched_cat_comp x y z). - exact (λ x y f, f). - exact (λ x y f, f). 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. Import MonoidalNotations.