proposition: Lemma indexed_set_cat_isaprop_is_cone_mor (t : indexed_set_cat ⟦ c, indexed_set_cat_tip ⟧) : isaprop (is_cone_mor cc indexed_set_cat_cone t).
proof: Proof. intro. apply impred_isaprop. intro. apply (homset_property indexed_set_cat). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits