Definition initial_enriched_from_underlying (TC : Initial C) (TV : Terminal V) (HV : conservative_moncat V) : is_initial_enriched TC. Proof. use (make_is_initial_enriched_from_iso TV). intro y. use HV. use isweq_iso. - intro f. apply enriched_from_arr. apply (InitialArrow TC). - abstract (intros f ; cbn ; refine (_ @ enriched_from_to_arr E f) ; apply maponpaths ; apply InitialArrowEq). - abstract (intros f ; cbn ; apply TerminalArrowEq). 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.