Definition isaprop_initial_enriched (HC : is_univalent C) : isaprop initial_enriched. Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply isaprop_is_initial_enriched. } use (isotoid _ HC). use iso_between_initial_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. Require Import UniMath.CategoryTheory.Limits.Initial. Import MonoidalNotations.