proposition: Lemma hartogs_number_injection : exists f : hartogs_number -> 𝒫 (𝒫 (𝒫 A)), IsInjective f.
proof: Proof. cbn. exists proj1. intros [X HX] [Y HY]. cbn. intros ->. apply ap. apply path_ishprop. Qed.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra HSet) HoTT(PropResizing.PropResizing) HoTT(Spaces.Card) HoTT.Sets(Ordinals Powers)