Timings for LocalizingClass.v
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-unimath.dev//./UniMath/CategoryTheory/LocalizingClass.v.timing
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-unimath.dev//./UniMath/CategoryTheory/LocalizingClass.v.timing
(** * 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.
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.
*)
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.
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).
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.
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)).
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.
set (sqr := isLocClassSqr1 iLC _ _ _ (RoofMor1 R) (RoofMor1Is R) (RoofMor2 R)).
exact (LocSqr1Mor2Is sqr).
(** ** 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).
use (squash_to_prop T1').
use (squash_to_prop T2').
set (tmp := isLocClassSqr2 iLC T2 T1 x (RoofTopMor1 T2 · RoofMor1 R2) (RoofTopMor1Is T2)
(RoofTopMor2 T1 · RoofMor1 R2)).
induction tmp as [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).
exact ((pr2 t) · m2 · RoofTopMor1 T1).
exact ((pr2 t) · m1 · RoofTopMor2 T2).
use (isLocClassComp iLC).
use (isLocClassComp iLC).
exact (RoofTopMor1Is T1).
repeat rewrite assoc in p2.
set (tmp := RoofTopEq1 T2).
repeat rewrite <- (assoc (pr2 t)).
apply cancel_precomposition.
apply cancel_precomposition.
repeat rewrite assoc in p2.
set (tmp := RoofTopEq2 T2).
apply cancel_precomposition.
apply cancel_precomposition.
rewrite <- (RoofTopEq1 T).
exact (! (RoofTopEq1 T)).
exact (! (RoofTopEq2 T)).
(** We are interested in the equivalence classes of roofs. *)
(* Definition eqclass {X : UU} {r : eqrel X} : UU := ∑ A : hsubtype X, iseqclass r A. *)
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).
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.
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.
set (tmp := eqax1 (pr2 RE1) R1 R2 H H1).
set (tmp' := eqax2 (pr2 RE1) R R2 H' tmp).
apply (eqax1 (pr2 RE2) R2 R tmp' H2).
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).
Definition RoofEqclassFromRoof {x y : ob C} (R : Roof x y) : RoofEqclass x y.
exact (λ RR : Roof x y, (make_eqrel _ (RoofEqrel x y)) RR R).
Definition RoofEqclassFromRoofIn {x y : ob C} (R : Roof x y) :
RoofEqclassIn (RoofEqclassFromRoof R) R.
use (isLocClassComp iLC).
apply (isLocClassIs iLC).
Definition RoofEqclassEqRoof {x y : ob C} (RE : RoofEqclass x y)
(R : Roof x y) (HR : RoofEqclassIn RE R) : RE = RoofEqclassFromRoof R.
use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R))).
use (eqax2 (RoofEqclassIs RE)).
apply RoofEqclassFromRoofIn.
use (eqax1 (RoofEqclassIs RE)).
use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof R))).
apply RoofEqclassFromRoofIn.
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.
exact (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R1)) R2 R3 H2 H1).
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.
use (squash_to_prop (pr1 (RoofEqclassIs RE))).
induction RE1 as [RE1 RE2].
apply (eqax1 (RoofEqclassIs RE) RE1 R3).
apply (eqax2 (RoofEqclassIs RE) RE1 R2 RE2 H1).
Definition roof_comp {x y z : ob C} (R1 : Roof x y) (R2 : Roof y z) : Roof x z.
set (LS2 := isLocClassSqr2 iLC R2 R1 y (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R1)).
exact ((LocSqr2Mor2 LS2) · (RoofMor1 R1)).
exact ((LocSqr2Mor1 LS2) · (RoofMor2 R2)).
use (isLocClassComp iLC).
exact (LocSqr2Mor2Is LS2).
(** ** 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).
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 _ (RoofMor1 R1)).
rewrite <- (assoc _ (RoofMor2 R2)).
set (PreS := isLocClassPre iLC _ _ _ (RoofTopMor1 T · RoofMor1 R1) (RoofTopMor1Is T)
(LocSqr1Mor1 sqr1 · LocSqr1Mor1 sqr3)
(LocSqr1Mor1 sqr2 · LocSqr1Mor2 sqr3) H).
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).
rewrite <- (LocSqr1Comm sqr3).
apply cancel_postcomposition.
apply cancel_postcomposition.
apply (LocSqr1Comm sqr1).
rewrite (PreSwitchEq PreS).
apply cancel_postcomposition.
apply cancel_postcomposition.
apply (LocSqr1Comm sqr2).
(** 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).
set (T' := RoofTopToCoroof T).
set (R4 := roof_comp R1 R3).
set (R5 := roof_comp R2 R3).
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)).
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).
assert (H : LocSqr2Mor1 sqr6 · LocSqr2Mor1 sqr5 · (RoofMor1 R3 · CoroofMor2 CR) =
LocSqr2Mor2 sqr6 · LocSqr2Mor1 sqr4 · (RoofMor1 R3 · CoroofMor2 CR)).
rewrite <- (assoc _ (LocSqr2Mor1 sqr5)).
rewrite (LocSqr2Comm sqr5).
rewrite <- (assoc _ (LocSqr2Mor1 sqr4)).
rewrite (LocSqr2Comm sqr4).
rewrite <- (dirprod_pr1 eq).
rewrite <- (dirprod_pr2 eq).
apply cancel_postcomposition.
set (tmp := LocSqr2Comm sqr6).
set (PostS := isLocClassPost iLC _ _ _
(LocSqr2Mor1 sqr6 · LocSqr2Mor1 sqr5)
(LocSqr2Mor2 sqr6 · LocSqr2Mor1 sqr4)
(RoofMor1 R3 · CoroofMor2 CR) s H).
exact (PostSwitchMor PostS · LocSqr2Mor2 sqr6).
exact (PostSwitchMor PostS · LocSqr2Mor1 sqr6).
use (isLocClassComp iLC).
use (isLocClassComp iLC).
exact (PostSwitchMorIs PostS).
exact (LocSqr2Mor2Is sqr6).
apply cancel_precomposition.
apply (! (LocSqr2Comm sqr6)).
set (tmp := ! (PostSwitchEq PostS)).
apply (maponpaths (λ f : _, f · RoofMor2 R3)) in tmp.
(** 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).
set (T' := RoofTopToCoroof T).
set (R4 := roof_comp R1 R2).
set (R5 := roof_comp R1 R3).
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)).
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 <- (dirprod_pr1 eq).
rewrite <- (dirprod_pr2 eq).
rewrite <- (assoc _ (LocSqr2Mor1 sqr4)).
rewrite (LocSqr2Comm sqr4).
rewrite <- (assoc _ (LocSqr2Mor1 sqr5)).
rewrite (LocSqr2Comm sqr5).
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).
exact (PostSwitchMor PostS · LocSqr2Mor2 sqr6).
exact (PostSwitchMor PostS · LocSqr2Mor1 sqr6).
use (isLocClassComp iLC).
use (isLocClassComp iLC).
exact (PostSwitchMorIs PostS).
exact (LocSqr2Mor2Is sqr6).
apply cancel_postcomposition.
set (tmp := ! (LocSqr2Comm sqr6)).
apply (maponpaths (λ f : _, PostSwitchMor PostS · f)) in tmp.
set (tmp := PostSwitchEq PostS).
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)).
induction e1 as [e1 e1eq].
induction e2 as [e2 e2eq].
use (squash_to_prop (dirprod_pr1 e1eq)).
induction R1 as [R1 R1'].
use (squash_to_prop (dirprod_pr1 e2eq)).
induction R2 as [R2 R2'].
exact (λ RR : (Roof x z), (make_eqrel _ (RoofEqrel x z)) RR (roof_comp R1 R2)).
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)).
set (tmp1 := eqax2 (pr2 (pr1 t))).
set (tmp1 := eqax1 (pr2 (pr1 t))).
apply (tmp1 (roof_comp R1 R2)).
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).
use (pr2 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))).
apply RoofEqclassFromRoofIn.
apply RoofEqclassFromRoofIn.
(** ** 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.
exact (isLocClassIs iLC x).
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).
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))).
use (isLocClassComp iLC).
apply (isLocClassIs iLC).
apply (! (LocSqr2Comm sqr)).
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)).
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)).
use (isLocClassComp iLC).
apply (isLocClassIs iLC).
Definition IdRoofEqclass (x : ob C) : RoofEqclass x x.
exact (RoofEqclassFromRoof (make_Roof x x x (identity x) (identity x) (isLocClassIs iLC x))).
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).
apply (pr2 (pr1 (roof_comp_iscontr x x y (IdRoofEqclass x) f))).
apply RoofEqclassFromRoofIn.
Local Lemma loc_id_left {x y : loc_precategory_data} (f : loc_precategory_data⟦x, y⟧) :
identity x · f = f.
use (squash_to_prop (pr1 (RoofEqclassIs f))).
set (tmp := IdRoofEqrel_left R).
set (e1 := eqax1 (RoofEqclassIs (identity x · f)) _ _ tmp HR).
(* Need to show that eqrel f1 R *)
assert (X : RoofEqclassIn (identity x · f) (roof_comp (IdRoof x) f1)).
apply (pr2 (pr1 (roof_comp_iscontr x x y (IdRoofEqclass x) f)) (IdRoof x)).
apply RoofEqclassFromRoofIn.
set (e2 := eqax2 (RoofEqclassIs (identity x · f)) _ _ e1 X).
set (e3 := IdRoofEqrel_left R).
use (eqax1 (RoofEqclassIs f)).
exact (roof_comp (IdRoof x) f1).
exact (roof_comp (IdRoof x) R).
set (e4 := IdRoofEqrel_left f1).
use (eqax1 (RoofEqclassIs f)).
set (tmp := IdRoofEqrel_left R).
use (eqax1 (RoofEqclassIs (identity x · f))).
exact (roof_comp (IdRoof x) R).
apply (pr2 (pr1 (roof_comp_iscontr x x y (IdRoofEqclass x) f))).
apply RoofEqclassFromRoofIn.
Local Lemma loc_id_right {x y : loc_precategory_data} (f : loc_precategory_data⟦x, y⟧) :
f · identity y = f.
use (squash_to_prop (pr1 (RoofEqclassIs f))).
set (tmp := IdRoofEqrel_right R).
set (e1 := eqax1 (RoofEqclassIs (f · identity y)) _ _ tmp HR).
(* Need to show (eqrel ...) f1 R *)
assert (X : RoofEqclassIn (f · identity y) (roof_comp f1 (IdRoof y))).
apply (pr2 (pr1 (roof_comp_iscontr x y y f (IdRoofEqclass y)))).
apply RoofEqclassFromRoofIn.
set (e2 := eqax2 (RoofEqclassIs (f · identity y)) _ _ e1 X).
use (eqax1 (RoofEqclassIs f)).
exact (roof_comp f1 (IdRoof y)).
exact (roof_comp R (IdRoof y)).
set (e4 := IdRoofEqrel_right f1).
use (eqax1 (RoofEqclassIs f)).
set (tmp := IdRoofEqrel_right R).
use (eqax1 (RoofEqclassIs (f · identity y))).
exact (roof_comp R (IdRoof y)).
apply (pr2 (pr1 (roof_comp_iscontr x y y f (IdRoofEqclass y)))).
apply RoofEqclassFromRoofIn.
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.
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)).
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).
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).
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).
rewrite <- (LocSqr1Comm sqrop).
rewrite <- (assoc _ (RoofMor2 R3)).
rewrite <- (LocSqr1Comm sqrop).
rewrite <- (assoc _ (LocSqr2Mor1 sqr4)).
rewrite (LocSqr2Comm sqr4).
rewrite <- (assoc _ (LocSqr2Mor1 sqr2)).
rewrite (LocSqr2Comm sqr2).
apply cancel_postcomposition.
apply cancel_postcomposition.
rewrite <- (LocSqr2Comm sqr).
apply cancel_precomposition.
apply (! (LocSqr2Comm sqr3)).
set (PostS := isLocClassPost iLC _ _ _ (LocSqr2Mor2 sqr · RoofMor2 R6')
(LocSqr2Mor1 sqr · RoofMor2 R6)
(CoroofMor2 CR) (CoroofMor2Is CR) H).
exact (PostSwitchMor PostS · LocSqr2Mor2 sqr).
exact (PostSwitchMor PostS · LocSqr2Mor1 sqr).
use (isLocClassComp iLC).
use (isLocClassComp iLC).
exact (PostSwitchMorIs PostS).
exact (LocSqr2Mor2Is sqr).
apply cancel_precomposition.
apply cancel_postcomposition.
apply cancel_postcomposition.
exact (! (LocSqr2Comm sqr)).
exact (PostSwitchEq PostS).
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).
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).
assert (H : LocSqr2Mor2 sqr · LocSqr2Mor1 sqr4 · LocSqr2Mor1 sqr2 ·
(RoofMor1 R3 · LocSqr1Mor2 sqrop) =
LocSqr2Mor1 sqr · LocSqr2Mor1 sqr3 · LocSqr2Mor1 sqr2 ·
(RoofMor1 R3 · LocSqr1Mor2 sqrop)).
rewrite <- (assoc _ (LocSqr2Mor1 sqr2)).
rewrite (LocSqr2Comm sqr2).
rewrite <- (assoc _ (LocSqr2Mor1 sqr2)).
rewrite (LocSqr2Comm sqr2).
rewrite <- (LocSqr1Comm sqrop).
rewrite <- (assoc _ _ (LocSqr1Mor2 sqrop)).
rewrite <- (LocSqr1Comm sqrop).
apply cancel_postcomposition.
rewrite <- (assoc _ (LocSqr2Mor1 sqr3)).
rewrite (LocSqr2Comm sqr3).
rewrite (LocSqr2Comm sqr4).
rewrite <- (LocSqr2Comm sqr).
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).
exact (PostSwitchMor PostS · LocSqr2Mor2 sqr).
exact (PostSwitchMor PostS · LocSqr2Mor1 sqr).
use (isLocClassComp iLC).
use (isLocClassComp iLC).
exact (PostSwitchMorIs PostS).
exact (LocSqr2Mor2Is sqr).
apply cancel_precomposition.
apply cancel_postcomposition.
apply cancel_postcomposition.
set (tmp := PostSwitchEq PostS).
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).
exact (loc_precategory_assoc_Roof x y z w R1 R2 R3).
exact (loc_precategory_assoc_eqrel2 x y z w R1 R2 R3).
exact (loc_precategory_assoc_eqrel1 R1 R2 R3).
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.
use (squash_to_prop (pr1 (RoofEqclassIs f))).
use (squash_to_prop (pr1 (RoofEqclassIs g))).
use (squash_to_prop (pr1 (RoofEqclassIs h))).
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 (pr2 (pr1 (roof_comp_iscontr b c d g h))).
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))).
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)))).
use (eqax1 (RoofEqclassIs (f · g · h))).
exact (roof_comp (roof_comp f1 g1) h1).
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 (pr2 (pr1 (roof_comp_iscontr b c d g h))).
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))).
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)).
exact (roof_comp (roof_comp f1 g1) h1).
use (eqax2 (RoofEqclassIs (f · g · h))).
Lemma is_precategory_loc_precategory_data : is_precategory loc_precategory_data.
apply is_precategory_one_assoc_to_two.
apply loc_precategory_assoc.
(** 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.
(** ** 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.
exact (isLocClassIs iLC x).
(** 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)).
set (Rfg := MorToRoof (f · g)).
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).
rewrite <- (LocSqr1Comm sqrop).
rewrite <- (LocSqr1Comm sqrop).
apply cancel_postcomposition.
set (tmp := LocSqr2Comm sqr1).
set (PostS := isLocClassPost iLC _ _ _ (LocSqr2Mor1 sqr1 · RoofMor2 Rg)
(LocSqr2Mor2 sqr1 · f · g)
(CoroofMor2 CR) (CoroofMor2Is CR) H).
exact (PostSwitchMor PostS · (LocSqr2Mor2 sqr1)).
exact (PostSwitchMor PostS).
use (isLocClassComp iLC).
use (isLocClassComp iLC).
exact (PostSwitchMorIs PostS).
exact (LocSqr2Mor2Is sqr1).
set (tmp := PostSwitchEq PostS).
(** 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)))).
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))))).
set (cont := pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof (MorToRoof f))
(RoofEqclassFromRoof (MorToRoof g)))).
unfold RoofEqclassIn in tmpp.
use (eqax1 (RoofEqclassIs eqclass)).
exact (roof_comp (MorToRoof f) (MorToRoof g)).
exact (MorToRoof (f · g)).
set (HR' := RoofEqclassFromRoofIn (MorToRoof (f · g))).
use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof (MorToRoof (f · g))))).
use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof (MorToRoof (f · g))))).
exact (MorToRoof (f · g)).
exact (roof_comp (MorToRoof f) (MorToRoof g)).
use (eqax2 (RoofEqclassIs eqclass)).
apply RoofEqclassFromRoofIn.
(** 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.
exact (RoofEqclassFromRoof (MorToRoof f)).
exact (FunctorToLocalization_comp f g).
(** 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⟧.
exact (inv_from_iso (make_iso _ (H _ _(RoofMor1 R) (RoofMor1Is R))) · (# F (RoofMor2 R))).
(** 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.
set (iso1 := make_iso _ H1).
set (iso2 := make_iso _ H2).
set (inv1 := inv_from_iso iso1).
set (inv2 := inv_from_iso iso2).
set (tmp := iso_inv_after_iso iso1).
set (tmp := iso_inv_after_iso iso2).
apply cancel_precomposition.
apply (post_comp_with_iso_is_inj _ _ g H2).
set (tmp := iso_after_iso_inv iso2).
set (tmp := iso_after_iso_inv iso1).
(** 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)).
exact (# F (RoofMor1 R1)).
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)).
exact (# F (RoofMor1 R2)).
rewrite <- (RoofTopEq1 T).
(** 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.
rewrite iso_inv_after_iso.
(** 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).
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)).
rewrite <- (id_left (# F (RoofMor2 R1))).
rewrite <- (iso_after_iso_inv (iso3)).
rewrite <- inv_from_iso_comp.
fold iso1 iso2 iso3 iso4.
assert (X : iso_comp iso3 iso1 = iso_comp iso4 iso2).
rewrite inv_from_iso_comp.
apply cancel_precomposition.
set (tmp := iso_after_iso_inv iso4).
(** 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).
use (squash_to_prop (pr1 (RoofEqclassIs eqclass))).
set (tmp := MorMap_iscomprelfun D hsD F x y H').
unfold iscomprelfun in tmp.
exact (MorMap D hsD F x y H' R1).
use (eqax2 (RoofEqclassIs eqclass)).
(** 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.
apply (pr2 (pr1 (MorMap_iscontr D hsD F H' x y eqclass))).
(** 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').
set (tmp := pr2 (pr1 (roof_comp_iscontr x y z R1 R2)) R1' R1'' R2' R2'').
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))))).
apply RoofEqclassFromRoofIn.
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.
(** 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.
set (sqr := isLocClassSqr2 iLC R2 R1 y (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R1)).
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).
rewrite inv_from_iso_comp.
apply cancel_postcomposition.
apply cancel_precomposition.
set (tmp := LocSqr2Comm sqr).
apply (pre_comp_with_iso_is_inj (C:=D) _ _ _ _ (pr2 iso2)).
set (tmp2 := iso_inv_after_iso iso2).
apply (post_comp_with_iso_is_inj (C:=D) _ _ _ (pr2 iso4)).
apply cancel_precomposition.
set (tmp2 := iso_after_iso_inv iso4).
(** 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.
(** 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))).
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)))).
use (isLocClassComp iLC).
exact (LocSqr2Mor2Is sqr).
set (tmp := LocSqr2Comm sqr).
(** 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)).
apply (pr2 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))).
apply RoofEqclassFromRoofIn.
apply RoofEqclassFromRoofIn.
(** 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).
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).
(** 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)).
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)))).
exact (RoofEqclassFromRoof (roof_comp R1 R2)).
apply RoofEqclassFromRoofIn.
apply RoofEqclassFromRoofIn.
set (sqr := (isLocClassSqr2 iLC R2 R1 f1 (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R1))).
exact (LocSqr2Mor2 sqr · (RoofMor1 f1)).
use (isLocClassComp iLC).
exact (isLocClassIs iLC _).
set (tmp := LocSqr2Comm sqr).
(** 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))).
use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R))).
exact (RoofDecomposeEqrel R).
apply RoofEqclassFromRoofIn.
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)))).
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)).
set (iso := make_iso _ (H' x x (identity x) (isLocClassIs iLC x))).
set (tmpp := iso_after_iso_inv iso).
apply RoofEqclassFromRoofIn.
use (squash_to_prop (pr1 (RoofEqclassIs R1))).
induction R1' as [R1' R1''].
use (squash_to_prop (pr1 (RoofEqclassIs 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'))).
(** 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.
apply (pr1 (pr1 (MorMap_iscontr D hsD F H' x y eqclass))).
exact (LocalizationUniversalFunctor_isfunctor D hsD F H').
(** 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.
use (functor_eq _ _ hsD).
use (pathscomp0 (MorMap_iscontr_eq D hsD F H' a b (RoofEqclassFromRoof (MorToRoof f))
(MorToRoof f) (RoofEqclassFromRoofIn _))).
set (iso := (make_iso (# F (identity a)) (H' a a (identity a) (isLocClassIs iLC a)))).
assert (X : iso = identity_iso (F a)).
(** 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').
use (functor_eq _ _ hsD).
use (squash_to_prop (pr1 (RoofEqclassIs f))).
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.
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))).
set (tmp := @functor_comp
loc_precategory D y
_ _ _
(RoofEqclassFromRoof (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1)))
(RoofEqclassFromRoof (MorToRoof (RoofMor1 f1)))).
unfold functor_on_morphisms in tmp.
rewrite RoofEqclassCompInvRToId.
apply (@functor_id loc_precategory D y).
(** 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).
exact (LocalizationUniversalFunctor D hsD F H').
(* Commutativity of the functor *)
exact (LocalizationUniversalFunctorComm D hsD F H').
(* Uniqueness of commutativity *)
apply (functor_isaset _ _ hsD hssD).
(* Uniqueness of the functor *)
exact (LocalizationUniversalFunctorUnique D hsD F H').
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).
use (@is_iso_qinv loc_precategory).
exact (RoofEqclassFromRoof (InvRoofFromMorInSom f s)).
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.
exact (PostSwitchMor PostS).
exact (PostSwitchMor PostS · LocSqr2Mor2 sqr).
use (isLocClassComp iLC).
exact (PostSwitchMorIs PostS).
use (isLocClassComp iLC).
exact (LocSqr2Mor2Is sqr).
exact (isLocClassIs iLC x).
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.
exact (LocSqr2Mor2 sqr · f).
use (isLocClassComp iLC).
exact (isLocClassIs iLC sqr).
use (isLocClassComp iLC).
exact (LocSqr2Mor2Is sqr).
set (tmp := LocSqr2Comm sqr).
(** 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 _)).
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')).
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 <- 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).
set (tmp2 := tmp (functor_identity _) (functor_identity_right _ _ _)).
Opaque LocalizationUniversalCategory.