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