(a : V) (b : V) (f : V) := f ⊆ (a × b) * (forall x, x ∈ a -> hexists (fun y => y ∈ b * [x,y] ∈ f)) * (forall x y y', [x,y] ∈ f * [x,y'] ∈ f -> y = y').
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.