(v : V) := @set ({x : [v] & [func_of_members x]}) (fun z => func_of_members (pr2 z)).
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.