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