Definition terminal_enriched_from_underlying (TC : Terminal C) (TV : Terminal V) (HV : conservative_moncat V) : is_terminal_enriched TC. Proof. use (make_is_terminal_enriched_from_iso TV). intro y. use HV. use isweq_iso. - intro f. apply enriched_from_arr. apply (TerminalArrow TC). - abstract (intros f ; cbn ; refine (_ @ enriched_from_to_arr E f) ; apply maponpaths ; apply TerminalArrowEq). - 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. Import MonoidalNotations.