Lemma isdecpropweqf {X Y} : X≃Y -> isdecprop X -> isdecprop Y. Proof. intros w i. unfold isdecprop in *. induction i as [xnx i]. split. - clear i. induction xnx as [x|nx]. * apply ii1. apply w. assumption. * apply ii2. intro x'. apply nx. apply (invmap w). assumption. - apply (isofhlevelweqf 1 (X:=X)). { exact w. } { exact i. } Defined.