(a : V) (b : V) : V := set (fun x : [a] * [b] => [func_of_members (fst x), func_of_members (snd x)]).
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.