proposition: Theorem quotient_kernel_factor : exists (C : Type) (e : A -> C) (m : C -> B), IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e).
proof: Proof. pose (C := quotient R). assert (IsHSet C) by (unfold C; apply _). exists C. pose (e := class_of R). exists e. transparent assert (m : (C -> B)). { apply quotient_ind with f; try exact _. intros x y H. transitivity (f x). - apply transport_const. - exact ((is_ker x y) ^-1 H). } exists m. split;[split;[split|]|]. - assumption. - apply quotient_surjective. - intro u. apply hprop_allpath. assert (H : forall (x y : C) (p : m x = u) (p' : m y = u), x = y). { simple refine (quotient_ind R _ _ _). - intro a. simple refine (quotient_ind R _ _ _). + intros a' p p'; fold e in p, p'. * apply related_classes_eq. refine (is_ker a a' _). change (m (e a) = m (e a')). exact (p @ p'^). + intros; apply path_ishprop. - intros; apply path_ishprop. } intros [x p] [y p']. apply path_sigma_hprop; simpl. exact (H x y p p'). - reflexivity. Defined.
imports: HoTT.Basics HoTT.Types HSet TruncType Truncations.Core