proposition: Lemma MorMap_compose (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)) {x y z : ob C} (R1 : Roof x y) (R2 : Roof y z) : MorMap D hsD F x z H' (roof_comp R1 R2) = MorMap D hsD F x y H' R1 · MorMap D hsD F y z H' R2.
proof: Proof. set (sqr := isLocClassSqr2 iLC R2 R1 y (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R1)). unfold roof_comp. fold sqr. unfold MorMap at 1. cbn. set (iso1 := make_iso (# F (LocSqr2Mor2 sqr · RoofMor1 R1)) (H' sqr x (LocSqr2Mor2 sqr · RoofMor1 R1) (isLocClassComp iLC sqr R1 x (LocSqr2Mor2 sqr) (LocSqr2Mor2Is sqr) (RoofMor1 R1) (RoofMor1Is R1)))). set (iso2 := make_iso _ (H' sqr R1 (LocSqr2Mor2 sqr) (LocSqr2Mor2Is sqr))). set (iso3 := make_iso _ (H' R1 x (RoofMor1 R1) (RoofMor1Is R1))). set (iso4 := make_iso _ (H' R2 y (RoofMor1 R2) (RoofMor1Is R2))). assert (X : iso1 = iso_comp iso2 iso3). { use eq_iso. cbn. rewrite functor_comp. apply idpath. } rewrite X. rewrite inv_from_iso_comp. rewrite functor_comp. rewrite assoc. unfold MorMap. rewrite assoc. fold iso3 iso4. apply cancel_postcomposition. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. set (tmp := LocSqr2Comm sqr). apply (pre_comp_with_iso_is_inj (C:=D) _ _ _ _ (pr2 iso2)). rewrite assoc. set (tmp2 := iso_inv_after_iso iso2). cbn in tmp2. cbn. rewrite tmp2. clear tmp2. rewrite id_left. apply (post_comp_with_iso_is_inj (C:=D) _ _ _ (pr2 iso4)). cbn. rewrite <- functor_comp. rewrite tmp. clear tmp. rewrite functor_comp. rewrite <- assoc. apply cancel_precomposition. rewrite <- assoc. set (tmp2 := iso_after_iso_inv iso4). cbn in tmp2. rewrite tmp2. rewrite id_right. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors