proposition: Lemma LocalizationUniversalFunctorUnique (D : precategory) (hsD : has_homsets D) (F : functor C D) (H' : ∏ (x y : C) (f : C ⟦ x, y ⟧), SOM x y f → is_iso (# F f)) (y : functor loc_precategory D) (T : functor_composite FunctorToLocalization y = F) : y = (LocalizationUniversalFunctor D hsD F H').
proof: Proof. use (functor_eq _ _ hsD). use total2_paths_f. - induction T. apply idpath. - use funextsec. intros a. use funextsec. intros b. use funextsec. intros f. induction T. cbn. use (squash_to_prop (pr1 (RoofEqclassIs f))). apply hsD. intros f'. induction f' as [f1 f2]. rewrite (RoofEqclassEqRoof f f1 f2). use (pathscomp0 _ (! (pr2 (pr1 (MorMap_iscontr D hsD (functor_composite FunctorToLocalization y) H' a b (RoofEqclassFromRoof f1))) f1 (RoofEqclassFromRoofIn f1)))). rewrite (RoofEqclassToRoofComp f1). rewrite <- (RoofEqclassCompToRoofComp (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1)) (MorToRoof (RoofMor2 f1))). use (pathscomp0 (@functor_comp loc_precategory D y _ _ _ (RoofEqclassFromRoof (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))) (RoofEqclassFromRoof (MorToRoof (RoofMor2 f1))))). unfold functor_composite. cbn. apply cancel_postcomposition. set (iso1 := make_iso _ (H' f1 a (RoofMor1 f1) (RoofMor1Is f1))). apply (post_comp_with_iso_is_inj _ _ _ (pr2 iso1)). use (pathscomp0 _ (! (iso_after_iso_inv iso1))). unfold iso1. clear iso1. cbn. set (tmp := @functor_comp loc_precategory D y _ _ _ (RoofEqclassFromRoof (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))) (RoofEqclassFromRoof (MorToRoof (RoofMor1 f1)))). unfold functor_on_morphisms in tmp. apply pathsinv0 in tmp. use (pathscomp0 tmp). clear tmp. rewrite RoofEqclassCompInvRToId. apply (@functor_id loc_precategory D y). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors