proposition: Lemma injective_uni_fix : IsInjective uni_fix.
proof: Proof. intros X Y. unfold uni_fix. intros H % injective_power_morph; trivial. intros P Q. intros H' % injective_power_morph; trivial. intros p q. apply injective_power_inj. Qed.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra HSet) HoTT(PropResizing.PropResizing) HoTT(Spaces.Card) HoTT.Sets(Ordinals Powers)