Lemma homottofromcoconusf {X Y : UU} (f : X -> Y) : ∏ yxe : coconusf f, tococonusf f (fromcoconusf f yxe) = yxe. Proof. intros. induction yxe as [y xe]. induction xe as [x e]. unfold fromcoconusf. unfold tococonusf. simpl. induction e. apply idpath. Defined.