`{PropResizing} {ua : Univalence} {C B : Type@{i}} (f : C -> B) : IsInjective f -> IsInjective (@power_morph _ _ C B f). Proof. intros Hf p p' q. apply path_forall. intros a. apply path_iff_hprop; intros Ha. - enough (Hp : power_morph f p (f a)). + rewrite q in Hp. apply equiv_smalltype in Hp. apply Hp. reflexivity. + apply equiv_smalltype. intros a' -> % Hf. apply Ha. - enough (Hp : power_morph f p' (f a)). + rewrite <- q in Hp. apply equiv_smalltype in Hp. apply Hp. reflexivity. + apply equiv_smalltype. intros a' -> % Hf. 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.