(u : V) (v : V) : V@{U' U} := set (fun b : Bool => if b then u else v).
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.