proposition: Lemma MorMap_iscomprelfun (D : precategory) (hsD : has_homsets D) (F : functor C D) (x y : ob C) (H : ∏ (x y : C) (f : x --> y) (s : SOM x y f), is_iso (# F f)) : iscomprelfun (make_eqrel _ (RoofEqrel x y)) (MorMap D hsD F x y H).
proof: Proof. intros R1 R2 T'. use (squash_to_prop T'). apply hsD. intros T. clear T'. set (iso1 := make_iso _ (H _ _ _ (RoofMor1Is R1))). set (iso2 := make_iso _ (H _ _ _ (RoofMor1Is R2))). set (iso3 := make_iso _ (MorMap_top_mor1_is_iso D hsD F x y H R1 R2 T)). set (iso4 := make_iso _ (MorMap_top_mor2_is_iso D hsD F x y H R1 R2 T)). unfold MorMap. rewrite <- (id_left (# F (RoofMor2 R1))). rewrite <- (iso_after_iso_inv (iso3)). cbn. rewrite <- assoc. rewrite <- functor_comp. rewrite assoc. rewrite <- inv_from_iso_comp. rewrite (RoofTopEq2 T). rewrite functor_comp. fold iso1 iso2 iso3 iso4. assert (X : iso_comp iso3 iso1 = iso_comp iso4 iso2). { apply eq_iso. cbn. rewrite <- functor_comp. rewrite <- functor_comp. apply maponpaths. apply (RoofTopEq1 T). } rewrite X. rewrite inv_from_iso_comp. rewrite <- assoc. apply cancel_precomposition. rewrite assoc. set (tmp := iso_after_iso_inv iso4). cbn in tmp. rewrite tmp. clear tmp. apply id_left. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors