Corollary UA_for_HLevels : ∏ (n : nat) (X X' : HLevel n), (X = X') ≃ (pr1 X ≃ pr1 X'). Proof. intros n [X pX] [X' pX']. simpl. apply (UA_for_Predicates (λ X, tpair isaprop (isofhlevel n X) (isapropisofhlevel _ _))). Defined.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.UnivalenceAxiom.