exists f : hartogs_number -> 𝒫 (𝒫 (𝒫 A)), IsInjective f. Proof. cbn. exists proj1. intros [X HX] [Y HY]. cbn. intros ->. apply ap. apply path_ishprop. 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.