Definition initial_underlying : Initial C. Proof. refine (x ,, _). intros y. use iscontraprop1. - abstract (use invproofirrelevance ; intros f g ; refine (!(enriched_to_from_arr E f) @ _ @ enriched_to_from_arr E g) ; apply maponpaths ; apply is_initial_enriched_eq). - exact (enriched_to_arr E (is_initial_enriched_arrow 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.