11import HoTTLean.Groupoids.UnstructuredModel
22import HoTTLean.ForMathlib.CategoryTheory.RepPullbackCone
33
4- universe v u v₁ u₁ v₂ u₂ v₃ u₃
5-
64noncomputable section
75
86namespace GroupoidModel
@@ -13,17 +11,22 @@ attribute [local simp] eqToHom_map Grpd.id_eq_id Grpd.comp_eq_comp Functor.id_co
1311
1412namespace FunctorOperation
1513
14+ /-! We first define Sigma formation as an operation on functors into Grpd. -/
15+
16+ universe v₁ u₁ v₂ u₂ v₃ u₃ v₄ u₄
17+
1618section
17- variable {Γ : Type u₂} [Category.{v₂} Γ] {A : Γ ⥤ Grpd.{v₁,u₁}}
18- (B : ∫ A ⥤ Grpd.{v₁,u₁}) (x : Γ)
19+
20+ variable {Γ : Type u₁} [Category.{v₁} Γ] {A : Γ ⥤ Grpd.{v₂,u₂}} (B : ∫ A ⥤ Grpd.{v₃,u₃})
21+
1922/--
2023For a point `x : Γ`, `(sigma A B).obj x` is the groupoidal Grothendieck
2124 construction on the composition
2225 `ι _ x ⋙ B : A.obj x ⥤ Groupoidal A ⥤ Grpd`
2326-/
24- def sigmaObj : Grpd := Grpd.of (∫ι A x ⋙ B)
27+ def sigmaObj (x : Γ) : Grpd := Grpd.of (∫ι A x ⋙ B)
2528
26- variable {x} { y : Γ} (f : x ⟶ y)
29+ variable {x y : Γ} (f : x ⟶ y)
2730/--
2831For a morphism `f : x ⟶ y` in `Γ`, `(sigma A B).map y` is a
2932composition of functors.
@@ -111,8 +114,7 @@ variable {z : Γ} {f} {g : y ⟶ z}
111114 ιNatTrans_comp_app, Functor.map_comp, eqToHom_map, Grpd.comp_eq_comp, Grpd.eqToHom_obj, cast_heq_iff_heq, heq_eq_eq]
112115 aesop_cat
113116
114- @[simp] theorem sigmaMap_comp_map {A : Γ ⥤ Grpd.{v₁,u₁}}
115- {B : ∫(A) ⥤ Grpd.{v₁,u₁}} {x y z : Γ} {f : x ⟶ y} {g : y ⟶ z}
117+ @[simp] theorem sigmaMap_comp_map {B : ∫(A) ⥤ Grpd.{v₃,u₃}} {x y z : Γ} {f : x ⟶ y} {g : y ⟶ z}
116118 {p q : sigmaObj B x} (hpq : p ⟶ q)
117119 {h1 : (sigmaMap B (f ≫ g)).obj p = (sigmaMap B g).obj ((sigmaMap B f).obj p)}
118120 {h2 : (sigmaMap B g).obj ((sigmaMap B f).obj q) = (sigmaMap B (f ≫ g)).obj q}
@@ -150,15 +152,15 @@ lemma sigmaMap_forget : sigmaMap B f ⋙ forget = forget ⋙ A.map f := rfl
150152 unfolded into operations between functors.
151153 See `sigmaObj` and `sigmaMap` for the actions of this functor.
152154 -/
153- @[simps] def sigma (A : Γ ⥤ Grpd.{v₁,u₁})
154- (B : ∫(A) ⥤ Grpd.{v₁,u₁}) : Γ ⥤ Grpd.{v₁,u₁ } where
155+ @[simps] def sigma (A : Γ ⥤ Grpd.{v₂,u₂}) (B : ∫(A) ⥤ Grpd.{v₃,u₃}) :
156+ Γ ⥤ Grpd.{max v₂ v₃, max u₂ u₃ } where
155157 -- NOTE using Grpd.of here instead of earlier speeds things up
156158 obj x := sigmaObj B x
157159 map := sigmaMap B
158160 map_id _ := sigmaMap_id
159161 map_comp _ _ := sigmaMap_comp
160162
161- variable (B) {Δ : Type u₃ } [Category.{v₃ } Δ] (σ : Δ ⥤ Γ)
163+ variable (B) {Δ : Type u₄ } [Category.{v₄ } Δ] (σ : Δ ⥤ Γ)
162164theorem sigma_naturality_aux (x) :
163165 ι (σ ⋙ A) x ⋙ pre A σ ⋙ B = ι A (σ.obj x) ⋙ B := by
164166 rw [← ι_comp_pre]
@@ -214,8 +216,7 @@ namespace sigma
214216
215217section
216218
217- variable {Γ : Type u₂} [Groupoid.{v₂} Γ] {A : Γ ⥤ Grpd.{v₁,u₁}}
218- (B : ∫(A) ⥤ Grpd.{v₁,u₁})
219+ variable {Γ : Type u₁} [Groupoid.{v₁} Γ] {A : Γ ⥤ Grpd.{v₂,u₂}} (B : ∫(A) ⥤ Grpd.{v₃,u₃})
219220
220221@[simp] def assocFib (x : Γ) : sigmaObj B x ⥤ ∫(B) :=
221222 pre _ _
@@ -504,7 +505,7 @@ lemma assoc_inv_map_fiber {x y} (f : x ⟶ y) : ((assoc B).inv.map f).fiber =
504505 simp [assoc]
505506 rfl
506507
507- lemma assocFibMap_pre_pre_map {Δ : Type u₃ } [Groupoid.{v₃ } Δ] {σ : Δ ⥤ Γ} {x y} (f : x ⟶ y) :
508+ lemma assocFibMap_pre_pre_map {Δ : Type u₄ } [Groupoid.{v₄ } Δ] {σ : Δ ⥤ Γ} {x y} (f : x ⟶ y) :
508509 assocFibMap ((pre B (pre A σ)).map f) ≍ assocFibMap f := by
509510 have pre_pre_obj_base_base (x) : ((pre B (pre A σ)).obj x).base.base = σ.obj x.base.base := by
510511 rw [pre_obj_base, pre_obj_base]
@@ -533,7 +534,7 @@ lemma assocFibMap_pre_pre_map {Δ : Type u₃} [Groupoid.{v₃} Δ] {σ : Δ ⥤
533534 rfl
534535 · simp
535536
536- lemma assoc_comp_fiber {Δ : Type u₃ } [Groupoid.{v₃ } Δ] (σ : Δ ⥤ Γ) {x y} (f : x ⟶ y) :
537+ lemma assoc_comp_fiber {Δ : Type u₄ } [Groupoid.{v₄ } Δ] (σ : Δ ⥤ Γ) {x y} (f : x ⟶ y) :
537538 Hom.fiber (((assoc (pre A σ ⋙ B)).hom ⋙ map (eqToHom (sigma_naturality ..).symm) ⋙
538539 pre (sigma A B) σ).map f) ≍ Hom.fiber ((pre B (pre A σ) ⋙ (assoc B).hom).map f) := by
539540 simp only [assoc_hom, Functor.comp_obj, sigma_obj, Functor.comp_map, sigma_map, pre_map_fiber,
@@ -545,7 +546,7 @@ lemma assoc_comp_fiber {Δ : Type u₃} [Groupoid.{v₃} Δ] (σ : Δ ⥤ Γ) {x
545546 rw! [assocFibMap_pre_pre_map]
546547 simp
547548
548- lemma assoc_comp {Δ : Type u₃ } [Groupoid.{v₃ } Δ] (σ : Δ ⥤ Γ) :
549+ lemma assoc_comp {Δ : Type u₄ } [Groupoid.{v₄ } Δ] (σ : Δ ⥤ Γ) :
549550 (sigma.assoc ((pre A σ) ⋙ B)).hom ⋙
550551 map (eqToHom (by simp [sigma_naturality])) ⋙ pre (sigma A B) σ =
551552 pre B (pre A σ) ⋙ (sigma.assoc B).hom := by
@@ -574,62 +575,14 @@ lemma assoc_comp {Δ : Type u₃} [Groupoid.{v₃} Δ] (σ : Δ ⥤ Γ) :
574575 · intro x y f
575576 apply assoc_comp_fiber B σ f
576577
577- lemma assoc_comp' {Δ : Type u₃ } [Groupoid.{v₃ } Δ] {σ : Δ ⥤ Γ} (Aσ) (eq : Aσ = σ ⋙ A) :
578+ lemma assoc_comp' {Δ : Type u₄ } [Groupoid.{v₄ } Δ] {σ : Δ ⥤ Γ} (Aσ) (eq : Aσ = σ ⋙ A) :
578579 (sigma.assoc ((map (eqToHom eq) ⋙ pre A σ) ⋙ B)).hom ⋙
579580 map (eqToHom (by subst eq; simp [sigma_naturality, map_id_eq])) ⋙ pre (sigma A B) σ =
580581 (pre (pre A σ ⋙ B) (map (eqToHom eq)) ⋙ pre B (pre A σ)) ⋙ (sigma.assoc B).hom := by
581582 subst eq
582583 rw! [eqToHom_refl, map_id_eq]
583584 simp [assoc_comp]
584585
585- section
586-
587- -- def fstAux' : ∫(sigma A B) ⥤ ∫(A) :=
588- -- (assoc B).inv ⋙ forget
589-
590- -- /-- `fst` projects out the pointed groupoid `(A,a)` appearing in `(A,B,a : A,b : B a)` -/
591- -- def fst : ∫(sigma A B) ⥤ PGrpd :=
592- -- fstAux' B ⋙ toPGrpd A
593-
594- -- theorem fst_forgetToGrpd : fst B ⋙ PGrpd.forgetToGrpd = forget ⋙ A := by
595- -- dsimp only [fst, fstAux']
596- -- rw [Functor.assoc, (Functor.Groupoidal.isPullback A).comm_sq,
597- -- ← Functor.assoc]
598- -- conv => left; left; rw [Functor.assoc, assoc_inv_comp_forget_comp_forget]
599-
600- def fstNatTrans : sigma A B ⟶ A where
601- app x := forget
602- naturality x y f:= by simp [sigmaMap_forget]
603-
604- @[simp]
605- lemma fstNatTrans_app (x) : (fstNatTrans B).app x = Functor.Groupoidal.forget :=
606- rfl
607-
608- lemma map_fstNatTrans_eq : map (fstNatTrans B) = (assoc B).inv ⋙ forget := by
609- apply Functor.Groupoidal.FunctorTo.hext
610- · simp [Functor.assoc, assoc_inv_comp_forget_comp_forget, map_forget]
611- · intro x
612- simp only [fstNatTrans, map_obj_fiber, sigma_obj, Functor.Groupoidal.forget_obj, assoc,
613- Functor.Iso.symm_inv, Functor.comp_obj, functorIsoFrom_hom_obj, assocFib, heq_eq_eq]
614- rw! (castMode := .all) [pre_obj_base]
615- simp
616- rfl
617- · intro x y f
618- simp only [fstNatTrans, map_map_fiber, sigma_obj, Grpd.comp_eq_comp, Functor.comp_obj,
619- Functor.Groupoidal.forget_obj, sigma_map, sigmaMap_obj_base, eqToHom_refl, forget_map,
620- Category.id_comp, assoc, Functor.Iso.symm_inv, functorIsoFrom_hom_obj, assocFib,
621- Functor.comp_map, functorIsoFrom_hom_map, comp_base, Functor.Groupoidal.comp_fiber,
622- heq_eqToHom_comp_iff]
623- rw! [pre_map_base]
624- simp only [ι_map_base, ι_obj_base, assocHom, assocFib, assocIso, ι_map_fiber, ι_obj_fiber]
625- rw [preNatIso_hom_app_base, ιNatIso_hom, ιNatTrans_app_base]
626- simp only [Functor.comp_obj, Pi.id_apply, homMk_base, homMk_fiber]
627- erw [CategoryTheory.Functor.map_id (A.map (𝟙 y.base))]
628- erw [Category.id_comp]
629- simp
630- rfl
631-
632- end
633586end
634587
635588end sigma
@@ -638,24 +591,41 @@ end FunctorOperation
638591
639592open FunctorOperation
640593
641- section
642-
643594namespace USig
644595
596+ universe v₁ v₂ u
597+
598+ /-! We now define Sigma on small types (represented as arrows into universes).
599+
600+ Type `A` is `v₁`-sized. Type `B` depending on `A` is `v₂`-sized.
601+ The context category has to fit `ΣA. B` which is `max v₁ v₂`-sized,
602+ but it can also be larger.
603+ Thus the context category is `max u (max v₁ v₂ + 1)`-sized. -/
604+
605+ variable {X : Type (v₂ + 1 )} [LargeCategory.{v₂} X]
606+ {Y : Type (max v₁ v₂ + 1 )} [LargeCategory.{max v₁ v₂} Y]
607+
608+ variable
609+ (S : ∀ {Γ : Ctx.{max u (max v₁ v₂ + 1 )}} (A : Γ ⥤ Grpd.{v₁,v₁}), (∫(A) ⥤ X) → (Γ ⥤ Y))
610+ (S_naturality : ∀ {Γ Δ : Ctx.{max u (max v₁ v₂ + 1 )}} (σ : Δ ⟶ Γ) {A : Γ ⥤ Grpd.{v₁,v₁}}
611+ {B : ∫(A) ⥤ X}, σ ⋙ S A B = S (σ ⋙ A) (pre A σ ⋙ B))
612+ {Γ Δ : Ctx.{max u (max v₁ v₂ + 1 )}}
613+ (σ : Δ ⟶ Γ)
614+ {A : Γ ⟶ U.{v₁, max u (max v₁ v₂ + 1 )}.Ty}
615+ {σA : Δ ⟶ U.{v₁, max u (max v₁ v₂ + 1 )}.Ty}
616+ (eq : σ ≫ A = σA)
617+ (B : U.ext A ⟶ U.{v₂, max u (max v₁ v₂ + 1 )}.Ty)
618+
645619@[simp]
646- abbrev SigAux {X : Type (v + 1 )} [Category.{v} X]
647- (S : ∀ {Γ : Ctx} (A : Γ ⥤ Grpd.{v,v}) (B : ∫(A) ⥤ X), Γ ⥤ X)
648- {Γ : Ctx} {A : Γ ⟶ U.{v}.Ty} (B : U.ext A ⟶ Ctx.coreAsSmall X) :
649- Γ ⟶ Ctx.coreAsSmall X :=
620+ abbrev SigAux
621+ (B : U.ext A ⟶ Ctx.coreAsSmall.{v₂, max u (max v₁ v₂ + 1 )} X) :
622+ Γ ⟶ Ctx.coreAsSmall.{max v₁ v₂, max u (max v₁ v₂ + 1 )} Y :=
650623 toCoreAsSmallEquiv.symm (S (toCoreAsSmallEquiv A) (toCoreAsSmallEquiv B))
651624
652- theorem SigAux_comp {X : Type (v + 1 )} [Category.{v} X]
653- (S : ∀ {Γ : Ctx} (A : Γ ⥤ Grpd.{v,v}) (B : ∫(A) ⥤ X), Γ ⥤ X)
654- (S_naturality : ∀ {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⥤ Grpd}
655- {B : ∫(A) ⥤ X}, σ ⋙ S A B = S (σ ⋙ A) (pre A σ ⋙ B))
656- {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U.{v}.Ty} {σA : Δ ⟶ U.Ty}
657- (eq : σ ≫ A = σA) (B : U.ext A ⟶ Ctx.coreAsSmall X) :
658- SigAux S (U.substWk σ A σA eq ≫ B) = σ ≫ SigAux S B := by
625+ include S_naturality in
626+ theorem SigAux_comp
627+ (B : U.ext A ⟶ Ctx.coreAsSmall.{v₂, max u (max v₁ v₂ + 1 )} X) :
628+ SigAux.{v₁,v₂,u} S (U.substWk σ A σA eq ≫ B) = σ ≫ SigAux.{v₁,v₂,u} S B := by
659629 simp only [SigAux, Grpd.comp_eq_comp]
660630 rw [← toCoreAsSmallEquiv_symm_apply_comp_left]
661631 congr 1
@@ -667,27 +637,24 @@ theorem SigAux_comp {X : Type (v + 1)} [Category.{v} X]
667637 simp [U.substWk_eq, map_id_eq]
668638 rfl
669639
670- def Sig {Γ : Ctx} {A : Γ ⟶ U.{v}.Ty} (B : U.ext A ⟶ U.{v}.Ty) : Γ ⟶ U.{v }.Ty :=
671- SigAux sigma B
640+ def Sig : Γ ⟶ U.{max v₁ v₂, max u (max v₁ v₂ + 1 ) }.Ty :=
641+ SigAux.{v₁,v₂,u} sigma B
672642
673643/--
674644Naturality for the formation rule for Σ-types.
675645Also known as Beck-Chevalley.
676646-/
677- theorem Sig_comp {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U.{v}.Ty} {σA : Δ ⟶ U.Ty}
678- (eq : σ ≫ A = σA) (B : U.ext A ⟶ U.{v}.Ty) :
679- Sig (U.substWk σ A σA eq ≫ B) = σ ≫ Sig B :=
680- SigAux_comp sigma (by intros; rw [sigma_naturality]) σ eq B
647+ theorem Sig_comp : Sig.{v₁,v₂,u} (U.substWk σ A σA eq ≫ B) = σ ≫ Sig.{v₁,v₂,u} B :=
648+ SigAux_comp.{v₁,v₂,u} sigma (by intros; rw [sigma_naturality]) σ eq B
681649
682- def assoc {Γ : Ctx} {A : Γ ⟶ U.{v}.Ty} (B : U. ext A ⟶ U.Ty) : U.ext B ≅ U.ext (USig. Sig B) :=
650+ def assoc : U. ext B ≅ U.ext (Sig.{v₁,v₂,u} B) :=
683651 Grpd.mkIso' (sigma.assoc (toCoreAsSmallEquiv B)) ≪≫
684652 eqToIso (by dsimp [U.ext, Sig]; rw [toCoreAsSmallEquiv.apply_symm_apply])
685653
686- set_option maxHeartbeats 300000 in
687- lemma assoc_comp {Γ Δ : Grpd} (σ : Δ ⟶ Γ) {A : Γ ⟶ U.Ty} {σA : Δ ⟶ U.Ty} (eq : σ ≫ A = σA)
688- (B : U.ext A ⟶ U.Ty) : (USig.assoc (U.substWk σ A σA eq ≫ B)).hom ≫ U.substWk σ (USig.Sig B)
689- (USig.Sig (U.substWk σ A σA eq ≫ B)) (Sig_comp ..).symm =
690- U.substWk (U.substWk σ A σA eq) B (U.substWk σ A σA eq ≫ B) rfl ≫ (USig.assoc B).hom := by
654+ set_option maxHeartbeats 400000 in
655+ lemma assoc_comp : (assoc (U.substWk σ A σA eq ≫ B)).hom ≫ U.substWk σ (Sig.{v₁,v₂,u} B)
656+ (Sig.{v₁,v₂,u} (U.substWk σ A σA eq ≫ B)) (Sig_comp.{v₁,v₂,u} ..).symm =
657+ U.substWk (U.substWk σ A σA eq) B (U.substWk σ A σA eq ≫ B) rfl ≫ (assoc B).hom := by
691658 dsimp [assoc]
692659 simp only [Sig, SigAux, U.substWk_eq, eqToHom_refl, map_id_eq, Cat.of_α]
693660 rw! (castMode := .all) [toCoreAsSmallEquiv_apply_comp_left]
@@ -697,17 +664,17 @@ lemma assoc_comp {Γ Δ : Grpd} (σ : Δ ⟶ Γ) {A : Γ ⟶ U.Ty} {σA : Δ ⟶
697664 simp only [pre_comp, Functor.id_comp]
698665 apply sigma.assoc_comp' (toCoreAsSmallEquiv B) (σ := σ) (toCoreAsSmallEquiv σA)
699666
700- lemma assoc_disp {Γ : Ctx} {A : Γ ⟶ U.{v}.Ty} (B : U.ext A ⟶ U.Ty) :
701- (USig.assoc B).hom ≫ U.disp (USig.Sig B) = U.disp B ≫ U.disp A := by
667+ lemma assoc_disp : (assoc B).hom ≫ U.disp (Sig.{v₁,v₂,u} B) = U.disp B ≫ U.disp A := by
702668 simpa [assoc] using sigma.assoc_hom_comp_forget _
703669
704670end USig
705671
706672open USig in
707- def USig : PolymorphicSigma U.{v} U.{v} U.{v} :=
708- .mk' Sig Sig_comp assoc assoc_comp assoc_disp
709-
710- end
673+ def USig. {v₁,v₂,u} : PolymorphicSigma
674+ U.{v₁, max u (max v₁ v₂ + 1 )}
675+ U.{v₂, max u (max v₁ v₂ + 1 )}
676+ U.{max v₁ v₂, max u (max v₁ v₂ + 1 )} :=
677+ .mk' Sig.{v₁,v₂,u} Sig_comp assoc assoc_comp assoc_disp
711678
712679end GroupoidModel
713680end
0 commit comments