Proposition isaprop_conical_colim_enriched (HC : is_univalent C) : isaprop (conical_colim_enriched). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply isaprop_is_conical_colim_enriched. } use total2_paths_f. - use (isotoid _ HC). apply iso_between_conical_colim_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'. apply is_conical_colim_enriched_map_in. 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.OppositeCategory.Core. 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.Colimits.EnrichedCoproducts. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoequalizers. Import MonoidalNotations.