Lemma isapropretract {P Q : UU} (i : isaprop Q) (f : P -> Q) (g : Q -> P) (h : g ∘ f ~ idfun _) : isaprop P. Proof. intros. apply invproofirrelevance; intros p p'. refine (_ @ (_ : g (f p) = g (f p')) @ _). - apply pathsinv0. apply h. - apply maponpaths. apply proofirrelevance. exact i. - apply h. Defined.