proposition: Lemma MorMap_top_mor2_is_iso (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)) (R1 R2 : Roof x y) (T : RoofTop R1 R2) : is_iso (# F (RoofTopMor2 T)).
proof: Proof. use (@is_iso_pre D). - exact (F x). - exact (# F (RoofMor1 R2)). - rewrite <- functor_comp. rewrite <- (RoofTopEq1 T). apply H. apply (RoofTopMor1Is T). - apply H. apply (RoofMor1Is R2). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors