quotient_kernel_factor@{a b ab ab' | a <= ab, b <= ab, ab < ab'} `{Funext} {A : Type@{a}} {B : Type@{b}} `{IsHSet B} (f : A -> B) : exists (C : Type@{ab}) (e : A -> C) (m : C -> B), IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e). Proof. exact (quotient_kernel_factor_general@{a b ab ab' b ab ab} f (fun a b => f a = f b) (fun x y => equiv_idmap)). Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.