Lemma cone_eq {C I:category} (c:C^op) (D: I⟶C) (p q:cone (C:=C) c D) : pr1 p ~ pr1 q -> p = q. Proof. intros h. apply subtypePath. { intro r. apply impred_isaprop; intro i; apply impred_isaprop; intro j; apply impred_isaprop; intro e. apply homset_property. } apply funextsec; intro i; apply h. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import Require Import Require Import UniMath.MoreFoundations.Tactics.