Definition isweq_enriched_from_arr (x y : C) : isweq (@enriched_from_arr _ _ E x y). Proof. use isweq_iso. - exact (enriched_to_arr E). - intro f. apply enriched_to_from_arr. - intro f. apply enriched_from_to_arr. 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.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import MonoidalNotations.