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