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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Definition RoofEqclassFromRoof {x y : ob C} (R : Roof x y) : RoofEqclass x y. Definition RoofEqclassFromRoofIn {x y : ob C} (R : Roof x y) : RoofEqclassIn (RoofEqclassFromRoof R) R. (R : Roof x y) (HR : RoofEqclassIn RE R) : RE = RoofEqclassFromRoof R. use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R))). + apply RoofEqclassFromRoofIn. + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof R))). * apply RoofEqclassFromRoofIn. (H1 : RoofEqclassIn (RoofEqclassFromRoof R1) R2) RoofEqclassIn (RoofEqclassFromRoof R1) R3. exact (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R1)) R2 R3 H2 H1). RoofEqclassIn (pr1 (pr1 (roof_comp_iscontr _ _ _ (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))) use (pr2 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))). - apply RoofEqclassFromRoofIn. - apply RoofEqclassFromRoofIn. exact (RoofEqclassFromRoof (make_Roof x x x (identity x) (identity x) (isLocClassIs iLC x))). - apply RoofEqclassFromRoofIn. - apply RoofEqclassFromRoofIn. * apply RoofEqclassFromRoofIn. - apply RoofEqclassFromRoofIn. * apply RoofEqclassFromRoofIn. RoofEqclassFromRoof (MorToRoof (f · g)) = pr1 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof (MorToRoof f)) (RoofEqclassFromRoof (MorToRoof g)))). set (eqclass := pr1 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof (MorToRoof f)) (RoofEqclassFromRoof (MorToRoof g))))). set (cont := pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof (MorToRoof f)) (RoofEqclassFromRoof (MorToRoof g)))). * set (HR' := RoofEqclassFromRoofIn (MorToRoof (f · g))). use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof (MorToRoof (f · g))))). use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof (MorToRoof (f · g))))). + apply RoofEqclassFromRoofIn. + intros x y f. exact (RoofEqclassFromRoof (MorToRoof f)). pr1 (pr1 (roof_comp_iscontr x y z R1 R2)) = RoofEqclassFromRoof (roof_comp R1' R2'). use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof (roof_comp R1' R2')))). + apply RoofEqclassFromRoofIn. + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof (roof_comp R1' R2')))). * apply RoofEqclassFromRoofIn. Definition InvRoofFromMorInSom {x y : C} (s : y --> x) (S : SOM y x s) : Roof x y. (make_eqrel _ (RoofEqrel x y)) R (roof_comp (InvRoofFromMorInSom (RoofMor1 R) (RoofMor1Is R)) (InvRoofFromMorInSom (RoofMor1 R) (RoofMor1Is R)) R (RoofMor2 (InvRoofFromMorInSom (RoofMor1 R) (RoofMor1Is R)))). @compose loc_precategory x y z (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2) = (RoofEqclassFromRoof (roof_comp R1 R2)). apply (pr2 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))). - apply RoofEqclassFromRoofIn. - apply RoofEqclassFromRoofIn. (RoofEqclassFromRoof R1) = (RoofEqclassFromRoof R2). use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R2))). + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof R1))). * exact (RoofEqclassFromRoofIn R1). + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof R2))). * exact (RoofEqclassFromRoofIn R2). use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R1))). + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof R2))). * exact (RoofEqclassFromRoofIn R2). + use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R1))). * exact (RoofEqclassFromRoofIn R1). (RoofEqclassFromRoof (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))) (RoofEqclassFromRoof (MorToRoof (RoofMor1 f1))) = (RoofEqclassFromRoof (IdRoof x)). set (R1 := (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))). set (tmp := pr2 (pr1 (roof_comp_iscontr x f1 x (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))). - exact (RoofEqclassFromRoof (roof_comp R1 R2)). + apply RoofEqclassFromRoofIn. + apply RoofEqclassFromRoofIn. RoofEqclassFromRoof R = RoofEqclassFromRoof (roof_comp (InvRoofFromMorInSom (RoofMor1 R) (RoofMor1Is R)) (MorToRoof (RoofMor2 R))). use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R))). - apply RoofEqclassFromRoofIn. apply RoofEqclassFromRoofIn. D hsD F H' x z (RoofEqclassFromRoof (roof_comp R1' R2')))) (roof_comp R1' R2') (RoofEqclassFromRoofIn (roof_comp R1' R2'))). use (pathscomp0 (MorMap_iscontr_eq D hsD F H' a b (RoofEqclassFromRoof (MorToRoof f)) (MorToRoof f) (RoofEqclassFromRoofIn _))). H' a b (RoofEqclassFromRoof f1))) f1 (RoofEqclassFromRoofIn f1)))). rewrite <- (RoofEqclassCompToRoofComp (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1)) (RoofEqclassFromRoof (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))) (RoofEqclassFromRoof (MorToRoof (RoofMor2 f1))))). (RoofEqclassFromRoof (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))) (RoofEqclassFromRoof (MorToRoof (RoofMor1 f1)))). - exact (RoofEqclassFromRoof (InvRoofFromMorInSom f s)). + set (sqr := isLocClassSqr2 iLC (InvRoofFromMorInSom f s) (MorToRoof f) y (RoofMor1 (InvRoofFromMorInSom f s)) (RoofMor1Is (InvRoofFromMorInSom f s)) + set (sqr := isLocClassSqr2 iLC (MorToRoof f) (InvRoofFromMorInSom f s) x (RoofMor2 (InvRoofFromMorInSom f s))).