Definition make_is_initial_enriched_from_iso (TV : Terminal V) (x : C) (Hx : ∏ (y : C), is_z_isomorphism (TerminalArrow TV (E ⦃ x , y ⦄))) : is_initial_enriched x. Proof. intros y. use (iso_to_Terminal TV). exact (z_iso_inv (TerminalArrow TV (E ⦃ x , y ⦄) ,, Hx y)). 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.