Definition weqlogeq (P Q : hProp) : (P = Q) ≃ (P ⇔ Q). Proof. intros. apply weqimplimpl. - intro e. induction e. apply isrefl_logeq. - intro c. apply hPropUnivalence. + exact (pr1 c). + exact (pr2 c). - apply isasethProp. - apply propproperty. Defined.