Lemma UA_for_Predicates (P : UU -> hProp) (X X' : UU) (pX : P X) (pX' : P X') : (tpair _ X pX) = (tpair P X' pX') ≃ (X ≃ X'). Proof. set (f := Id_p_weq_Id P X X' pX pX'). set (g := tpair _ _ (univalenceAxiom X X')). exact (weqcomp f g). Defined.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.UnivalenceAxiom.