exists f : hartogs_number' -> (𝒫 (𝒫 (𝒫 A))), IsInjective f. Proof. transparent assert (ϕ : (forall X : 𝒫 (𝒫 A), Lt X)). { intros X. intros x1 x2. exact (x1.1 ⊊ x2.1). } unshelve eexists. - intros [B _]. intros X. exact (merely (Isomorphism (X : Type; ϕ X) B)). - intros [B B_A] [C C_A] H0. apply path_sigma_hprop; cbn. revert B_A. rapply Trunc_rec. intros [f injective_f]. apply equiv_path_Ordinal. assert {X : 𝒫 (𝒫 A) & Isomorphism (X : Type; ϕ X) B} as [X iso]. { assert (H2 : forall X : 𝒫 A, IsHProp { b : B & forall a, X a <-> exists b', b' < b /\ a = f b' }). { intros X. apply hprop_allpath; intros [b1 Hb1] [b2 Hb2]. snrapply path_sigma_hprop; cbn. - intros b. snrapply istrunc_forall. intros a. snrapply istrunc_prod. 2: exact _. snrapply istrunc_arrow. rapply ishprop_sigma_disjoint. intros b1' b2' [_ ->] [_ p]. apply (injective_f). exact p. - apply extensionality. intros b'. split. + intros b'_b1. specialize (Hb1 (f b')). apply snd in Hb1. specialize (Hb1 (b'; (b'_b1, idpath))). apply Hb2 in Hb1. destruct Hb1 as (? & H2 & H3). apply injective in H3. 2: assumption. destruct H3. exact H2. + intros b'_b2. specialize (Hb2 (f b')). apply snd in Hb2. specialize (Hb2 (b'; (b'_b2, idpath))). apply Hb1 in Hb2. destruct Hb2 as (? & H2 & H3). apply injective in H3. 2: assumption. destruct H3. exact H2. } exists (fun X : 𝒫 A => Build_HProp { b : B & forall a, X a <-> exists b', b' < b /\ a = f b' }). { unfold subtype_as_type'. unshelve eexists. - srapply equiv_adjointify. + intros [X [b _]]. exact b. + intros b. unshelve eexists (fun a => Build_HProp (exists b', b' < b /\ a = f b')). 1: exact _. { apply hprop_allpath. intros [b1 [b1_b p]] [b2 [b2_b q]]. apply path_sigma_hprop; cbn. apply (injective f). destruct p, q. reflexivity. } exists b. intros b'. cbn. reflexivity. + cbn. reflexivity. + cbn. intros [X [b Hb]]. apply path_sigma_hprop. cbn. apply path_forall; intros a. apply path_iff_hprop; apply Hb. - cbn. intros [X1 [b1 H'1]] [X2 [b2 H'2]]. unfold ϕ, proper_subtype_inclusion. cbn. split. + intros H3. refine (Trunc_rec _ (trichotomy_ordinal b1 b2)). intros [b1_b2 | H4]. * exact b1_b2. * revert H4. rapply Trunc_rec. intros [b1_b2 | b2_b1]. -- apply Empty_rec. destruct H3 as [_ H3]. revert H3. rapply Trunc_rec. intros [a [X2a not_X1a]]. apply not_X1a. apply H'1. rewrite b1_b2. apply H'2. exact X2a. -- apply Empty_rec. destruct H3 as [_ H3]. revert H3. rapply Trunc_rec. intros [a [X2a not_X1a]]. apply not_X1a. apply H'1. apply H'2 in X2a. destruct X2a as [b' [b'_b2 a_fb']]. exists b'. split. ++ transitivity b2; assumption. ++ assumption. + intros b1_b2. split. * intros a X1a. apply H'2. apply H'1 in X1a. destruct X1a as [b' [b'_b1 a_fb']]. exists b'. split. -- transitivity b1; assumption. -- assumption. * apply tr. exists (f b1). split. -- apply H'2. exists b1; auto. -- intros X1_fb1. apply H'1 in X1_fb1. destruct X1_fb1 as [b' [b'_b1 fb1_fb']]. apply (injective f) in fb1_fb'. destruct fb1_fb'. apply irreflexivity in b'_b1. 2: exact _. assumption. } } assert (IsOrdinal X (ϕ X)) by exact (isordinal_simulation iso.1). apply apD10 in H0. specialize (H0 X). cbn in H0. refine (transitive_Isomorphism _ (X : Type; ϕ X) _ _ _). { apply isomorphism_inverse. assumption. } enough (merely (Isomorphism (X : Type; ϕ X) C)). { revert X1. nrapply Trunc_rec. { exact (ishprop_Isomorphism (Build_Ordinal X (ϕ X) _) C). } auto. } rewrite <- H0. apply tr. exact iso. 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.