Proposition isaprop_conical_lim_enriched (HC : is_univalent C) : isaprop (conical_lim_enriched). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply isaprop_is_conical_lim_enriched. } use total2_paths_f. - use (isotoid _ HC). apply iso_between_conical_lim_enriched. - use subtypePath. { intro. repeat (use impred ; intro). apply homset_property. } rewrite pr1_transportf. rewrite transportf_sec_constant. use funextsec. intro j. rewrite transportf_isotoid. use z_iso_inv_on_right ; cbn. refine (!_). apply is_conical_lim_enriched_map_pr. Qed.
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.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedProducts. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedEqualizers. Import MonoidalNotations.