proposition: Lemma Cantor_rel X (R : X -> (X -> HProp) -> HProp) : (forall x p p', R x p -> R x p' -> merely (p = p')) -> { p | forall x, ~ R x p }.
proof: Proof. intros HR. pose (pc x := Build_HProp (resize_hprop (forall p : X -> HProp, R x p -> ~ p x))). exists pc. intros x H. enough (Hpc : pc x <-> ~ pc x). 2: split. { apply Hpc; apply Hpc; intros H'; now apply Hpc. } - intros Hx. apply equiv_resize_hprop in Hx. now apply Hx. - intros Hx. apply equiv_resize_hprop. intros p Hp. eapply merely_destruct; try apply (HR _ _ _ Hp H). now intros ->. 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)