{u : V} : [u] -> V := pr1 (pr2 (monic_set_present u)) : [u] -> V.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.