proposition: Lemma LocalizationUniversalCategory (CC : precategory) (hss : has_homsets CC) (In : functor C CC) (H' : ∏ (x y : C) (f : x --> y) (s : SOM x y f), is_iso (# In f)) (HH : ∏ (D : precategory) (hsD : has_homsets D) (F : functor C D) (H' : ∏ (x y : C) (f : x --> y) (s : SOM x y f), is_iso (# F f)), ∑ HH : functor CC D, (functor_composite In HH = F) × (∏ (yy : functor CC D) (comm : functor_composite In yy = F), yy = HH)) : ∑ D : (functor CC loc_precategory × functor loc_precategory CC), (functor_composite (dirprod_pr1 D) (dirprod_pr2 D) = (functor_identity _)) × (functor_composite (dirprod_pr2 D) (dirprod_pr1 D) = (functor_identity _)).
proof: Proof. set (comm1 := LocalizationUniversalFunctorComm CC hss In H'). set (tmp := HH loc_precategory has_homsets_loc_precategory FunctorToLocalization FunctorToLocalization_is_iso). induction tmp as [inv1 p]. induction p as [comm2 unique2]. set (inv2 := (LocalizationUniversalFunctor CC hss In H')). use tpair. - use make_dirprod. + exact inv1. + exact inv2. - use make_dirprod. + cbn. rewrite <- comm2 in comm1. rewrite functor_assoc in comm1. set (tmp := HH CC hss In H'). induction tmp as [F' CC2]. induction CC2 as [comm3 unique3]. set (tmp1 := unique3 (functor_identity CC) (functor_identity_right _ _ _)). set (tmp2 := unique3 (functor_composite inv1 (LocalizationUniversalFunctor CC hss In H')) comm1). rewrite <- tmp1 in tmp2. exact tmp2. + cbn. rewrite <- comm1 in comm2. rewrite functor_assoc in comm2. set (tmp := LocalizationUniversalFunctorUnique loc_precategory has_homsets_loc_precategory FunctorToLocalization FunctorToLocalization_is_iso). set (tmp1 := tmp _ comm2). fold inv2 in tmp1. set (tmp2 := tmp (functor_identity _) (functor_identity_right _ _ _)). rewrite <- tmp2 in tmp1. exact tmp1. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors