Definition make_is_terminal_enriched (x : C) (f : ∏ (w : V) (y : C), w --> E ⦃ y , x ⦄) (p : ∏ (w : V) (y : C) (f g : w --> E ⦃ y , x ⦄), f = g) : is_terminal_enriched x. Proof. intros y w. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; apply p). - apply f. 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.