IsInjective uni_fix. 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.
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.