proposition: Lemma homotfromtococonusf {X Y : UU} (f : X -> Y) : ∏ x : X, fromcoconusf f (tococonusf f x) = x.
proof: Proof. intros. unfold fromcoconusf. unfold tococonusf. simpl. apply idpath. Defined.
imports: UniMath.Foundations.Preamble