(U V : 𝒫 A) := (forall a, U a -> V a) /\ merely (exists a : A, V a /\ ~(U a)).
From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra HSet. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Card. From HoTT.Sets Require Import Ordinals Powers.