{u : V} : IsEmbedding func_of_members := snd (fst (pr2 (pr2 (monic_set_present u)))).
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.