fact: Definition bitotal {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)).
imports: HoTT.Basics HoTT.Types HSet TruncType Colimits.SpanPushout HoTT.Truncations.Core Colimits.Quotient