X (f : X -> X -> Type) : { p | forall x, f x <> p }. Proof. exists (fun x => ~ f x x). intros x H. enough (Hx : f x x <-> ~ f x x). - apply Hx; apply Hx; intros H'; by apply Hx. - pattern (f x) at 1. rewrite H. reflexivity. 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.