proposition: Fact Cantor_injects_injects {X Y : HSet} : InjectsInto (X -> HProp) (X + Y) -> InjectsInto (X + X) X -> InjectsInto (X -> HProp) Y.
proof: Proof. intros H1 H2. assert (HF : InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)). - eapply InjectsInto_trans; try apply H1. eapply InjectsInto_trans; try apply InjectsInto_power_morph, H2. rewrite path_sum_prod. apply tr. reflexivity. - eapply merely_destruct; try apply HF. intros [f Hf]. pose (R x p := hexists (fun q => f (p, q) = inl x)). destruct (@Cantor_rel _ R) as [p Hp]. { intros x p p' H3 H4. eapply merely_destruct; try apply H3. intros [q Hq]. eapply merely_destruct; try apply H4. intros [q' Hq']. apply tr. change p with (fst (p, q)). rewrite (Hf (p, q) (p', q')); trivial. now rewrite Hq, Hq'. } pose (f' q := f (p, q)). assert (H' : forall q x, f' q <> inl x). + intros q x H. apply (Hp x). apply tr. exists q. apply H. + apply tr. exists (fun x => proj1 (clean_sum _ H' x)). intros q q' H. assert (Hqq' : f' q = f' q'). * destruct clean_sum as [z <-]. destruct clean_sum as [z' <-]. cbn in H. now rewrite H. * apply Hf in Hqq'. change q with (snd (p, q)). now rewrite Hqq'. Qed.
imports: HoTT(TruncType ExcludedMiddle abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card) HoTT(Equiv.BiInv) HoTT(HIT.unique_choice) HoTT.Sets(Ordinals Hartogs Powers GCH AC)