Lemma isdecpropweqb {X Y} : X≃Y -> isdecprop Y -> isdecprop X. Proof. intros w i. unfold isdecprop in *. induction i as [yny i]. split. - clear i. induction yny as [y|ny]. * apply ii1. apply (invmap w). assumption. * apply ii2. intro x. apply ny. apply w. assumption. - apply (isofhlevelweqb 1 (Y:=Y)). { exact w. } { exact i. } Defined.