{A B : Type} (R : A -> B -> HProp) := (forall a : A, hexists (fun (b : B) => R a b)) * (forall b : B, hexists (fun (a : A) => R a b)).
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.