Definition cat_with_enrichment_from_alt {V : monoidal_cat} (E : cat_with_enrichment_alt V) : cat_with_enrichment V. Proof. simple refine (((((_ ,, _) ,, (_ ,, _)) ,, _) ,, _) ,, _). - exact (pr11 E). - exact (pr122 (pr221 E)). - exact (pr1 (pr222 (pr221 E))). - exact (pr12 (pr222 (pr221 E))). - exact (pr122 E). - exact (pr12 E). - simple refine ((_ ,, _ ,, _ ,, _ ,, _) ,, _). + exact (pr121 E). + exact (pr1 (pr221 E)). + exact (pr12 (pr221 E)). + exact (pr122 (pr222 (pr221 E))). + exact (pr222 (pr222 (pr221 E))). + exact (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.