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