Definition cat_with_enrichment_to_alt {V : monoidal_cat} (E : cat_with_enrichment V) : cat_with_enrichment_alt V. Proof. simple refine ((_ ,, (_ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _)) ,, _). - exact (ob (pr1 E)). - exact (pr11 (pr2 E)). - exact (pr121 (pr2 E)). - exact (pr1 (pr221 (pr2 E))). - exact (pr21 (pr111 E)). - apply identity. - exact (λ _ _ _ f g, f · g). - exact (pr12 (pr221 (pr2 E))). - exact (pr22 (pr221 (pr2 E))). - simple refine (_ ,, _ ,, _). + apply homset_property. + exact (pr211 E). + exact (pr22 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.