X Y : InjectsInto X Y -> InjectsInto (X -> HProp) (Y -> HProp). Proof. intros HF. eapply merely_destruct; try apply HF. intros [f Hf]. apply tr. exists (fun p => fun y => hexists (fun x => p x /\ y = f x)). intros p q H. apply path_forall. intros x. apply equiv_path_iff_hprop. split; intros Hx. - assert (Hp : (fun y : Y => hexists (fun x : X => p x * (y = f x))) (f x)). { apply tr. exists x. split; trivial. } pattern (f x) in Hp. rewrite H in Hp. eapply merely_destruct; try apply Hp. by intros [x'[Hq <- % Hf]]. - assert (Hq : (fun y : Y => hexists (fun x : X => q x * (y = f x))) (f x)). { apply tr. exists x. split; trivial. } pattern (f x) in Hq. rewrite <- H in Hq. eapply merely_destruct; try apply Hq. by intros [x'[Hp <- % Hf]]. Qed.
From HoTT Require Import TruncType ExcludedMiddle abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Nat.Core Spaces.Card. From HoTT Require Import Equiv.BiInv. From HoTT Require Import HIT.unique_choice. From HoTT.Sets Require Import Ordinals Hartogs Powers GCH AC.