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