{UA : Univalence} {PR : PropResizing} (X : HSet) n : infinite X -> infinite (power_iterated X n). Proof. intros H. eapply infinite_inject; try apply H. apply Injection_power_iterated. Qed.
From HoTT Require Import Basics Types TruncType. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Card Spaces.Nat.Core.