Theorem hlevelretract (n : nat) {X Y : UU} (p : X -> Y) (s : Y -> X) (eps : ∏ y : Y , paths (p (s y)) y) : isofhlevel n X -> isofhlevel n Y. Proof. revert X Y p s eps. induction n as [ | n IHn ]. - intros X Y p s eps X0. unfold isofhlevel. apply (iscontrretract p s eps X0). - unfold isofhlevel. intros X Y p s eps X0 x x'. unfold isofhlevel in X0. assert (is: isofhlevel n (paths (s x) (s x'))) by apply X0. set (s':= @maponpaths _ _ s x x'). set (p':= pathssec2 s p eps x x'). set (eps':= @pathssec3 _ _ s p eps x x'). simpl. apply (IHn _ _ p' s' eps' is). Defined.