Definition terminal_underlying : Terminal 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_terminal_enriched_eq). - exact (enriched_to_arr E (is_terminal_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. Import MonoidalNotations.