(u : V) (v : V) : V := V_pair (V_singleton u) (V_pair u v).
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.