Lemma iscontrretract {X Y : UU} (p : X -> Y) (s : Y -> X) (eps : ∏ y : Y, p (s y) = y) (is : iscontr X) : iscontr Y. Proof. intros. set (x := iscontrpr1 is). set (fe := pr2 is). split with (p x). intro t. apply (! (eps t) @ maponpaths p (fe (s t))). Defined.