Library UniMath.CategoryTheory.LocalizingClass

Localizing class

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.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.Core.Functors.

Localizing class and localization of categories.

In this section we define localization of categories when the collection of morphisms forms so called localizing class. The axioms of localizing class S are the following

every identity morphism must be in the collection
if f and g are in S, then so is f · g
Suppose we morphisms s : X --> Y and f : Z --> Y such that s in in S. Then we can find a square, that is morphisms, s' : W --> Z and f' : W --> X, such that s' in in S and we have s' · f = f' · s.
Dual version of the previous. Suppose s : X --> Y and f : X --> Z such that s in in S. Then we can find a square, that is morphisms, s' : Z --> W and f' : Y --> W, such that s' is in S and we have s' · f = f' · s.
Suppose we have a morphism s : X --> Y contained in S and two morphisms f g : Y --> Z such that s · f = s · g. Then S contains a morphism s' such that f · s' = f · s'.
Dual of the above. Suppose we have a morphism s : Z --> W in S and two morphisms f g : Y --> Z such that f · s = g · s. Then we can find a morphism s' in S such that s' · f = s' · g.

Section def_roofs.

  Variable C : precategory.
  Hypothesis hs : has_homsets C.

  Definition SubsetsOfMors : UU := ∏ (x y : ob C ), hsubtype (make_hSet (C ⟦x , y ⟧) (hs x y)).

Localizing classes

Identities and compositions are in the subset of morphisms

  Definition isLocalizingClass1 (SOM : SubsetsOfMors) : UU :=
    (∏ (x : ob C ), SOM x x (identity x))
      × (∏ (x y z : ob C) (f : x --> y) (e1 : SOM x y f) (g : y --> z) (e2 : SOM y z g ),
         SOM x z (f · g)).

  Definition isLocClassIs {SOM : SubsetsOfMors} (H : isLocalizingClass1 SOM) :
    ∏ (x : ob C ), SOM x x (identity x) := pr1 H.

  Definition isLocClassComp {SOM : SubsetsOfMors} (H : isLocalizingClass1 SOM) :
    ∏ (x y z : ob C) (f : x --> y) (e1 : SOM x y f) (g : y --> z) (e2 : SOM y z g ),
    SOM x z (f · g) := pr2 H.

Squares

  Definition LocSqr1 (SOM : SubsetsOfMors) {x y z : ob C} (s : x --> y) (e1 : SOM x y s)
             (f : x --> z) : UU :=
    ∑ D : (∑ (w : ob C ), C ⟦y , w ⟧ × C ⟦z , w ⟧),
          (SOM z (pr1 D) (dirprod_pr2 (pr2 D)))
            × (s · (dirprod_pr1 (pr2 D)) = f · (dirprod_pr2 (pr2 D))).

  Definition LocSqr1Ob {SOM : SubsetsOfMors} {x y z : ob C} {s : x --> y} {e1 : SOM x y s}
             {f : x --> z} (LS1 : LocSqr1 SOM s e1 f) : ob C := pr1 (pr1 LS1).
  Coercion LocSqr1Ob : LocSqr1 >-> ob.

  Definition LocSqr1Mor1 {SOM : SubsetsOfMors} {x y z : ob C} {s : x --> y} {e1 : SOM x y s}
             {f : x --> z} (LS1 : LocSqr1 SOM s e1 f) : C ⟦y , LS1 ⟧ := dirprod_pr1 (pr2 (pr1 LS1)).

  Definition LocSqr1Mor2 {SOM : SubsetsOfMors} {x y z : ob C} {s : x --> y} {e1 : SOM x y s}
             {f : x --> z} (LS1 : LocSqr1 SOM s e1 f) : C ⟦z , LS1 ⟧ := dirprod_pr2 (pr2 (pr1 LS1)).

  Definition LocSqr1Mor2Is {SOM : SubsetsOfMors} {x y z : ob C} {s : x --> y} {e1 : SOM x y s}
             {f : x --> z} (LS1 : LocSqr1 SOM s e1 f) : SOM z LS1 (LocSqr1Mor2 LS1) :=
    pr1 (pr2 LS1).

  Definition LocSqr1Comm {SOM : SubsetsOfMors} {x y z : ob C} {s : x --> y} {e1 : SOM x y s}
             {f : x --> z} (LS1 : LocSqr1 SOM s e1 f) :
    s · (LocSqr1Mor1 LS1 ) = f · (LocSqr1Mor2 LS1 ) := dirprod_pr2 (pr2 LS1).

  Definition LocSqr2 (SOM : SubsetsOfMors) {y z w : ob C} (s : y --> w) (e1 : SOM y w s)
             (f : z --> w) : UU :=
    ∑ D : (∑ (x : ob C ), C ⟦x , y ⟧ × C ⟦x , z ⟧),
          (SOM (pr1 D) z (dirprod_pr2 (pr2 D)))
            × ((dirprod_pr1 (pr2 D)) · s = (dirprod_pr2 (pr2 D)) · f ).

  Definition LocSqr2Ob {SOM : SubsetsOfMors} {y z w : ob C} {s : y --> w} {e1 : SOM y w s}
             {f : z --> w} (LS2 : LocSqr2 SOM s e1 f) : ob C := pr1 (pr1 LS2).
  Coercion LocSqr2Ob : LocSqr2 >-> ob.

  Definition LocSqr2Mor1 {SOM : SubsetsOfMors} {y z w : ob C} {s : y --> w} {e1 : SOM y w s}
             {f : z --> w} (LS2 : LocSqr2 SOM s e1 f) : C ⟦LS2 , y ⟧ := dirprod_pr1 (pr2 (pr1 LS2)).

  Definition LocSqr2Mor2 {SOM : SubsetsOfMors} {y z w : ob C} {s : y --> w} {e1 : SOM y w s}
             {f : z --> w} (LS2 : LocSqr2 SOM s e1 f) : C ⟦LS2 , z ⟧ := dirprod_pr2 (pr2 (pr1 LS2)).

  Definition LocSqr2Mor2Is {SOM : SubsetsOfMors} {y z w : ob C} {s : y --> w} {e1 : SOM y w s}
             {f : z --> w} (LS2 : LocSqr2 SOM s e1 f) : SOM LS2 z (LocSqr2Mor2 LS2) :=
    dirprod_pr1 (pr2 LS2).

  Definition LocSqr2Comm {SOM : SubsetsOfMors} {y z w : ob C} {s : y --> w} {e1 : SOM y w s}
             {f : z --> w} (LS2 : LocSqr2 SOM s e1 f) :
    (LocSqr2Mor1 LS2 ) · s = (LocSqr2Mor2 LS2 ) · f := dirprod_pr2 (pr2 LS2).

Completion to squares

  Definition isLocalizingClass2 (SOM : SubsetsOfMors) : UU :=
    (∏ (x y z : ob C) (s : x --> y) (e1 : SOM x y s) (f : x --> z ), (LocSqr1 SOM s e1 f ))
      × (∏ (y z w : ob C) (s : y --> w) (e1 : SOM y w s) (f : z --> w ), (LocSqr2 SOM s e1 f )).

  Definition isLocClassSqr1 {SOM : SubsetsOfMors} (H : isLocalizingClass2 SOM) :
    ∏ (x y z : ob C) (s : x --> y) (e1 : SOM x y s) (f : x --> z ), LocSqr1 SOM s e1 f :=
    dirprod_pr1 H.

  Definition isLocClassSqr2 {SOM : SubsetsOfMors} (H : isLocalizingClass2 SOM) :
    ∏ (y z w : ob C) (s : y --> w) (e1 : SOM y w s) (f : z --> w ), LocSqr2 SOM s e1 f :=
    dirprod_pr2 H.

Pre- and post switch

  Definition PreSwitch (SOM : SubsetsOfMors) {x y z : ob C} (s : x --> y) (e : SOM x y s)
             (f g : y --> z) (H : s · f = s · g) : UU :=
    ∑ D : (∑ (w : ob C ), C ⟦z , w ⟧), (SOM z (pr1 D) (pr2 D)) × (f · (pr2 D ) = g · (pr2 D )).

  Definition PreSwitchOb {SOM : SubsetsOfMors} {x y z : ob C} {s : x --> y} {e : SOM x y s}
             {f g : y --> z} {H : s · f = s · g} (PreS : PreSwitch SOM s e f g H) : ob C :=
    pr1 (pr1 PreS).
  Coercion PreSwitchOb : PreSwitch >-> ob.

  Definition PreSwitchMor {SOM : SubsetsOfMors} {x y z : ob C} {s : x --> y} {e : SOM x y s}
             {f g : y --> z} {H : s · f = s · g} (PreS : PreSwitch SOM s e f g H) :
    C ⟦z , PreS ⟧ := pr2 (pr1 PreS).

  Definition PreSwitchMorIs {SOM : SubsetsOfMors} {x y z : ob C} {s : x --> y} {e : SOM x y s}
             {f g : y --> z} {H : s · f = s · g} (PreS : PreSwitch SOM s e f g H) :
    SOM z PreS (PreSwitchMor PreS) := dirprod_pr1 (pr2 PreS).

  Definition PreSwitchEq {SOM : SubsetsOfMors} {x y z : ob C} {s : x --> y} {e : SOM x y s}
             {f g : y --> z} {H : s · f = s · g} (PreS : PreSwitch SOM s e f g H) :
    f · (PreSwitchMor PreS ) = g · (PreSwitchMor PreS ) := dirprod_pr2 (pr2 PreS).

Post switch

  Definition PostSwitch (SOM : SubsetsOfMors) {y z w : ob C} (f g : y --> z) (s : z --> w)
             (e : SOM z w s) (H : f · s = g · s) : UU :=
    ∑ D : (∑ (x : ob C ), C ⟦x , y ⟧), (SOM (pr1 D) y (pr2 D)) × ((pr2 D ) · f = (pr2 D ) · g ).

  Definition PostSwitchOb {SOM : SubsetsOfMors} {y z w : ob C} {f g : y --> z} {s : z --> w}
             {e : SOM z w s} {H : f · s = g · s} (PostS : PostSwitch SOM f g s e H) : ob C :=
    pr1 (pr1 PostS).
  Coercion PostSwitchOb : PostSwitch >-> ob.

  Definition PostSwitchMor {SOM : SubsetsOfMors} {y z w : ob C} {f g : y --> z} {s : z --> w}
             {e : SOM z w s} {H : f · s = g · s} (PostS : PostSwitch SOM f g s e H) :
    C ⟦PostS , y ⟧ := pr2 (pr1 PostS).

  Definition PostSwitchMorIs {SOM : SubsetsOfMors} {y z w : ob C} {f g : y --> z} {s : z --> w}
             {e : SOM z w s} {H : f · s = g · s} (PostS : PostSwitch SOM f g s e H) :
    SOM PostS y (PostSwitchMor PostS) := dirprod_pr1 (pr2 PostS).

  Definition PostSwitchEq {SOM : SubsetsOfMors} {y z w : ob C} {f g : y --> z} {s : z --> w}
             {e : SOM z w s} {H : f · s = g · s} (PostS : PostSwitch SOM f g s e H) :
    (PostSwitchMor PostS ) · f = (PostSwitchMor PostS ) · g := dirprod_pr2 (pr2 PostS).

Pre- and postcomposition with morphisms in the subset

  Definition isLocalizingClass3 (SOM : SubsetsOfMors) : UU :=
    (∏ (x y z : ob C) (s : x --> y) (e : SOM x y s) (f g : y --> z) (H : s · f = s · g ),
     PreSwitch SOM s e f g H )
      × (∏ (y z w : ob C) (f g : y --> z) (s : z --> w) (e : SOM z w s) (H : f · s = g · s ),
         PostSwitch SOM f g s e H ).

  Definition isLocClassPre {SOM : SubsetsOfMors} (H : isLocalizingClass3 SOM) :
    ∏ (x y z : ob C) (s : x --> y) (e : SOM x y s) (f g : y --> z) (H : s · f = s · g ),
    PreSwitch SOM s e f g H := dirprod_pr1 H.

  Definition isLocClassPost {SOM : SubsetsOfMors} (H : isLocalizingClass3 SOM) :
    ∏ (y z w : ob C) (f g : y --> z) (s : z --> w) (e : SOM z w s) (H : f · s = g · s ),
    PostSwitch SOM f g s e H := dirprod_pr2 H.

Localizing class

  Definition isLocalizingClass (SOM : SubsetsOfMors) : UU :=
    (isLocalizingClass1 SOM ) × (isLocalizingClass2 SOM ) × (isLocalizingClass3 SOM ).

  Definition isLocalizingClass_isLocalizingClass1 {SOM : SubsetsOfMors}
             (H : isLocalizingClass SOM) : isLocalizingClass1 SOM := dirprod_pr1 H.
  Coercion isLocalizingClass_isLocalizingClass1 : isLocalizingClass >-> isLocalizingClass1.

  Definition isLocalizingClass_isLocalizingClass2 {SOM : SubsetsOfMors}
             (H : isLocalizingClass SOM) : isLocalizingClass2 SOM :=
    dirprod_pr1 (dirprod_pr2 H).
  Coercion isLocalizingClass_isLocalizingClass2 : isLocalizingClass >-> isLocalizingClass2.

  Definition isLocalizingClass_isLocalizingClass3 {SOM : SubsetsOfMors}
             (H : isLocalizingClass SOM) : isLocalizingClass3 SOM :=
    dirprod_pr2 (dirprod_pr2 H).
  Coercion isLocalizingClass_isLocalizingClass3 : isLocalizingClass >-> isLocalizingClass3.

Collection of morphisms in C

Variable SOM : SubsetsOfMors.

The above collection satisfies the conditions of localizin class. See the comment on top of this section.

Hypothesis iLC : isLocalizingClass SOM.

Roofs

  Definition Roof (x y : ob C) : UU :=
    ∑ D : (∑ z : ob C , C ⟦z , x ⟧ × C ⟦z , y ⟧), (SOM (pr1 D) x (dirprod_pr1 (pr2 D))).

  Definition make_Roof (x y z : ob C) (s : z --> x) (f : z --> y) (e : SOM z x s) : Roof x y :=
    tpair _ (tpair _ z (s ,,f)) e.

  Definition RoofOb {x y : ob C} (R : Roof x y) : ob C := pr1 (pr1 R).
  Coercion RoofOb : Roof >-> ob.

  Definition RoofMor1 {x y : ob C} (R : Roof x y) : C ⟦R , x ⟧ := dirprod_pr1 (pr2 (pr1 R)).

  Definition RoofMor1Is {x y : ob C} (R : Roof x y) : SOM R x (RoofMor1 R) := pr2 R.

  Definition RoofMor2 {x y : ob C} (R : Roof x y) : C ⟦R , y ⟧ := dirprod_pr2 (pr2 (pr1 R)).

Coroofs

  Definition Coroof (x y : ob C) : UU :=
    ∑ D : (∑ z : ob C , C ⟦x , z ⟧ × C ⟦y , z ⟧), (SOM y (pr1 D) (dirprod_pr2 (pr2 D))).

  Definition make_Coroof (x y z : ob C) (f : x --> z) (s : y --> z) (e : SOM y z s) : Coroof x y :=
    tpair _ (tpair _ z (f ,,s)) e.

  Definition CoroofOb {x y : ob C} (CR : Coroof x y) : ob C := pr1 (pr1 CR).
  Coercion CoroofOb : Coroof >-> ob.

  Definition CoroofMor1 {x y : ob C} (CR : Coroof x y) : C ⟦x , CR ⟧ := dirprod_pr1 (pr2 (pr1 CR)).

  Definition CoroofMor2 {x y : ob C} (CR : Coroof x y) : C ⟦y , CR ⟧ := dirprod_pr2 (pr2 (pr1 CR)).

  Definition CoroofMor2Is {x y : ob C} (CR : Coroof x y) : SOM y CR (CoroofMor2 CR) := pr2 CR.

  Definition RoofToCoroof {x y : ob C} (R : Roof x y) : Coroof x y.
  Proof.
    set (sqr := isLocClassSqr1 iLC _ _ _ (RoofMor1 R) (RoofMor1Is R) (RoofMor2 R)).
    use make_Coroof.
    - exact sqr.
    - exact (LocSqr1Mor1 sqr).
    - exact (LocSqr1Mor2 sqr).
    - exact (LocSqr1Mor2Is sqr).
  Defined.

RoofTop

These are used to define an equivalence relation between roofs

  Definition RoofTop {x y : ob C} (R1 R2 : Roof x y) : UU :=
    ∑ D : (∑ w : ob C , C ⟦w , R1 ⟧ × C ⟦w , R2 ⟧),
          (SOM (pr1 D) x ((dirprod_pr1 (pr2 D)) · (RoofMor1 R1 )))
            × ((dirprod_pr1 (pr2 D)) · (RoofMor1 R1 ) = (dirprod_pr2 (pr2 D)) · (RoofMor1 R2 ))
            × ((dirprod_pr1 (pr2 D)) · (RoofMor2 R1 ) = (dirprod_pr2 (pr2 D)) · (RoofMor2 R2 )).

  Definition make_RoofTop {x y : ob C} {R1 R2 : Roof x y} (w : ob C) (s : w --> R1) (f : w --> R2)
             (e : SOM w x (s · RoofMor1 R1))
             (H1 : s · (RoofMor1 R1 ) = f · (RoofMor1 R2 ))
             (H2 : s · (RoofMor2 R1 ) = f · (RoofMor2 R2 )) : RoofTop R1 R2 :=
    tpair _ (tpair _ w (s ,,f)) (e ,,(H1 ,,H2 )).

  Definition RoofTopOb {x y : ob C} {R1 R2 : Roof x y} (T : RoofTop R1 R2) : ob C := pr1 (pr1 T).
  Coercion RoofTopOb : RoofTop >-> ob.

  Definition RoofTopMor1 {x y : ob C} {R1 R2 : Roof x y} (T : RoofTop R1 R2) : C ⟦T , R1 ⟧ :=
    dirprod_pr1 (pr2 (pr1 T)).

  Definition RoofTopMor1Is {x y : ob C} {R1 R2 : Roof x y} (T : RoofTop R1 R2) :
    (SOM T x ((RoofTopMor1 T ) · (RoofMor1 R1 ))) := (dirprod_pr1 (pr2 T)).

  Definition RoofTopMor2 {x y : ob C} {R1 R2 : Roof x y} (T : RoofTop R1 R2) : C ⟦T , R2 ⟧ :=
    dirprod_pr2 (pr2 (pr1 T)).

  Definition RoofTopEq1 {x y : ob C} {R1 R2 : Roof x y} (T : RoofTop R1 R2) :
    (RoofTopMor1 T ) · (RoofMor1 R1 ) = (RoofTopMor2 T ) · (RoofMor1 R2 ) :=
    dirprod_pr1 (dirprod_pr2 (pr2 T)).

  Definition RoofTopEq2 {x y : ob C} {R1 R2 : Roof x y} (T : RoofTop R1 R2) :
    (RoofTopMor1 T ) · (RoofMor2 R1 ) = (RoofTopMor2 T ) · (RoofMor2 R2 ) :=
    dirprod_pr2 (dirprod_pr2 (pr2 T)).

We define an equivalence relation between the roofs

  Definition RoofHrel' {x y : ob C} (R1 R2 : Roof x y) : hProp := ishinh (RoofTop R1 R2).

  Definition RoofHrel (x y : ob C) : hrel (Roof x y) :=
    (λ R1 : Roof x y , λ R2 : Roof x y , RoofHrel' R1 R2).

  Lemma RoofEqrel (x y : ob C) : iseqrel (RoofHrel x y).
  Proof.
    use iseqrelconstr.
    - intros R1 R2 R3 T1' T2'.
      use (squash_to_prop T1'). apply isapropishinh. intros T1. clear T1'.
      use (squash_to_prop T2'). apply isapropishinh. intros T2. clear T2'.
      set (tmp := isLocClassSqr2 iLC T2 T1 x (RoofTopMor1 T2 · RoofMor1 R2) (RoofTopMor1Is T2)
                                 (RoofTopMor2 T1 · RoofMor1 R2)).
      induction tmp as [D1 D2]. induction D1 as [w m]. induction m as [m1 m2].
      induction D2 as [D1 D2]. cbn in D1, D2. repeat rewrite assoc in D2.
      set (tmp := isLocClassPost iLC w R2 x (m1 · RoofTopMor1 T2) (m2 · RoofTopMor2 T1)
                                 (RoofMor1 R2) (RoofMor1Is R2) D2).
      induction tmp as [t p].
      intros P X. apply X. clear X P.
      use make_RoofTop.
      + exact (pr1 t).
      + exact ((pr2 t) · m2 · RoofTopMor1 T1).
      + exact ((pr2 t) · m1 · RoofTopMor2 T2).
      + repeat rewrite <- assoc. use (isLocClassComp iLC).
        × exact (dirprod_pr1 p).
        × use (isLocClassComp iLC).
          -- exact D1.
          -- exact (RoofTopMor1Is T1).
      + induction p as [p1 p2]. repeat rewrite assoc in p2.
        set (tmp := RoofTopEq1 T2). repeat rewrite <- assoc. rewrite <- tmp. clear tmp.
        repeat rewrite assoc. repeat rewrite <- (assoc (pr2 t)). rewrite D2.
        repeat rewrite <- assoc.
        apply cancel_precomposition. apply cancel_precomposition.
        exact (RoofTopEq1 T1).
      + induction p as [p1 p2]. repeat rewrite assoc in p2.
        set (tmp := RoofTopEq2 T2). repeat rewrite <- assoc. rewrite <- tmp. clear tmp.
        repeat rewrite assoc. rewrite p2. repeat rewrite <- assoc.
        apply cancel_precomposition. apply cancel_precomposition.
        exact (RoofTopEq2 T1).
    - intros R1.
      intros P X. apply X. clear X P.
      use make_RoofTop.
      + exact R1.
      + exact (identity R1).
      + exact (identity R1).
      + rewrite id_left. exact (RoofMor1Is R1).
      + apply idpath.
      + apply idpath.
    - intros R1 R2 T'.
      use (squash_to_prop T'). apply isapropishinh. intros T. clear T'.
      intros P X. apply X. clear X P.
      use make_RoofTop.
      + exact T.
      + exact (RoofTopMor2 T).
      + exact (RoofTopMor1 T).
      + rewrite <- (RoofTopEq1 T). exact (RoofTopMor1Is T).
      + exact (! (RoofTopEq1 T)).
      + exact (! (RoofTopEq2 T)).
  Qed.

We are interested in the equivalence classes of roofs.

  Definition RoofEqclass (x y : ob C) : UU :=
    ∑ A : hsubtype (Roof x y), iseqclass (make_eqrel _ (RoofEqrel x y)) A.

  Lemma isasetRoofEqclass (x y : ob C) : isaset (RoofEqclass x y).
  Proof.
    apply isaset_total2.
    - apply isasethsubtype.
    - intros x0.
      apply isasetaprop.
      apply isapropiseqclass.
  Defined.

  Definition make_RoofEqclass {x y : ob C} (A : hsubtype (Roof x y))
             (H : iseqclass (make_eqrel _ (RoofEqrel x y)) A) : RoofEqclass x y := tpair _ A H.

  Definition RoofEqclassIn {x y : ob C} (RE : RoofEqclass x y) : hsubtype (Roof x y) := pr1 RE.

  Definition RoofEqclassIs {x y : ob C} (RE : RoofEqclass x y) :
    iseqclass (make_eqrel _ (RoofEqrel x y)) (RoofEqclassIn RE) := pr2 RE.

  Definition RoofEqclassEq {x y : ob C} (RE1 RE2 : RoofEqclass x y)
             (H1 : ∏ (R : Roof x y) (H : (pr1 RE1) R ), (pr1 RE2) R)
             (H2 : ∏ (R : Roof x y) (H : (pr1 RE2) R ), (pr1 RE1) R) : RE1 = RE2.
  Proof.
    use total2_paths_f.
    - use funextfun. intros g.
      apply hPropUnivalence.
      + apply H1.
      + apply H2.
    - apply proofirrelevance. apply isapropiseqclass.
  Qed.

  Definition RoofEqclassDisjoint {x y : ob C} (RE1 RE2 : RoofEqclass x y)
             (R1 R2 : Roof x y) (H1 : RoofEqclassIn RE1 R1) (H2 : RoofEqclassIn RE2 R2)
             (H : (make_eqrel _ (RoofEqrel x y)) R1 R2) : RE1 = RE2.
  Proof.
    use RoofEqclassEq.
    - intros R H'.
      set (tmp := eqax1 (pr2 RE1) R1 R2 H H1).
      set (tmp' := eqax2 (pr2 RE1) R R2 H' tmp).
      apply eqrelsymm in tmp'.
      apply (eqax1 (pr2 RE2) R2 R tmp' H2).
    - intros R H'.
      apply eqrelsymm in H.
      set (tmp := eqax1 (pr2 RE2) R2 R1 H H2).
      set (tmp' := eqax2 (pr2 RE2) R1 R tmp H').
      apply (eqax1 (pr2 RE1) R1 R tmp' H1).
  Qed.

  Definition RoofEqclassFromRoof {x y : ob C} (R : Roof x y) : RoofEqclass x y.
  Proof.
    use tpair.
    - exact (λ RR : Roof x y, (make_eqrel _ (RoofEqrel x y)) RR R).
    - use tpair.
      + intros P X. apply X. clear X P.
        use tpair.
        × exact R.
        × apply eqrelrefl.
      + split.
        × intros x1 x2 X X0.
          use eqreltrans.
          -- exact x1.
          -- apply eqrelsymm. apply X.
          -- apply X0.
        × intros x1 x2 X X0.
          use eqreltrans.
          -- exact R.
          -- exact X.
          -- apply eqrelsymm. apply X0.
  Defined.

  Definition RoofEqclassFromRoofIn {x y : ob C} (R : Roof x y) :
    RoofEqclassIn (RoofEqclassFromRoof R) R.
  Proof.
    intros P X. apply X. clear X P.
    use make_RoofTop.
    - exact R.
    - exact (identity R).
    - exact (identity R).
    - use (isLocClassComp iLC).
      + apply (isLocClassIs iLC).
      + apply (RoofMor1Is R).
    - apply idpath.
    - apply idpath.
  Qed.

  Definition RoofEqclassEqRoof {x y : ob C} (RE : RoofEqclass x y)
             (R : Roof x y) (HR : RoofEqclassIn RE R) : RE = RoofEqclassFromRoof R.
  Proof.
    use RoofEqclassEq.
    - intros R0 HR0.
      use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R))).
      + exact R.
      + use (eqax2 (RoofEqclassIs RE)).
        × exact HR.
        × exact HR0.
      + apply RoofEqclassFromRoofIn.
    - intros R0 HR0.
      use (eqax1 (RoofEqclassIs RE)).
      + exact R.
      + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof R))).
        × apply RoofEqclassFromRoofIn.
        × exact HR0.
      + exact HR.
  Qed.

  Definition RoofEqClassIn {x y : ob C} (R1 R2 R3 : Roof x y)
             (H1 : RoofEqclassIn (RoofEqclassFromRoof R1) R2)
             (H2 : (make_eqrel _ (RoofEqrel x y)) R2 R3) :
    RoofEqclassIn (RoofEqclassFromRoof R1) R3.
  Proof.
    exact (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R1)) R2 R3 H2 H1).
  Qed.

  Definition RoofEqClassIn2 {x y : ob C} (RE : RoofEqclass x y) (R2 R3 : Roof x y)
             (H1 : RoofEqclassIn RE R2) (H2 : (make_eqrel _ (RoofEqrel x y)) R2 R3) :
    RoofEqclassIn RE R3.
  Proof.
    use (squash_to_prop (pr1 (RoofEqclassIs RE))). apply propproperty. intros RE1.
    induction RE1 as [RE1 RE2].
    apply (eqax1 (RoofEqclassIs RE) RE1 R3).
    - use eqreltrans.
      + exact R2.
      + apply (eqax2 (RoofEqclassIs RE) RE1 R2 RE2 H1).
      + apply H2.
    - apply RE2.
  Qed.

  Definition roof_comp {x y z : ob C} (R1 : Roof x y) (R2 : Roof y z) : Roof x z.
  Proof.
    set (LS2 := isLocClassSqr2 iLC R2 R1 y (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R1)).
    use make_Roof.
    - exact LS2.
    - exact ((LocSqr2Mor2 LS2) · (RoofMor1 R1)).
    - exact ((LocSqr2Mor1 LS2) · (RoofMor2 R2)).
    - use (isLocClassComp iLC).
      + exact (LocSqr2Mor2Is LS2).
      + exact (RoofMor1Is R1).
  Defined.

Composition of roofs

Construct a "commutative coroof" from RoofTop

  Definition RoofTopToCoroof {x y : ob C} {R1 R2 : Roof x y} (T : RoofTop R1 R2) :
    ∑ CR : Coroof x y , (RoofMor1 R1 · CoroofMor1 CR = RoofMor2 R1 · CoroofMor2 CR )
                         × (RoofMor1 R2 · CoroofMor1 CR = RoofMor2 R2 · CoroofMor2 CR ).
  Proof.
    set (sqr1 := isLocClassSqr1 iLC _ _ _ (RoofMor1 R1) (RoofMor1Is R1) (RoofMor2 R1)).
    set (sqr2 := isLocClassSqr1 iLC _ _ _ (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R2)).
    set (sqr3 := isLocClassSqr1 iLC _ _ _ (LocSqr1Mor2 sqr1) (LocSqr1Mor2Is sqr1)
                                (LocSqr1Mor2 sqr2)).
    set (mor1 := RoofTopMor1 T · RoofMor1 R1 · LocSqr1Mor1 sqr1 · LocSqr1Mor1 sqr3).
    set (mor2 := RoofTopMor1 T · RoofMor1 R1 · LocSqr1Mor1 sqr2 · LocSqr1Mor2 sqr3).

    assert (H : RoofTopMor1 T · RoofMor1 R1 · (LocSqr1Mor1 sqr1 · LocSqr1Mor1 sqr3)
                = RoofTopMor1 T · RoofMor1 R1 · (LocSqr1Mor1 sqr2 · LocSqr1Mor2 sqr3)).
    {
      set (tmp1 := LocSqr1Comm sqr1).
      set (tmp2 := LocSqr1Comm sqr2).
      set (tmp3 := LocSqr1Comm sqr3).
      rewrite assoc. rewrite <- (assoc _ (RoofMor1 R1)). rewrite tmp1.
      rewrite assoc. rewrite <- assoc. rewrite tmp3.
      rewrite assoc. rewrite (RoofTopEq2 T).
      rewrite <- (assoc _ (RoofMor2 R2)). rewrite <- tmp2.
      rewrite assoc. rewrite (RoofTopEq1 T). rewrite assoc.
      apply idpath.
    }
    set (PreS := isLocClassPre iLC _ _ _ (RoofTopMor1 T · RoofMor1 R1) (RoofTopMor1Is T)
                               (LocSqr1Mor1 sqr1 · LocSqr1Mor1 sqr3)
                               (LocSqr1Mor1 sqr2 · LocSqr1Mor2 sqr3) H).
    use tpair.
    - use make_Coroof.
      + exact PreS.
      + exact (LocSqr1Mor1 sqr1 · LocSqr1Mor1 sqr3 · PreSwitchMor PreS).
      + exact (LocSqr1Mor2 sqr2 · LocSqr1Mor2 sqr3 · PreSwitchMor PreS).
      + use (isLocClassComp iLC).
        × use (isLocClassComp iLC).
          -- exact (LocSqr1Mor2Is sqr2).
          -- exact (LocSqr1Mor2Is sqr3).
        × exact (PreSwitchMorIs PreS).
    - cbn. split.
      + rewrite <- (LocSqr1Comm sqr3).
        rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc.
        apply cancel_postcomposition. apply cancel_postcomposition.
        apply (LocSqr1Comm sqr1).
      + rewrite (PreSwitchEq PreS).
        rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc.
        apply cancel_postcomposition. apply cancel_postcomposition.
        apply (LocSqr1Comm sqr2).
  Defined.
  Opaque RoofTopToCoroof.

Precomposition with equivalent roofs yield equivalent roofs.

  Lemma roof_pre_comp {x y z : ob C} (R1 R2 : Roof x y)
        (e : (make_eqrel (RoofHrel x y) (RoofEqrel x y)) R1 R2) (R3 : Roof y z) :
    (make_eqrel (RoofHrel x z) (RoofEqrel x z)) (roof_comp R1 R3) (roof_comp R2 R3).
  Proof.
    use (squash_to_prop e). apply propproperty. intros T.
    set (T' := RoofTopToCoroof T). induction T' as [CR eq].
    intros P X. apply X. clear X P.
    set (R4 := roof_comp R1 R3). set (R5 := roof_comp R2 R3).
    unfold roof_comp in R4. unfold roof_comp in R5.
    set (sqr4 := isLocClassSqr2 iLC R3 R1 y (RoofMor1 R3) (RoofMor1Is R3) (RoofMor2 R1)).
    set (sqr5 := isLocClassSqr2 iLC R3 R2 y (RoofMor1 R3) (RoofMor1Is R3) (RoofMor2 R2)).
    fold sqr4 in R4. fold sqr5 in R5.
    set (sqr6 := isLocClassSqr2 iLC R5 R4 x (LocSqr2Mor2 sqr5 · RoofMor1 R2) (RoofMor1Is R5)
                                (LocSqr2Mor2 sqr4 · RoofMor1 R1)).
    assert (s : SOM R3 CR (RoofMor1 R3 · CoroofMor2 CR)).
    {
      use (isLocClassComp iLC).
      - exact (RoofMor1Is R3).
      - exact (CoroofMor2Is CR).
    }
    assert (H : LocSqr2Mor1 sqr6 · LocSqr2Mor1 sqr5 · (RoofMor1 R3 · CoroofMor2 CR) =
                LocSqr2Mor2 sqr6 · LocSqr2Mor1 sqr4 · (RoofMor1 R3 · CoroofMor2 CR)).
    {
      rewrite assoc. rewrite assoc.
      rewrite <- (assoc _ (LocSqr2Mor1 sqr5)). rewrite (LocSqr2Comm sqr5).
      rewrite <- (assoc _ (LocSqr2Mor1 sqr4)). rewrite (LocSqr2Comm sqr4).
      rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc.
      rewrite <- (dirprod_pr1 eq). rewrite <- (dirprod_pr2 eq).
      rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc.
      apply cancel_postcomposition.
      set (tmp := LocSqr2Comm sqr6). rewrite assoc in tmp. rewrite assoc in tmp.
      apply tmp.
    }
    set (PostS := isLocClassPost iLC _ _ _
                                 (LocSqr2Mor1 sqr6 · LocSqr2Mor1 sqr5)
                                 (LocSqr2Mor2 sqr6 · LocSqr2Mor1 sqr4)
                                 (RoofMor1 R3 · CoroofMor2 CR) s 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_precomposition.
      apply (! (LocSqr2Comm sqr6)).
    - cbn.
      rewrite assoc. rewrite assoc.
      set (tmp := ! (PostSwitchEq PostS)). rewrite assoc in tmp. rewrite assoc in tmp.
      apply (maponpaths (λ f : _, f · RoofMor2 R3)) in tmp.
      apply tmp.
  Qed.

Postcomposition with equivalent roofs yield equivalent roofs.

  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.
    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.

  Lemma roof_comp_iscontr (x y z : ob C) (e1 : RoofEqclass x y) (e2 : RoofEqclass y z) :
    iscontr (∑ e3 : RoofEqclass x z ,
                    ∏ (f : Roof x y) (s1 : (RoofEqclassIn e1) f)
                      (g : Roof y z) (s2 : (RoofEqclassIn e2) g ),
                    (RoofEqclassIn e3) (roof_comp f g)).
  Proof.
    induction e1 as [e1 e1eq]. induction e2 as [e2 e2eq].
    use (squash_to_prop (dirprod_pr1 e1eq)). apply isapropiscontr. intros R1.
    induction R1 as [R1 R1'].
    use (squash_to_prop (dirprod_pr1 e2eq)). apply isapropiscontr. intros R2.
    induction R2 as [R2 R2'].
    use tpair.
    - use tpair.
      + use make_RoofEqclass.
        × exact (λ RR : (Roof x z), (make_eqrel _ (RoofEqrel x z)) RR (roof_comp R1 R2)).
        × use iseqclassconstr.
          -- intros P X. apply X. clear X P.
             use tpair.
             ++ exact (roof_comp R1 R2).
             ++ use eqrelrefl.
          -- intros R3 R4 H1 H2. cbn beta in H2. cbn beta.
             use (squash_to_prop H1). apply propproperty. intros T1.
             use (squash_to_prop H2). apply propproperty. intros T2.
             apply eqrelsymm in H1.
             use eqreltrans.
             ++ exact R3.
             ++ exact H1.
             ++ exact H2.
          -- intros R3 R4 H1 H2. cbn beta in H1, H2.
             apply eqrelsymm in H2.
             use eqreltrans.
             ++ exact (roof_comp R1 R2).
             ++ exact H1.
             ++ exact H2.
      + cbn. intros R3 R3' R4 R4'.
        set (tmp1 := eqax2 e1eq R1 R3 R1' R3').
        set (tmp2 := eqax2 e2eq R2 R4 R2' R4').
        set (tmp_pre := roof_pre_comp R1 R3 tmp1 R4).
        set (tmp_post := roof_post_comp R1 R2 R4 tmp2).
        assert (X : (make_eqrel (RoofHrel x z) (RoofEqrel x z)) (roof_comp R3 R4) (roof_comp R1 R2)).
        {
          apply eqrelsymm.
          use eqreltrans.
          - exact (roof_comp R1 R4).
          - exact tmp_post.
          - exact tmp_pre.
        }
        exact X.
    - intros t.
      use total2_paths_f.
      + use RoofEqclassEq.
        × intros R HR. cbn.
          set (tmp1 := eqax2 (pr2 (pr1 t))). apply tmp1.
          -- exact HR.
          -- apply (pr2 t).
             ++ cbn. exact R1'.
             ++ cbn. exact R2'.
        × intros R HR. cbn in HR.
          set (tmp1 := eqax1 (pr2 (pr1 t))). apply (tmp1 (roof_comp R1 R2)).
          -- apply eqrelsymm. apply HR.
          -- apply (pr2 t).
             ++ cbn. exact R1'.
             ++ cbn. exact R2'.
      + apply proofirrelevance.
        apply impred_isaprop. intros t0.
        apply impred_isaprop. intros t1.
        apply impred_isaprop. intros t2.
        apply impred_isaprop. intros t3.
        apply impred_isaprop. intros t4.
        apply impred_isaprop. intros t5.
        apply propproperty.
  Qed.

  Local Lemma roof_comp_iscontr_in (x y z : ob C) (R1 : Roof x y) (R2 : Roof y z) :
    RoofEqclassIn (pr1 (pr1 (roof_comp_iscontr _ _ _ (RoofEqclassFromRoof R1)
                                               (RoofEqclassFromRoof R2))))
                  (roof_comp R1 R2).
  Proof.
    use (pr2 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))).
    - apply RoofEqclassFromRoofIn.
    - apply RoofEqclassFromRoofIn.
  Qed.

Definition of the localization

  Definition loc_precategory_ob_mor : precategory_ob_mor :=
    tpair (λ ob : UU , ob → ob → UU) (ob C) (λ x y : ob C , RoofEqclass x y).

  Definition IdRoof (x : ob C) : Roof x x.
  Proof.
    use make_Roof.
    - exact x.
    - exact (identity x).
    - exact (identity x).
    - exact (isLocClassIs iLC x).
  Defined.

  Lemma IdRoofEqrel_left {x y : ob C} (R1 : Roof x y) :
    (make_eqrel (RoofHrel x y) (RoofEqrel x y)) R1 (roof_comp (IdRoof x) R1).
  Proof.
    set (comp := roof_comp (IdRoof x) R1). unfold roof_comp in comp.
    set (sqr := isLocClassSqr2 iLC R1 (IdRoof x) x (RoofMor1 R1) (RoofMor1Is R1)
                               (RoofMor2 (IdRoof x))).
    fold sqr in comp. apply eqrelsymm.
    intros P X. apply X. clear X P.
    use make_RoofTop.
    - exact comp.
    - exact (identity comp).
    - exact (LocSqr2Mor1 sqr).
    - use (isLocClassComp iLC).
      + apply (isLocClassIs iLC).
      + apply (RoofMor1Is comp).
    - rewrite id_left. cbn. apply (! (LocSqr2Comm sqr)).
    - cbn. rewrite id_left. apply idpath.
  Qed.

  Lemma IdRoofEqrel_right {x y : ob C} (R1 : Roof x y) :
    (make_eqrel (RoofHrel x y) (RoofEqrel x y)) R1 (roof_comp R1 (IdRoof y)).
  Proof.
    set (comp := roof_comp R1 (IdRoof y)). unfold roof_comp in comp.
    set (sqr := isLocClassSqr2 iLC (IdRoof y) R1 y (RoofMor1 (IdRoof y))
                               (RoofMor1Is (IdRoof y)) (RoofMor2 R1)).
    fold sqr in comp. apply eqrelsymm.
    intros P X. apply X. clear X P.
    use make_RoofTop.
    - exact comp.
    - exact (identity comp).
    - exact (LocSqr2Mor2 sqr).
    - use (isLocClassComp iLC).
      + apply (isLocClassIs iLC).
      + apply (RoofMor1Is comp).
    - rewrite id_left. cbn. apply idpath.
    - rewrite id_left. cbn. apply (LocSqr2Comm sqr).
  Qed.

  Definition IdRoofEqclass (x : ob C) : RoofEqclass x x.
  Proof.
    exact (RoofEqclassFromRoof (make_Roof x x x (identity x) (identity x) (isLocClassIs iLC x))).
  Defined.

  Definition loc_precategory_data : precategory_data :=
    make_precategory_data
      loc_precategory_ob_mor
      (λ (x : ob C ), IdRoofEqclass x)
      (fun (x y z : ob C) (f : RoofEqclass x y) (g : RoofEqclass y z) ⇒
         pr1 (pr1 (roof_comp_iscontr x y z f g))).

  Lemma loc_id_left_in {x y : loc_precategory_data} (f : loc_precategory_data ⟦x , y ⟧)
    (R1 : Roof x y) (H1 : RoofEqclassIn f R1) :
    pr1 (identity x · f) (roof_comp (IdRoof x) R1).
  Proof.
    apply (pr2 (pr1 (roof_comp_iscontr x x y (IdRoofEqclass x) f))).
    - apply RoofEqclassFromRoofIn.
    - apply H1.
  Qed.

  Local Lemma loc_id_left {x y : loc_precategory_data} (f : loc_precategory_data ⟦x , y ⟧) :
    identity x · f = f.
  Proof.
    use (squash_to_prop (pr1 (RoofEqclassIs f))). apply isasetRoofEqclass. intros f'.
    induction f' as [f1 f2].
    use RoofEqclassEq.
    - intros R HR.
      set (tmp := IdRoofEqrel_left R).
      set (e1 := eqax1 (RoofEqclassIs (identity x · f)) _ _ tmp HR).
      assert (X : RoofEqclassIn (identity x · f) (roof_comp (IdRoof x) f1)).
      {
        cbn.
        apply (pr2 (pr1 (roof_comp_iscontr x x y (IdRoofEqclass x) f)) (IdRoof x)).
        - apply RoofEqclassFromRoofIn.
        - apply f2.
      }
      set (e2 := eqax2 (RoofEqclassIs (identity x · f)) _ _ e1 X).
      set (e3 := IdRoofEqrel_left R).
      use (eqax1 (RoofEqclassIs f)).
      + exact (roof_comp (IdRoof x) f1).
      + use eqreltrans.
        × exact (roof_comp (IdRoof x) R).
        × apply eqrelsymm. apply e2.
        × apply eqrelsymm. apply e3.
      + set (e4 := IdRoofEqrel_left f1).
        use (eqax1 (RoofEqclassIs f)).
        -- exact f1.
        -- exact e4.
        -- exact f2.
    - intros R HR.
      set (tmp := IdRoofEqrel_left R).
      use (eqax1 (RoofEqclassIs (identity x · f))).
      + exact (roof_comp (IdRoof x) R).
      + apply eqrelsymm. apply tmp.
      + apply (pr2 (pr1 (roof_comp_iscontr x x y (IdRoofEqclass x) f))).
        × apply RoofEqclassFromRoofIn.
        × apply HR.
  Qed.

  Local Lemma loc_id_right {x y : loc_precategory_data} (f : loc_precategory_data ⟦x , y ⟧) :
    f · identity y = f.
  Proof.
    use (squash_to_prop (pr1 (RoofEqclassIs f))). apply isasetRoofEqclass. intros f'.
    induction f' as [f1 f2].
    use RoofEqclassEq.
    - intros R HR.
      set (tmp := IdRoofEqrel_right R).
      set (e1 := eqax1 (RoofEqclassIs (f · identity y)) _ _ tmp HR).
      assert (X : RoofEqclassIn (f · identity y) (roof_comp f1 (IdRoof y))).
      {
        cbn.
        apply (pr2 (pr1 (roof_comp_iscontr x y y f (IdRoofEqclass y)))).
        - apply f2.
        - apply RoofEqclassFromRoofIn.
      }
      set (e2 := eqax2 (RoofEqclassIs (f · identity y)) _ _ e1 X).
      use (eqax1 (RoofEqclassIs f)).
      + exact (roof_comp f1 (IdRoof y)).
      + use eqreltrans.
        × exact (roof_comp R (IdRoof y)).
        × apply eqrelsymm. apply e2.
        × apply eqrelsymm. apply tmp.
      + set (e4 := IdRoofEqrel_right f1).
        use (eqax1 (RoofEqclassIs f)).
        -- exact f1.
        -- exact e4.
        -- exact f2.
    - intros R HR.
      set (tmp := IdRoofEqrel_right R).
      use (eqax1 (RoofEqclassIs (f · identity y))).
      + exact (roof_comp R (IdRoof y)).
      + apply eqrelsymm. apply tmp.
      + apply (pr2 (pr1 (roof_comp_iscontr x y y f (IdRoofEqclass y)))).
        × apply HR.
        × apply RoofEqclassFromRoofIn.
  Qed.

  Local Definition loc_precategory_assoc_Roof (x y z w : loc_precategory_data) (R1 : Roof x y)
        (R2 : Roof y z) (R3 : Roof z w) : Roof x w.
  Proof.
    set (sqr1 := isLocClassSqr2 iLC _ _ _ (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R1)).
    set (sqr2 := isLocClassSqr2 iLC _ _ _ (RoofMor1 R3) (RoofMor1Is R3) (RoofMor2 R2)).
    set (sqr3 := isLocClassSqr2 iLC _ _ _ (LocSqr2Mor2 sqr2) (LocSqr2Mor2Is sqr2)
                                (LocSqr2Mor1 sqr1)).
    use make_Roof.
    - exact sqr3.
    - exact (LocSqr2Mor2 sqr3 · LocSqr2Mor2 sqr1 · RoofMor1 R1).
    - exact (LocSqr2Mor1 sqr3 · LocSqr2Mor1 sqr2 · RoofMor2 R3).
    - use (isLocClassComp iLC).
      + use (isLocClassComp iLC).
        × exact (LocSqr2Mor2Is sqr3).
        × exact (LocSqr2Mor2Is sqr1).
      + exact (RoofMor1Is R1).
  Defined.

  Local Lemma loc_precategory_assoc_eqrel1 {x y z w : loc_precategory_data} (R1 : Roof x y)
        (R2 : Roof y z) (R3 : Roof z w) :
    (make_eqrel (RoofHrel x w) (RoofEqrel x w)) (roof_comp (roof_comp R1 R2) R3)
                                               (loc_precategory_assoc_Roof x y z w R1 R2 R3).
  Proof.
    set (R4 := roof_comp R1 R2).
    set (R5 := roof_comp R2 R3).
    set (R6 := loc_precategory_assoc_Roof x y z w R1 R2 R3).
    set (R6' := roof_comp R4 R3).
    set (CR := RoofToCoroof R3).
    set (sqrop := isLocClassSqr1 iLC R3 z w (RoofMor1 R3) (RoofMor1Is R3) (RoofMor2 R3)).
    set (sqr1 := isLocClassSqr2 iLC R2 R1 y (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R1)).
    set (sqr2 := isLocClassSqr2 iLC R3 R2 z (RoofMor1 R3) (RoofMor1Is R3) (RoofMor2 R2)).
    set (sqr3 := isLocClassSqr2 iLC sqr2 sqr1 R2 (LocSqr2Mor2 sqr2) (LocSqr2Mor2Is sqr2)
                                (LocSqr2Mor1 sqr1)).
    set (sqr4 := isLocClassSqr2 iLC R3 sqr1 z (RoofMor1 R3) (RoofMor1Is R3)
                                (LocSqr2Mor1 sqr1 · RoofMor2 R2)).
    set (sqr := isLocClassSqr2 iLC _ _ _ (LocSqr2Mor2 sqr3) (LocSqr2Mor2Is sqr3)
                               (LocSqr2Mor2 sqr4)).
    assert (H : LocSqr2Mor2 sqr · RoofMor2 R6' · CoroofMor2 CR =
                LocSqr2Mor1 sqr · RoofMor2 R6 · CoroofMor2 CR).
    {
      cbn. fold sqrop. fold sqr1. fold sqr2. fold sqr3. fold sqr4.
      rewrite assoc. rewrite assoc. rewrite assoc.
      rewrite <- assoc. rewrite <- (LocSqr1Comm sqrop).
      rewrite <- (assoc _ (RoofMor2 R3)). rewrite <- (LocSqr1Comm sqrop).
      rewrite assoc. rewrite assoc.
      rewrite <- (assoc _ (LocSqr2Mor1 sqr4)). rewrite (LocSqr2Comm sqr4).
      rewrite assoc. rewrite assoc.
      rewrite <- (assoc _ (LocSqr2Mor1 sqr2)). rewrite (LocSqr2Comm sqr2).
      rewrite assoc.
      apply cancel_postcomposition. apply cancel_postcomposition.
      rewrite <- (LocSqr2Comm sqr). rewrite <- assoc. rewrite <- assoc.
      apply cancel_precomposition.
      apply (! (LocSqr2Comm sqr3)).
    }
    set (PostS := isLocClassPost iLC _ _ _ (LocSqr2Mor2 sqr · RoofMor2 R6')
                                 (LocSqr2Mor1 sqr · RoofMor2 R6)
                                 (CoroofMor2 CR) (CoroofMor2Is CR) H).
    intros P X. apply X. clear X P.
    use make_RoofTop.
    - exact (PostS).
    - exact (PostSwitchMor PostS · LocSqr2Mor2 sqr).
    - exact (PostSwitchMor PostS · LocSqr2Mor1 sqr).
    - use (isLocClassComp iLC).
      + use (isLocClassComp iLC).
        × exact (PostSwitchMorIs PostS).
        × exact (LocSqr2Mor2Is sqr).
      + exact (RoofMor1Is R6').
    - rewrite <- assoc. rewrite <- assoc.
      apply cancel_precomposition. cbn. fold sqr1. fold sqr2. fold sqr3. fold sqr4.
      rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc.
      apply cancel_postcomposition. apply cancel_postcomposition.
      exact (! (LocSqr2Comm sqr)).
    - rewrite <- assoc. rewrite <- assoc.
      exact (PostSwitchEq PostS).
  Qed.

  Local Lemma loc_precategory_assoc_eqrel2 (x y z w : loc_precategory_data) (R1 : Roof x y)
        (R2 : Roof y z) (R3 : Roof z w) :
    (make_eqrel (RoofHrel x w) (RoofEqrel x w)) (roof_comp R1 (roof_comp R2 R3))
                                               (loc_precategory_assoc_Roof x y z w R1 R2 R3).
  Proof.
    set (R4 := roof_comp R1 R2).
    set (R5 := roof_comp R2 R3).
    set (R6 := loc_precategory_assoc_Roof x y z w R1 R2 R3).
    set (R6' := roof_comp R1 R5).
    set (CR := RoofToCoroof R2).
    set (sqrop := isLocClassSqr1 iLC R2 y z (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R2)).
    set (sqr1 := isLocClassSqr2 iLC R2 R1 y (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R1)).
    set (sqr2 := isLocClassSqr2 iLC R3 R2 z (RoofMor1 R3) (RoofMor1Is R3) (RoofMor2 R2)).
    set (sqr3 := isLocClassSqr2 iLC sqr2 sqr1 R2 (LocSqr2Mor2 sqr2) (LocSqr2Mor2Is sqr2)
                                (LocSqr2Mor1 sqr1)).
    set (sqr4 := isLocClassSqr2 iLC sqr2 R1 y (LocSqr2Mor2 sqr2 · RoofMor1 R2)
                                (isLocClassComp iLC sqr2 R2 y (LocSqr2Mor2 sqr2)
                                                (LocSqr2Mor2Is sqr2)
                                                (RoofMor1 R2) (RoofMor1Is R2)) (RoofMor2 R1)).
    assert (e0 : SOM _ _ (LocSqr2Mor2 sqr3 · LocSqr2Mor2 sqr1)).
    {
      use (isLocClassComp iLC).
      - exact (LocSqr2Mor2Is sqr3).
      - exact (LocSqr2Mor2Is sqr1).
    }
    set (sqr := isLocClassSqr2 iLC _ _ _ (LocSqr2Mor2 sqr3 · LocSqr2Mor2 sqr1) e0
                               (LocSqr2Mor2 sqr4)).
    assert (e : SOM R3 CR (RoofMor1 R3 · CoroofMor2 CR)).
    {
      use (isLocClassComp iLC).
      - exact (RoofMor1Is R3).
      - exact (CoroofMor2Is CR).
    }
    assert (H : LocSqr2Mor2 sqr · LocSqr2Mor1 sqr4 · LocSqr2Mor1 sqr2 ·
                            (RoofMor1 R3 · LocSqr1Mor2 sqrop) =
                LocSqr2Mor1 sqr · LocSqr2Mor1 sqr3 · LocSqr2Mor1 sqr2 ·
                            (RoofMor1 R3 · LocSqr1Mor2 sqrop)).
    {
      rewrite assoc. rewrite assoc.
      rewrite <- (assoc _ (LocSqr2Mor1 sqr2)). rewrite (LocSqr2Comm sqr2). rewrite assoc.
      rewrite <- (assoc _ (LocSqr2Mor1 sqr2)). rewrite (LocSqr2Comm sqr2). rewrite assoc.
      rewrite <- assoc. rewrite <- (LocSqr1Comm sqrop). rewrite assoc.
      rewrite <- (assoc _ _ (LocSqr1Mor2 sqrop)). rewrite <- (LocSqr1Comm sqrop). rewrite assoc.
      apply cancel_postcomposition.
      rewrite <- (assoc _ (LocSqr2Mor1 sqr3)). rewrite (LocSqr2Comm sqr3). rewrite assoc.

      rewrite <- assoc. rewrite <- assoc. rewrite (LocSqr2Comm sqr4). rewrite assoc.
      rewrite <- (LocSqr2Comm sqr).
      rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc.
      apply cancel_precomposition. apply cancel_precomposition.
      apply (! (LocSqr2Comm sqr1)).
    }
    set (PostS := isLocClassPost iLC _ _ _ (LocSqr2Mor2 sqr · LocSqr2Mor1 sqr4 · LocSqr2Mor1 sqr2)
                                 (LocSqr2Mor1 sqr · LocSqr2Mor1 sqr3 · LocSqr2Mor1 sqr2)
                                 (RoofMor1 R3 · CoroofMor2 CR) e H).
    intros P X. apply X. clear X P.
    use make_RoofTop.
    - exact PostS.
    - exact (PostSwitchMor PostS · LocSqr2Mor2 sqr).
    - exact (PostSwitchMor PostS · LocSqr2Mor1 sqr).
    - use (isLocClassComp iLC).
      + use (isLocClassComp iLC).
        × exact (PostSwitchMorIs PostS).
        × exact (LocSqr2Mor2Is sqr).
      + exact (RoofMor1Is R6').
    - cbn. fold sqr1. fold sqr2. fold sqr3. fold sqr4.
      rewrite <- assoc. apply pathsinv0. rewrite <- assoc. apply cancel_precomposition.
      rewrite assoc. rewrite assoc. rewrite assoc. apply cancel_postcomposition.
      rewrite <- assoc. apply (LocSqr2Comm sqr).
    - cbn. fold sqr1. fold sqr2. fold sqr3. fold sqr4.
      rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc.
      apply cancel_postcomposition.
      set (tmp := PostSwitchEq PostS). rewrite assoc in tmp. rewrite assoc in tmp.
      rewrite assoc in tmp. rewrite assoc in tmp.
      exact tmp.
  Qed.

  Local Lemma loc_precategory_assoc_eqrel (x y z w : loc_precategory_data) (R1 : Roof x y)
        (R2 : Roof y z) (R3 : Roof z w) :
    (make_eqrel (RoofHrel x w) (RoofEqrel x w)) (roof_comp R1 (roof_comp R2 R3))
                                               (roof_comp (roof_comp R1 R2) R3).
  Proof.
    use eqreltrans.
    - exact (loc_precategory_assoc_Roof x y z w R1 R2 R3).
    - exact (loc_precategory_assoc_eqrel2 x y z w R1 R2 R3).
    - apply eqrelsymm.
      exact (loc_precategory_assoc_eqrel1 R1 R2 R3).
  Qed.

  Local Lemma loc_precategory_assoc (a b c d : loc_precategory_data)
        (f : loc_precategory_data ⟦a , b ⟧) (g : loc_precategory_data ⟦b , c ⟧)
        (h : loc_precategory_data ⟦c , d ⟧) : f · (g · h ) = f · g · h.
  Proof.
    use (squash_to_prop (pr1 (RoofEqclassIs f))). apply isasetRoofEqclass. intros f'.
    use (squash_to_prop (pr1 (RoofEqclassIs g))). apply isasetRoofEqclass. intros g'.
    use (squash_to_prop (pr1 (RoofEqclassIs h))). apply isasetRoofEqclass. intros h'.
    induction f' as [f1 f2]. induction g' as [g1 g2]. induction h' as [h1 h2].
    use RoofEqclassEq.
    - intros R HR.
      assert (X1 : pr1 (f · (g · h)) (roof_comp f1 (roof_comp g1 h1))).
      {
        apply (pr2 (pr1 (roof_comp_iscontr a b d f (pr1 (pr1 (roof_comp_iscontr b c d g h)))))).
        - apply f2.
        - apply (pr2 (pr1 (roof_comp_iscontr b c d g h))).
          + apply g2.
          + apply h2.
      }
      assert (X2 : pr1 (f · g · h) (roof_comp (roof_comp f1 g1) h1)).
      {
        apply (pr2 (pr1 (roof_comp_iscontr a c d (pr1 (pr1 (roof_comp_iscontr a b c f g))) h))).
        - apply (pr2 (pr1 (roof_comp_iscontr a b c f g))).
          + apply f2.
          + apply g2.
        - apply h2.
      }
      set (X3 := loc_precategory_assoc_eqrel a b c d f1 g1 h1).
      use (eqax1 (RoofEqclassIs (f · g · h))).
      + exact (roof_comp f1 (roof_comp g1 h1)).
      + use (eqax2 (RoofEqclassIs (f · (g · h)))).
        × exact X1.
        × exact HR.
      + use (eqax1 (RoofEqclassIs (f · g · h))).
        × exact (roof_comp (roof_comp f1 g1) h1).
        × apply eqrelsymm. exact X3.
        × exact X2.
    - intros R HR.
      assert (X1 : pr1 (f · (g · h)) (roof_comp f1 (roof_comp g1 h1))).
      {
        apply (pr2 (pr1 (roof_comp_iscontr a b d f (pr1 (pr1 (roof_comp_iscontr b c d g h)))))).
        - apply f2.
        - apply (pr2 (pr1 (roof_comp_iscontr b c d g h))).
          + apply g2.
          + apply h2.
      }
      assert (X2 : pr1 (f · g · h) (roof_comp (roof_comp f1 g1) h1)).
      {
        apply (pr2 (pr1 (roof_comp_iscontr a c d (pr1 (pr1 (roof_comp_iscontr a b c f g))) h))).
        - apply (pr2 (pr1 (roof_comp_iscontr a b c f g))).
          + apply f2.
          + apply g2.
        - apply h2.
      }
      set (X3 := loc_precategory_assoc_eqrel a b c d f1 g1 h1).
      use (eqax1 (RoofEqclassIs (f · (g · h)))).
      + exact (roof_comp f1 (roof_comp g1 h1)).
      + use eqreltrans.
        × exact (roof_comp (roof_comp f1 g1) h1).
        × exact X3.
        × use (eqax2 (RoofEqclassIs (f · g · h))).
          -- exact X2.
          -- exact HR.
      + exact X1.
  Qed.

  Lemma is_precategory_loc_precategory_data : is_precategory loc_precategory_data.
  Proof.
    apply is_precategory_one_assoc_to_two.
    split.
    - split.
      + intros a b f.
        apply loc_id_left.
      + intros a b f.
        apply loc_id_right.
    - intros a b c d f g h.
      apply loc_precategory_assoc.
  Qed.

The category of roofs under the correct equivalence relation

Definition loc_precategory : precategory := tpair _ _ is_precategory_loc_precategory_data.

In particular, loc_precategory has homsets.

  Lemma has_homsets_loc_precategory : has_homsets loc_precategory.
  Proof.
    intros R1 R2. apply isasetRoofEqclass.
  Qed.

Universal property

We verify that loc_precategory satisfies the universal property required for localization of categories. Universal property: Suppose F : C -> D is a functor which maps the morphisms in SOM to isomorphisms in D. Then there exists a unique functor H : loc_precategory

> D such that functor_composite FunctorToLocalization H = F, where FunctorToLocalization

is the natural inclusion functor C -> loc_precategory.

The unique functor H is constructed in LocalizationUniversalFunctor, commutativity is proved in LocalizationUniversalFunctorComm, and uniqueness of the functor is proved in LocalizationUniversalFunctorUnique. In case the objects of D satisfy isaset, then we also show that commutativity is unique. This means that the type "functor_composite FunctorToLocalization H = F" has only one term.

Maps a morphism to roofs

  Definition MorToRoof {x y : ob C} (f : x --> y) : Roof x y.
  Proof.
    use make_Roof.
    - exact x.
    - exact (identity x).
    - exact f.
    - exact (isLocClassIs iLC x).
  Defined.

MorToRoof is linear with respect to composition in C.

  Lemma MorphismCompEqrel {x y z : ob C} (f : x --> y) (g : y --> z) :
    (make_eqrel _ (RoofEqrel x z)) (MorToRoof (f · g)) (roof_comp (MorToRoof f) (MorToRoof g)).
  Proof.
    set (Rf := MorToRoof f).
    set (Rg := MorToRoof g).
    set (Rfg := MorToRoof (f · g)).
    unfold roof_comp.
    set (sqr1 := isLocClassSqr2 iLC Rg Rf y (RoofMor1 Rg) (RoofMor1Is Rg) (RoofMor2 Rf)).
    set (CR := RoofToCoroof (MorToRoof g)).
    set (sqrop := isLocClassSqr1 iLC y y z (identity y) (isLocClassIs iLC y) g).
    assert (H : LocSqr2Mor1 sqr1 · RoofMor2 Rg · CoroofMor2 CR =
                LocSqr2Mor2 sqr1 · f · g · CoroofMor2 CR).
    {
      cbn. fold sqrop.
      rewrite <- assoc. rewrite <- (LocSqr1Comm sqrop). rewrite id_left.
      rewrite <- assoc. rewrite <- (LocSqr1Comm sqrop). rewrite id_left.
      apply cancel_postcomposition.
      set (tmp := LocSqr2Comm sqr1). cbn in tmp. rewrite id_right in tmp.
      exact tmp.
    }
    set (PostS := isLocClassPost iLC _ _ _ (LocSqr2Mor1 sqr1 · RoofMor2 Rg)
                                 (LocSqr2Mor2 sqr1 · f · g)
                                 (CoroofMor2 CR) (CoroofMor2Is CR) H).
    intros P X. apply X. clear X P.
    use make_RoofTop.
    - exact PostS.
    - exact (PostSwitchMor PostS · (LocSqr2Mor2 sqr1)).
    - exact (PostSwitchMor PostS).
    - use (isLocClassComp iLC).
      + use (isLocClassComp iLC).
        × exact (PostSwitchMorIs PostS).
        × exact (LocSqr2Mor2Is sqr1).
      + exact (RoofMor1Is Rfg).
    - cbn. rewrite assoc. apply idpath.
    - cbn.
      set (tmp := PostSwitchEq PostS). cbn in tmp.
      rewrite assoc in tmp. rewrite assoc in tmp. rewrite assoc in tmp.
      rewrite assoc. rewrite assoc.
      exact (! (tmp)).
  Qed.

This is used to show that the natural inclusion functor C --> loc_precategory respects composition. See FunctorToLocalization.

  Lemma FunctorToLocalization_comp {x y z : ob C} (f : x --> y) (g : y --> z) :
    RoofEqclassFromRoof (MorToRoof (f · g)) =
    pr1 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof (MorToRoof f))
                                (RoofEqclassFromRoof (MorToRoof g)))).
  Proof.
    set (tmpp := roof_comp_iscontr_in x y z (MorToRoof f) (MorToRoof g)).
    set (eqclass := pr1 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof (MorToRoof f))
                                                (RoofEqclassFromRoof (MorToRoof g))))).
    fold eqclass in tmpp.
    set (cont := pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof (MorToRoof f))
                                        (RoofEqclassFromRoof (MorToRoof g)))).
    set (cont' := pr2 cont). cbn in cont, cont'.
    use RoofEqclassEq.
    - intros R HR.
      unfold RoofEqclassIn in tmpp.
      use (eqax1 (RoofEqclassIs eqclass)).
      + exact (roof_comp (MorToRoof f) (MorToRoof g)).
      + use eqreltrans.
        × exact (MorToRoof (f · g)).
        × apply eqrelsymm. apply MorphismCompEqrel.
        × set (HR' := RoofEqclassFromRoofIn (MorToRoof (f · g))).
          use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof (MorToRoof (f · g))))).
          -- exact HR'.
          -- exact HR.
      + exact tmpp.
    - intros R HR.
      use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof (MorToRoof (f · g))))).
      + exact (MorToRoof (f · g)).
      + use eqreltrans.
        × exact (roof_comp (MorToRoof f) (MorToRoof g)).
        × apply MorphismCompEqrel.
        × use (eqax2 (RoofEqclassIs eqclass)).
          -- exact tmpp.
          -- exact HR.
      + apply RoofEqclassFromRoofIn.
  Qed.

This is the natural inclusion functor from C to loc_precategory. It is identity on objects and sends a morphisms f : X --> Y to a roof (id_X, f).

  Definition FunctorToLocalization : functor C loc_precategory.
  Proof.
    use tpair.
    - use functor_data_constr.
      + intros x. exact x.
      + intros x y f. exact (RoofEqclassFromRoof (MorToRoof f)).
    - split.
      + intros x. apply idpath.
      + intros x y z f g. exact (FunctorToLocalization_comp f g).
  Defined.

This definition is the map used by the unique localization functor to map morphisms. It sends a roof (s, f) to the composite ( F s)^{-1} · ( F f).

  Definition MorMap (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)) :
    Roof x y → D ⟦F x , F y ⟧.
  Proof.
    intros R.
    exact (inv_from_iso (make_iso _ (H _ _(RoofMor1 R) (RoofMor1Is R))) · (# F (RoofMor2 R))).
  Defined.

One of the 2-out-of-3 properties for isomorphisms.

  Lemma is_iso_pre {D : precategory} {x y z : D} (f : x --> y) (g : y --> z)
        (H1 : is_iso (f · g)) (H2 : is_iso g) : is_iso f.
  Proof.
    set (iso1 := make_iso _ H1).
    set (iso2 := make_iso _ H2).
    set (inv1 := inv_from_iso iso1).
    set (inv2 := inv_from_iso iso2).
    use is_iso_qinv.
    - exact (g · inv1).
    - split.
      + rewrite assoc. unfold inv1.
        set (tmp := iso_inv_after_iso iso1). cbn in tmp.
        apply tmp.
      + set (tmp := iso_inv_after_iso iso2). cbn in tmp. rewrite <- tmp. clear tmp.
        rewrite <- assoc. apply cancel_precomposition.
        apply (post_comp_with_iso_is_inj _ _ _ g H2).
        set (tmp := iso_after_iso_inv iso2). cbn in tmp. rewrite tmp. clear tmp.
        rewrite <- assoc. set (tmp := iso_after_iso_inv iso1). cbn in tmp. exact tmp.
  Qed.

These two lemmas are used in the proof of MorMap_iscomprelfun.

  Lemma MorMap_top_mor1_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 (RoofTopMor1 T)).
  Proof.
    use (@is_iso_pre D).
    - exact (F x).
    - exact (# F (RoofMor1 R1)).
    - rewrite <- functor_comp. apply H. apply (RoofTopMor1Is T).
    - apply H. apply (RoofMor1Is R1).
  Qed.

  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.
    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.

Equation for compositions of inverses

  Lemma inv_from_iso_comp {D : precategory} {x y z : D} (f : iso x y) (g : iso y z) :
    inv_from_iso (iso_comp f g) = inv_from_iso g · inv_from_iso f.
  Proof.
    apply pathsinv0. apply inv_iso_unique'. unfold precomp_with. unfold iso_comp. cbn.
    rewrite assoc. rewrite <- (assoc _ g). rewrite iso_inv_after_iso. rewrite id_right.
    apply iso_inv_after_iso.
  Qed.

MorMap is compatible with equivalence relation of roofs when one assumes that all the morpsisms in SOM are mapped to isomorphisms.

  Lemma MorMap_iscomprelfun (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)) :
    iscomprelfun (make_eqrel _ (RoofEqrel x y)) (MorMap D hsD F x y H).
  Proof.
    intros R1 R2 T'.
    use (squash_to_prop T'). apply hsD. intros T. clear T'.
    set (iso1 := make_iso _ (H _ _ _ (RoofMor1Is R1))).
    set (iso2 := make_iso _ (H _ _ _ (RoofMor1Is R2))).
    set (iso3 := make_iso _ (MorMap_top_mor1_is_iso D hsD F x y H R1 R2 T)).
    set (iso4 := make_iso _ (MorMap_top_mor2_is_iso D hsD F x y H R1 R2 T)).
    unfold MorMap.
    rewrite <- (id_left (# F (RoofMor2 R1))).
    rewrite <- (iso_after_iso_inv (iso3)). cbn.
    rewrite <- assoc. rewrite <- functor_comp. rewrite assoc.
    rewrite <- inv_from_iso_comp.
    rewrite (RoofTopEq2 T). rewrite functor_comp.
    fold iso1 iso2 iso3 iso4.
    assert (X : iso_comp iso3 iso1 = iso_comp iso4 iso2).
    {
      apply eq_iso. cbn.
      rewrite <- functor_comp. rewrite <- functor_comp. apply maponpaths.
      apply (RoofTopEq1 T).
    }
    rewrite X.
    rewrite inv_from_iso_comp. rewrite <- assoc.
    apply cancel_precomposition.
    rewrite assoc.
    set (tmp := iso_after_iso_inv iso4). cbn in tmp. rewrite tmp. clear tmp.
    apply id_left.
  Qed.

There is a unique morphism in D such that all the roofs R which are in equivalence class eqclass are mapped to. This uses the assumption H' which says that all morphisms in SOM are mapped to isomorphisms in D.

  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.

MorMap equality from MorMap_iscontr

  Lemma MorMap_iscontr_eq (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) (R : Roof x y) (H1 : RoofEqclassIn eqclass R) :
    pr1 (pr1 (MorMap_iscontr D hsD F H' x y eqclass)) = MorMap D hsD F x y H' R.
  Proof.
    apply (pr2 (pr1 (MorMap_iscontr D hsD F H' x y eqclass))).
    exact H1.
  Qed.

Equivalence class equality of roof_comp_iscontr with roof_comp's using R1'' and R2''

  Lemma roof_comp_iscontr_eqclass {x y z : ob C} (R1 : RoofEqclass x y) (R2 : RoofEqclass y z)
        (R1' : Roof x y) (R1'' : RoofEqclassIn R1 R1')
        (R2' : Roof y z) (R2'' : RoofEqclassIn R2 R2') :
    pr1 (pr1 (roof_comp_iscontr x y z R1 R2)) = RoofEqclassFromRoof (roof_comp R1' R2').
  Proof.
    set (tmp := pr2 (pr1 (roof_comp_iscontr x y z R1 R2)) R1' R1'' R2' R2'').
    use RoofEqclassEq.
    - intros R3 HR3.
      use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof (roof_comp R1' R2')))).
      + exact (roof_comp R1' R2').
      + use (eqax2 (RoofEqclassIs (pr1 (pr1 (roof_comp_iscontr x y z R1 R2))))).
        × exact tmp.
        × exact HR3.
      + apply RoofEqclassFromRoofIn.
    - intros R3 HR3.
      use (eqax1 (RoofEqclassIs (pr1 (pr1 (roof_comp_iscontr x y z R1 R2))))).
      + exact (roof_comp R1' R2').
      + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof (roof_comp R1' R2')))).
        × apply RoofEqclassFromRoofIn.
        × exact HR3.
      + apply tmp.
  Qed.

MorMap is linear with respect to composition in D

  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.
    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 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 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.

Construct a roof representing s^{-1} from a morphism s in SOM

  Definition InvRoofFromMorInSom {x y : C} (s : y --> x) (S : SOM y x s) : Roof x y.
  Proof.
    use make_Roof.
    - exact y.
    - exact s.
    - exact (identity y).
    - exact S.
  Defined.

Roof is equivalent to composition of its "components".

  Definition RoofDecomposeEqrel {x y : C} (R : Roof x y) :
    (make_eqrel _ (RoofEqrel x y)) R (roof_comp (InvRoofFromMorInSom (RoofMor1 R) (RoofMor1Is R))
                                               (MorToRoof (RoofMor2 R))).
  Proof.
    unfold roof_comp.
    set (sqr := isLocClassSqr2 iLC (MorToRoof (RoofMor2 R))
                               (InvRoofFromMorInSom (RoofMor1 R) (RoofMor1Is R)) R
                               (RoofMor1 (MorToRoof (RoofMor2 R)))
                               (RoofMor1Is (MorToRoof (RoofMor2 R)))
                               (RoofMor2 (InvRoofFromMorInSom (RoofMor1 R) (RoofMor1Is R)))).
    fold sqr.
    intros P X. apply X. clear X P.
    use make_RoofTop.
    - exact sqr.
    - exact (LocSqr2Mor2 sqr).
    - exact (identity (sqr)).
    - use (isLocClassComp iLC).
      + exact (LocSqr2Mor2Is sqr).
      + exact (RoofMor1Is R).
    - rewrite id_left. cbn. apply idpath.
    - cbn. set (tmp := LocSqr2Comm sqr). cbn in tmp.
      rewrite id_right in tmp. rewrite id_right in tmp.
      rewrite id_left. rewrite tmp. apply idpath.
  Qed.

Composition of RoofEqclasses is the same as the equivalence class of composition of the roofs.

  Lemma RoofEqclassCompToRoofComp {x y z : C} (R1 : Roof x y) (R2 : Roof y z) :
    @compose loc_precategory x y z (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2) =
    (RoofEqclassFromRoof (roof_comp R1 R2)).
  Proof.
    apply RoofEqclassEqRoof.
    apply (pr2 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))).
    - apply RoofEqclassFromRoofIn.
    - apply RoofEqclassFromRoofIn.
  Qed.

Equivalent roofs give rise to the same equivalence class.

  Lemma RoofEqClassEq1 {x y : ob C} (R1 R2 : Roof x y) (H : (make_eqrel _ (RoofEqrel x y)) R1 R2) :
    (RoofEqclassFromRoof R1 ) = (RoofEqclassFromRoof R2 ).
  Proof.
    use RoofEqclassEq.
    - intros R HR.
      use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R2))).
      + exact R1.
      + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof R1))).
        × exact (RoofEqclassFromRoofIn R1).
        × exact HR.
      + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof R2))).
        × exact H.
        × exact (RoofEqclassFromRoofIn R2).
    - intros R HR.
      use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R1))).
      + exact R2.
      + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof R2))).
        × exact (RoofEqclassFromRoofIn R2).
        × exact HR.
      + use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R1))).
        × exact R1.
        × exact H.
        × exact (RoofEqclassFromRoofIn R1).
  Qed.

This lemma is used to show that inverse roof composed with roof gives the same equivalence class as the IdRoof.

  Lemma RoofEqclassCompInvRToId {x y : ob C} (f1 : Roof x y) :
    @compose loc_precategory _ _ _
             (RoofEqclassFromRoof (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1)))
             (RoofEqclassFromRoof (MorToRoof (RoofMor1 f1))) = (RoofEqclassFromRoof (IdRoof x)).
  Proof.
    set (R1 := (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))).
    set (R2 := (MorToRoof (RoofMor1 f1))).
    set (tmp := pr2 (pr1 (roof_comp_iscontr x f1 x (RoofEqclassFromRoof R1)
                                            (RoofEqclassFromRoof R2)))).
    cbn in tmp.
    use pathscomp0.
    - exact (RoofEqclassFromRoof (roof_comp R1 R2)).
    - use RoofEqclassEqRoof.
      apply tmp.
      + apply RoofEqclassFromRoofIn.
      + apply RoofEqclassFromRoofIn.
    - apply RoofEqClassEq1.
      intros P X. apply X. clear X P. clear tmp.
      unfold roof_comp.
      set (sqr := (isLocClassSqr2 iLC R2 R1 f1 (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R1))).
      use make_RoofTop.
      + exact sqr.
      + cbn. exact (identity sqr).
      + exact (LocSqr2Mor2 sqr · (RoofMor1 f1)).
      + use (isLocClassComp iLC).
        × exact (isLocClassIs iLC _).
        × exact (RoofMor1Is _).
      + rewrite id_left. cbn. rewrite id_right. apply idpath.
      + rewrite id_left. rewrite id_right. cbn.
        set (tmp := LocSqr2Comm sqr). cbn in tmp. rewrite id_right in tmp. rewrite id_right in tmp.
        rewrite tmp. apply idpath.
  Qed.

This lemma shows that the equivalence class of roofs induced by a roof R is equal to the equivalence class of roofs induced by composition of roofs (InvRoof (RoofMor1 R)) and (MorToRoof (RoofMor2 R))

  Lemma RoofEqclassToRoofComp {x y : ob C} (R : Roof x y) :
    RoofEqclassFromRoof R =
    RoofEqclassFromRoof
      (roof_comp (InvRoofFromMorInSom (RoofMor1 R) (RoofMor1Is R)) (MorToRoof (RoofMor2 R))).
  Proof.
    use RoofEqclassEqRoof.
    use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R))).
    - exact R.
    - exact (RoofDecomposeEqrel R).
    - apply RoofEqclassFromRoofIn.
  Defined.
  Opaque RoofEqclassToRoofComp.

This lemma is used to show that the localization functor LocalizationUniversalFunctor is indeed a functor.

  Lemma LocalizationUniversalFunctor_isfunctor
    (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)) :
    @is_functor loc_precategory_data D
      (functor_data_constr
         loc_precategory_ob_mor D (λ x : C , F x)
         (λ (x y : C) (eqclass : RoofEqclass x y ),
          pr1 (pr1 (MorMap_iscontr D hsD F H' x y eqclass)))).
  Proof.
    split.
    - intros x. cbn. cbn in ×.
      set (tmp := pr2 (pr1 (MorMap_iscontr D hsD F H' x x (IdRoofEqclass x))) (IdRoof x)).
      assert (H2 : MorMap D hsD F x x H' (IdRoof x) = identity (F x)).
      {
        unfold MorMap. cbn.
        set (iso := make_iso _ (H' x x (identity x) (isLocClassIs iLC x))).
        set (tmpp := iso_after_iso_inv iso). cbn in tmpp. apply tmpp.
      }
      use (pathscomp0 _ H2).
      apply tmp.
      apply RoofEqclassFromRoofIn.
    - intros x y z R1 R2. cbn.
      use (squash_to_prop (pr1 (RoofEqclassIs R1))). apply hsD. intros R1'.
      induction R1' as [R1' R1''].
      use (squash_to_prop (pr1 (RoofEqclassIs R2))). apply hsD. intros R2'.
      induction R2' as [R2' R2''].
      rewrite (MorMap_iscontr_eq D hsD F H' x y R1 R1' R1'').
      rewrite (MorMap_iscontr_eq D hsD F H' y z R2 R2' R2'').
      rewrite (roof_comp_iscontr_eqclass R1 R2 R1' R1'' R2' R2'').
      set (tmp := pr2 (pr1 (MorMap_iscontr
                              D hsD F H' x z (RoofEqclassFromRoof (roof_comp R1' R2'))))
                      (roof_comp R1' R2') (RoofEqclassFromRoofIn (roof_comp R1' R2'))).
      rewrite tmp. clear tmp.
      apply MorMap_compose.
  Qed.

The universal functor which we use to factor F through loc_precategory

  Definition LocalizationUniversalFunctor (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)) :
    functor loc_precategory D.
  Proof.
    use make_functor.
    - use functor_data_constr.
      + intros x. exact (F x).
      + intros x y eqclass. apply (pr1 (pr1 (MorMap_iscontr D hsD F H' x y eqclass))).
    - exact (LocalizationUniversalFunctor_isfunctor D hsD F H').
  Defined.

We show that LocalizationUniversalFunctor satisfies the commutativity required for the universal functor.

  Definition LocalizationUniversalFunctorComm (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)) :
    functor_composite FunctorToLocalization (LocalizationUniversalFunctor D hsD F H') = F.
  Proof.
    use (functor_eq _ _ hsD).
    use total2_paths_f.
    - apply idpath.
    - cbn.
      use funextsec. intros a.
      use funextsec. intros b.
      use funextsec. intros f.
      use (pathscomp0 (MorMap_iscontr_eq D hsD F H' a b (RoofEqclassFromRoof (MorToRoof f))
                                         (MorToRoof f) (RoofEqclassFromRoofIn _))).
      unfold MorToRoof. unfold MorMap. cbn.
      set (iso := (make_iso (# F (identity a)) (H' a a (identity a) (isLocClassIs iLC a)))).
      assert (X : iso = identity_iso (F a)).
      {
        use eq_iso. cbn.
        rewrite functor_id.
        apply idpath.
      }
      rewrite X. cbn. apply id_left.
  Qed.

This lemma shows uniqueness of the functor LocalizationUniversalFunctor

  Lemma LocalizationUniversalFunctorUnique (D : precategory) (hsD : has_homsets D) (F : functor C D)
        (H' : ∏ (x y : C) (f : C ⟦ x , y ⟧), SOM x y f → is_iso (# F f))
        (y : functor loc_precategory D) (T : functor_composite FunctorToLocalization y = F) :
    y = (LocalizationUniversalFunctor D hsD F H').
  Proof.
    use (functor_eq _ _ hsD).
    use total2_paths_f.
    - induction T. apply idpath.
    - use funextsec. intros a.
      use funextsec. intros b.
      use funextsec. intros f.
      induction T. cbn. unfold idfun.
      use (squash_to_prop (pr1 (RoofEqclassIs f))). apply hsD. intros f'. induction f' as [f1 f2].
      rewrite (RoofEqclassEqRoof f f1 f2).
      use (pathscomp0 _ (! (pr2 (pr1 (MorMap_iscontr
                                        D hsD (functor_composite FunctorToLocalization y)
                                        H' a b (RoofEqclassFromRoof f1)))
                                f1 (RoofEqclassFromRoofIn f1)))).
      rewrite (RoofEqclassToRoofComp f1).
      rewrite <- (RoofEqclassCompToRoofComp (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))
                                           (MorToRoof (RoofMor2 f1))).
      use (pathscomp0 (@functor_comp
                         loc_precategory D y
                         _ _ _
                         (RoofEqclassFromRoof (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1)))
                         (RoofEqclassFromRoof (MorToRoof (RoofMor2 f1))))).
      unfold functor_composite. cbn. apply cancel_postcomposition.
      set (iso1 := make_iso _ (H' f1 a (RoofMor1 f1) (RoofMor1Is f1))).
      apply (post_comp_with_iso_is_inj _ _ _ _ (pr2 iso1)).
      use (pathscomp0 _ (! (iso_after_iso_inv iso1))).
      unfold iso1. clear iso1. cbn.
      set (tmp := @functor_comp
                    loc_precategory D y
                    _ _ _
                    (RoofEqclassFromRoof (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1)))
                    (RoofEqclassFromRoof (MorToRoof (RoofMor1 f1)))).
      unfold functor_on_morphisms in tmp. apply pathsinv0 in tmp. use (pathscomp0 tmp). clear tmp.
      rewrite RoofEqclassCompInvRToId.
      apply (@functor_id loc_precategory D y).
  Qed.

The following lemma only applies when the objects of D satisfy isaset.

  Lemma LocalizationUniversalProperty (D : precategory) (hsD : has_homsets D) (hssD : isaset D)
        (F : functor C D) (H' : ∏ (x y : C) (f : x --> y) (s : SOM x y f ), is_iso (# F f)) :
    iscontr (∑ H : functor loc_precategory D , functor_composite FunctorToLocalization H = F).
  Proof.
    use unique_exists.
    - exact (LocalizationUniversalFunctor D hsD F H').
    - exact (LocalizationUniversalFunctorComm D hsD F H').
    - intros y. apply (functor_isaset _ _ hsD hssD).
    - exact (LocalizationUniversalFunctorUnique D hsD F H').
  Defined.
  Opaque LocalizationUniversalProperty.

The functor FunctorToLocalization maps morphisms in SOM to isomorphisms

  Definition FunctorToLocalization_is_iso :
    ∏ (x y : C) (f : x --> y) (s : SOM x y f ), is_iso (# FunctorToLocalization f).
  Proof.
    intros x y f s. cbn.
    use (@is_iso_qinv loc_precategory).
    - exact (RoofEqclassFromRoof (InvRoofFromMorInSom f s)).
    - split.
      + set (sqr := isLocClassSqr2 iLC (InvRoofFromMorInSom f s) (MorToRoof f) y
                                   (RoofMor1 (InvRoofFromMorInSom f s))
                                   (RoofMor1Is (InvRoofFromMorInSom f s))
                                   (RoofMor2 (MorToRoof f))).
        set (PostS := isLocClassPost iLC sqr x y (LocSqr2Mor2 sqr) (LocSqr2Mor1 sqr) f s
                                     (! (LocSqr2Comm sqr))).
        rewrite RoofEqclassCompToRoofComp.
        use RoofEqClassEq1.
        intros P X. apply X. clear X P.
        unfold roof_comp. fold sqr.
        use make_RoofTop.
        × exact PostS.
        × exact (PostSwitchMor PostS).
        × exact (PostSwitchMor PostS · LocSqr2Mor2 sqr).
        × use (isLocClassComp iLC).
          -- exact (PostSwitchMorIs PostS).
          -- use (isLocClassComp iLC).
             ++ exact (LocSqr2Mor2Is sqr).
             ++ exact (isLocClassIs iLC x).
        × cbn. rewrite assoc. apply idpath.
        × cbn. rewrite assoc. rewrite id_right. rewrite id_right.
          exact (! (PostSwitchEq PostS)).
      + set (sqr := isLocClassSqr2 iLC (MorToRoof f) (InvRoofFromMorInSom f s) x
                                   (RoofMor1 (MorToRoof f)) (RoofMor1Is (MorToRoof f))
                                   (RoofMor2 (InvRoofFromMorInSom f s))).
        rewrite RoofEqclassCompToRoofComp.
        use RoofEqClassEq1.
        intros P X. apply X. clear X P.
        unfold roof_comp. fold sqr.
        use make_RoofTop.
        × exact sqr.
        × exact (identity sqr).
        × exact (LocSqr2Mor2 sqr · f).
        × use (isLocClassComp iLC).
          -- exact (isLocClassIs iLC sqr).
          -- use (isLocClassComp iLC).
             ++ exact (LocSqr2Mor2Is sqr).
             ++ exact s.
        × rewrite id_left. cbn. rewrite id_right. apply idpath.
        × rewrite id_left. cbn. rewrite id_right.
          set (tmp := LocSqr2Comm sqr). cbn in tmp.
          rewrite id_right in tmp. rewrite id_right in tmp. rewrite tmp.
          apply idpath.
  Qed.

Localization of categories is unique up to isomorphism of categories and loc_precategory is one such precategory.

  Lemma LocalizationUniversalCategory (CC : precategory) (hss : has_homsets CC)
        (In : functor C CC) (H' : ∏ (x y : C) (f : x --> y) (s : SOM x y f ), is_iso (# In f))
        (HH : ∏ (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)),
              ∑ HH : functor CC D , (functor_composite In HH = F )
                                     × (∏ (yy : functor CC D) (comm : functor_composite In yy = F ),
                                        yy = HH )) :
    ∑ D : (functor CC loc_precategory × functor loc_precategory CC ),
          (functor_composite (dirprod_pr1 D) (dirprod_pr2 D) = (functor_identity _))
            × (functor_composite (dirprod_pr2 D) (dirprod_pr1 D) = (functor_identity _)).
  Proof.
    set (comm1 := LocalizationUniversalFunctorComm CC hss In H').
    set (tmp := HH loc_precategory has_homsets_loc_precategory FunctorToLocalization
                   FunctorToLocalization_is_iso).
    induction tmp as [inv1 p]. induction p as [comm2 unique2].
    set (inv2 := (LocalizationUniversalFunctor CC hss In H')).
    use tpair.
    - use make_dirprod.
      + exact inv1.
      + exact inv2.
    - use make_dirprod.
      + cbn.
        rewrite <- comm2 in comm1. rewrite functor_assoc in comm1.
        set (tmp := HH CC hss In H').
        induction tmp as [F' CC2]. induction CC2 as [comm3 unique3].
        set (tmp1 := unique3 (functor_identity CC) (functor_identity_right _ _ _)).
        set (tmp2 := unique3 (functor_composite inv1 (LocalizationUniversalFunctor CC hss In H'))
                             comm1).
        rewrite <- tmp1 in tmp2. exact tmp2.
      + cbn.
        rewrite <- comm1 in comm2. rewrite functor_assoc in comm2.
        set (tmp := LocalizationUniversalFunctorUnique
                      loc_precategory has_homsets_loc_precategory FunctorToLocalization
                      FunctorToLocalization_is_iso).
        set (tmp1 := tmp _ comm2). fold inv2 in tmp1.
        set (tmp2 := tmp (functor_identity _) (functor_identity_right _ _ _)).
        rewrite <- tmp2 in tmp1.
        exact tmp1.
  Defined.
  Opaque LocalizationUniversalCategory.

End def_roofs.