{UA : Univalence} {PR : PropResizing} (X : HSet) n : Injection X (power_iterated X n). Proof. induction n as [|n IHn]. - reflexivity. - eapply Injection_trans; try apply IHn. apply Injection_power. exact _. Qed.
From HoTT Require Import Basics Types TruncType. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Card Spaces.Nat.Core.