Definition initial_enriched_from_iso {x y : C} (Hx : is_initial_enriched x) (f : z_iso x y) : is_initial_enriched y. Proof. intros w. use (iso_to_Terminal (_ ,, Hx w)) ; cbn. exact (precomp_arr_z_iso E w (z_iso_inv 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.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.