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. intros HR. pose (pc x := Build_HProp (smalltype (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'; by apply Hpc. } - intros Hx. apply equiv_smalltype in Hx. by apply Hx. - intros Hx. apply equiv_smalltype. intros p Hp. eapply merely_destruct; try apply (HR _ _ _ Hp H). by intros ->. 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.