proposition: Lemma hCantor {X} (f : X -> X -> HProp) : { p | forall x, f x <> p }.
proof: Proof. exists (fun x => Build_HProp (f x x -> Empty)). intros x H. enough (Hx : f x x <-> ~ f x x). - apply Hx; apply Hx; intros H'; now apply Hx. - pattern (f x) at 1. rewrite H. reflexivity. 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)