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