proposition: Lemma LocalizationUniversalFunctor_isfunctor (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)) : @is_functor loc_precategory_data D (functor_data_constr loc_precategory_ob_mor D (λ x : C, F x) (λ (x y : C) (eqclass : RoofEqclass x y), pr1 (pr1 (MorMap_iscontr D hsD F H' x y eqclass)))).
proof: Proof. split. - intros x. cbn. cbn in *. set (tmp := pr2 (pr1 (MorMap_iscontr D hsD F H' x x (IdRoofEqclass x))) (IdRoof x)). assert (H2 : MorMap D hsD F x x H' (IdRoof x) = identity (F x)). { unfold MorMap. cbn. set (iso := make_iso _ (H' x x (identity x) (isLocClassIs iLC x))). set (tmpp := iso_after_iso_inv iso). cbn in tmpp. apply tmpp. } use (pathscomp0 _ H2). apply tmp. apply RoofEqclassFromRoofIn. - intros x y z R1 R2. cbn. use (squash_to_prop (pr1 (RoofEqclassIs R1))). apply hsD. intros R1'. induction R1' as [R1' R1'']. use (squash_to_prop (pr1 (RoofEqclassIs R2))). apply hsD. intros R2'. induction R2' as [R2' R2'']. rewrite (MorMap_iscontr_eq D hsD F H' x y R1 R1' R1''). rewrite (MorMap_iscontr_eq D hsD F H' y z R2 R2' R2''). rewrite (roof_comp_iscontr_eqclass R1 R2 R1' R1'' R2' R2''). set (tmp := pr2 (pr1 (MorMap_iscontr D hsD F H' x z (RoofEqclassFromRoof (roof_comp R1' R2')))) (roof_comp R1' R2') (RoofEqclassFromRoofIn (roof_comp R1' R2'))). rewrite tmp. clear tmp. apply MorMap_compose. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors