Definition iso_between_initial_enriched {x y : C} (Hx : is_initial_enriched x) (Hy : is_initial_enriched y) : z_iso x y. Proof. use make_z_iso. - exact (enriched_to_arr E (is_initial_enriched_arrow Hx y)). - exact (enriched_to_arr E (is_initial_enriched_arrow Hy x)). - split. + abstract (refine (enriched_to_arr_comp E _ _ @ _ @ enriched_to_arr_id E _) ; apply maponpaths ; apply (is_initial_enriched_eq Hx)). + abstract (refine (enriched_to_arr_comp E _ _ @ _ @ enriched_to_arr_id E _) ; apply maponpaths ; apply (is_initial_enriched_eq Hy)). 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.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Initial. Import MonoidalNotations.