proposition: Lemma monic_set_present : forall u : V, exists (Au : Type) (m : Au -> V), (IsHSet Au) * (IsEmbedding m) * (u = set m).
proof: Proof. apply V_ind_hprop. - intros A f _. destruct (quotient_kernel_factor_general f (ker_bisim f) (ker_bisim_is_ker f)) as [Au [eu [mu (((hset_Au, epi_eu), mono_mu), factor)]]]. exists Au, mu. split;[exact (hset_Au, mono_mu)|]. apply setext'; split. + intro a. apply tr; exists (eu a). exact (ap10 factor a). + intro a'. generalize (epi_eu a'). intro IC; refine (Trunc_functor (-1) _ (@center _ IC)). intros [a p]. exists a. transitivity (mu (eu a)). * exact (ap10 factor a). * exact (ap mu p). - intro v. apply hprop_allpath. intros [Au [mu ((hset, mono), p)]]. intros [Au' [mu' ((hset', mono'), p')]]. apply monic_set_present_uniqueness. Defined.
imports: HoTT.Basics HoTT.Types HSet TruncType Colimits.SpanPushout HoTT.Truncations.Core Colimits.Quotient