Definition isaprop_terminal_enriched (HC : is_univalent C) : isaprop terminal_enriched. Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply isaprop_is_terminal_enriched. } use (isotoid _ HC). use iso_between_terminal_enriched. - exact (pr2 φ₁). - exact (pr2 φ₂). 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.