Definition iscontrcoconustot_comp {X} {x:X} : iscontrpr1 (iscontrcoconustot X x) = x,,idpath x. Proof. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Equivalences.