proposition: Lemma roof_post_comp {x y z : ob C} (R1 : Roof x y) (R2 R3 : Roof y z) (e : (make_eqrel (RoofHrel y z) (RoofEqrel y z)) R2 R3) : (make_eqrel (RoofHrel x z) (RoofEqrel x z)) (roof_comp R1 R2) (roof_comp R1 R3).
proof: Proof. use (squash_to_prop e). apply propproperty. intros T. clear e. set (T' := RoofTopToCoroof T). induction T' as [CR eq]. intros P X. apply X. clear X P. set (R4 := roof_comp R1 R2). set (R5 := roof_comp R1 R3). unfold roof_comp in R4. unfold roof_comp in R5. set (sqr4 := isLocClassSqr2 iLC R2 R1 y (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R1)). set (sqr5 := isLocClassSqr2 iLC R3 R1 y (RoofMor1 R3) (RoofMor1Is R3) (RoofMor2 R1)). fold sqr4 in R4. fold sqr5 in R5. set (sqr6 := isLocClassSqr2 iLC R5 R4 R1 (LocSqr2Mor2 sqr5) (LocSqr2Mor2Is sqr5) (LocSqr2Mor2 sqr4)). assert (H : LocSqr2Mor1 sqr6 · LocSqr2Mor1 sqr5 · RoofMor2 R3 · CoroofMor2 CR = LocSqr2Mor2 sqr6 · LocSqr2Mor1 sqr4 · RoofMor2 R2 · CoroofMor2 CR). { rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- (dirprod_pr1 eq). rewrite <- (dirprod_pr2 eq). rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite <- (assoc _ (LocSqr2Mor1 sqr4)). rewrite (LocSqr2Comm sqr4). rewrite <- (assoc _ (LocSqr2Mor1 sqr5)). rewrite (LocSqr2Comm sqr5). rewrite assoc. rewrite assoc. apply cancel_postcomposition. apply cancel_postcomposition. apply (LocSqr2Comm sqr6). } set (PostS := isLocClassPost iLC _ _ _ (LocSqr2Mor1 sqr6 · LocSqr2Mor1 sqr5 · RoofMor2 R3) (LocSqr2Mor2 sqr6 · LocSqr2Mor1 sqr4 · RoofMor2 R2) (CoroofMor2 CR) (CoroofMor2Is CR) H). use make_RoofTop. - exact PostS. - exact (PostSwitchMor PostS · LocSqr2Mor2 sqr6). - exact (PostSwitchMor PostS · LocSqr2Mor1 sqr6). - use (isLocClassComp iLC). + use (isLocClassComp iLC). * exact (PostSwitchMorIs PostS). * exact (LocSqr2Mor2Is sqr6). + exact (RoofMor1Is R4). - cbn. rewrite assoc. rewrite assoc. apply cancel_postcomposition. set (tmp := ! (LocSqr2Comm sqr6)). apply (maponpaths (λ f : _, PostSwitchMor PostS · f)) in tmp. rewrite assoc in tmp. rewrite assoc in tmp. apply tmp. - cbn. apply pathsinv0. rewrite assoc. rewrite assoc. set (tmp := PostSwitchEq PostS). rewrite assoc in tmp. rewrite assoc in tmp. rewrite assoc in tmp. rewrite assoc in tmp. apply tmp. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors