proposition: Lemma MorMap_iscontr (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 : C) (eqclass : RoofEqclass x y) : iscontr (∑ g : D⟦F x, F y⟧, ∏ (R : Roof x y) (H1 : RoofEqclassIn (eqclass) R), g = MorMap D hsD F x y H' R).
proof: Proof. use (squash_to_prop (pr1 (RoofEqclassIs eqclass))). apply isapropiscontr. intros R. induction R as [R1 R2]. set (tmp := MorMap_iscomprelfun D hsD F x y H'). unfold iscomprelfun in tmp. use unique_exists. - exact (MorMap D hsD F x y H' R1). - cbn. intros R' HR'. apply tmp. use (eqax2 (RoofEqclassIs eqclass)). + exact R2. + exact HR'. - intros y0. apply impred_isaprop. intros t. apply impred_isaprop. intros t0. apply hsD. - intros y0 T. cbn beta in T. exact (T R1 R2). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors