`{PropResizing} {ua : Univalence} (C : Type@{i}) : IsInjective (@power_inj _ C). Proof. intros p p'. unfold power_inj. intros q. apply path_forall. intros a. apply path_iff_hprop; intros Ha. - eapply equiv_smalltype. change ((fun a => Build_HProp (smalltype (p' a))) a). rewrite <- q. apply equiv_smalltype. apply Ha. - eapply equiv_smalltype. change ((fun a => Build_HProp (smalltype (p a))) a). rewrite q. apply equiv_smalltype. apply Ha. Qed.
From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra HSet. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Card. From HoTT.Sets Require Import Ordinals Powers.