Lemma coconusfromt_isProofIrrelevant {T : UU} {t : T} (c1 c2 : coconusfromt T t) : c1 = c2. Proof. intros. induction c1 as [x0 x]. induction x. induction c2 as [x1 y]. induction y. apply idpath. Defined.