proposition: Lemma LocalizationUniversalProperty (D : precategory) (hsD : has_homsets D) (hssD : isaset D) (F : functor C D) (H' : ∏ (x y : C) (f : x --> y) (s : SOM x y f), is_iso (# F f)) : iscontr (∑ H : functor loc_precategory D, functor_composite FunctorToLocalization H = F).
proof: Proof. use unique_exists. - exact (LocalizationUniversalFunctor D hsD F H'). - exact (LocalizationUniversalFunctorComm D hsD F H'). - intros y. apply (functor_isaset _ _ hsD hssD). - exact (LocalizationUniversalFunctorUnique D hsD F H'). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors