feat: GroupoidModel polymorphic type formers

HoTTLean/Groupoids/Pi.lean

@@ -558,6 +558,42 @@ end Section
 
 section
 variable {Γ : Type u₂} [Groupoid.{v₂} Γ] (A : Γ ⥤ Grpd.{u₁,u₁}) (B : ∫(A) ⥤ Grpd.{u₁,u₁})
+
+section
+
+def sigma.fstNatTrans : sigma A B ⟶ A where
+  app x := forget
+  naturality x y f:= by simp [sigmaMap_forget]
+
+@[simp]
+lemma sigma.fstNatTrans_app (x) : (fstNatTrans A B).app x = Functor.Groupoidal.forget :=
+  rfl
+
+lemma sigma.map_fstNatTrans_eq : map (fstNatTrans A B) = (assoc B).inv ⋙ forget := by
+  apply Functor.Groupoidal.FunctorTo.hext
+  · simp [Functor.assoc, assoc_inv_comp_forget_comp_forget, map_forget]
+  · intro x
+    simp only [fstNatTrans, map_obj_fiber, sigma_obj, Functor.Groupoidal.forget_obj, assoc,
+      Functor.Iso.symm_inv, Functor.comp_obj, functorIsoFrom_hom_obj, assocFib, heq_eq_eq]
+    rw! (castMode := .all) [pre_obj_base]
+    simp
+    rfl
+  · intro x y f
+    simp only [fstNatTrans, map_map_fiber, sigma_obj, Grpd.comp_eq_comp, Functor.comp_obj,
+      Functor.Groupoidal.forget_obj, sigma_map, sigmaMap_obj_base, eqToHom_refl, forget_map,
+      Category.id_comp, assoc, Functor.Iso.symm_inv, functorIsoFrom_hom_obj, assocFib,
+      Functor.comp_map, functorIsoFrom_hom_map, comp_base, Functor.Groupoidal.comp_fiber,
+      heq_eqToHom_comp_iff]
+    rw! [pre_map_base]
+    simp only [ι_map_base, ι_obj_base, assocHom, assocFib, assocIso, ι_map_fiber, ι_obj_fiber]
+    rw [preNatIso_hom_app_base, ιNatIso_hom, ιNatTrans_app_base]
+    simp only [Functor.comp_obj, Pi.id_apply, homMk_base, homMk_fiber]
+    erw [CategoryTheory.Functor.map_id (A.map (𝟙 y.base))]
+    erw [Category.id_comp]
+    simp
+    rfl
+
+end
 /-- The formation rule for Π-types for the natural model `smallU`
 as operations between functors.
 
@@ -577,7 +613,7 @@ as the induced map in the following diagram
 ```
 -/
 @[simps!] def pi : Γ ⥤ Grpd.{u₁,u₁} := Section.functor (A := A)
-  (B := sigma A B) (sigma.fstNatTrans B)
+  (B := sigma A B) (sigma.fstNatTrans A B)
 
 lemma pi.obj_hext {A A' : Γ ⥤ Grpd.{u₁,u₁}} (hA : A ≍ A') {B : ∫ A ⥤ Grpd.{u₁,u₁}}
     {B' : ∫ A' ⥤ Grpd.{u₁,u₁}} (hB : B ≍ B') (x : Γ)
@@ -638,7 +674,7 @@ namespace pi
 
 section
 
-variable {Γ : Type u₂} [Groupoid.{v₂} Γ] {A : Γ ⥤ Grpd.{u₁,u₁}} (B : ∫(A) ⥤ Grpd.{u₁,u₁})
+variable {Γ : Type u₂} [Groupoid.{v₂} Γ] {A : Γ ⥤ Grpd.{u₁,u₁}} (B : ∫ A ⥤ Grpd.{u₁,u₁})
   (s : Γ ⥤ PGrpd.{u₁,u₁}) (hs : s ⋙ PGrpd.forgetToGrpd = pi A B)
   {Δ : Type u₃} [Groupoid.{v₃} Δ] (σ : Δ ⥤ Γ)
 
@@ -691,7 +727,7 @@ lemma strongTrans.pi_map_map {x y z} (f : x ⟶ y) (g : y ⟶ z) :
     Functor.whiskerLeft (A.map (CategoryTheory.inv g))
     (Functor.whiskerRight (twoCell B s hs f) (sigmaMap B g)) :=
   Section.functor_map_map (A := A)
-    (B := sigma A B) (sigma.fstNatTrans B) g (PGrpd.mapFiber' hs f)
+    (B := sigma A B) (sigma.fstNatTrans A B) g (PGrpd.mapFiber' hs f)
 
 set_option maxHeartbeats 300000 in
 /--
@@ -779,12 +815,12 @@ lemma strongTrans.naturality_comp_hom {x y z : Γ} (g1 : x ⟶ y) (g2 : y ⟶ z)
     erw [Category.id_comp]
 
 lemma strongTrans.app_comp_fstNatTrans_app (x : Γ) :
-    strongTrans.app B s hs x ⋙ (sigma.fstNatTrans B).app x = 𝟭 ↑(A.obj x) := by
+    strongTrans.app B s hs x ⋙ (sigma.fstNatTrans A B).app x = 𝟭 ↑(A.obj x) := by
   simpa [strongTrans.app] using (PGrpd.objFiber' hs x).obj.property
 
 lemma strongTrans.app_map_naturality_hom_app {x y : Γ} (f : x ⟶ y) (a : (A.obj x)) :
-    ((sigma.fstNatTrans B).app y).map (((strongTrans.naturality B s hs) f).hom.app a) =
-    eqToHom (Section.strongTrans_comp_toStrongTrans'_self_aux (sigma.fstNatTrans B)
+    ((sigma.fstNatTrans A B).app y).map (((strongTrans.naturality B s hs) f).hom.app a) =
+    eqToHom (Section.strongTrans_comp_toStrongTrans'_self_aux (sigma.fstNatTrans A B)
       (app B s hs) (app_comp_fstNatTrans_app B s hs) f a) := by
   simp only [sigma_obj, sigma.fstNatTrans, Functor.comp_obj, Functor.Groupoidal.forget_obj,
     sigmaMap_obj_base, naturality, sigma_map, conjugatingObjNatTransEquiv₁, Grpd.Functor.iso,
@@ -873,8 +909,8 @@ lemma assocHom_app_base_fiber
   rfl
 
 lemma mapStrongTrans_comp_map_fstNatTrans :
-    mapStrongTrans B s hs ⋙ map (sigma.fstNatTrans B) = 𝟭 _ := by
-  convert Section.mapStrongTrans_comp_map_self (sigma.fstNatTrans B)
+    mapStrongTrans B s hs ⋙ map (sigma.fstNatTrans A B) = 𝟭 _ := by
+  convert Section.mapStrongTrans_comp_map_self (sigma.fstNatTrans A B)
     (strongTrans.app B s hs) (strongTrans.naturality B s hs)
     (strongTrans.naturality_id_hom B s hs) (strongTrans.naturality_comp_hom B s hs) _ _
   · apply strongTrans.app_comp_fstNatTrans_app
@@ -1655,13 +1691,13 @@ lemma unLam_lam {Γ : Ctx} {A : Γ ⟶ U.{v}.Ty} (B : U.ext A ⟶ U.Ty) (b : U.e
 
 lemma lam_unLam {Γ : Ctx} {A : Γ ⟶ U.{v}.Ty} (B : U.ext A ⟶ U.Ty) (f : Γ ⟶ U.Tm)
     (f_tp : f ≫ U.tp = UPi.Pi B) : UPi.lam (UPi.unLam B f f_tp) = f := by
-  simp [lam, unLam, toCoreAsSmallEquiv.symm_apply_eq]
+  simp only [U_Tm, lam, USig.SigAux, unLam, toCoreAsSmallEquiv.symm_apply_eq]
   erw [toCoreAsSmallEquiv.apply_symm_apply]
   rw [pi.lam_inversion]
 
 end UPi
 
-def UPi : Model.UnstructuredUniverse.PolymorphicPi U.{v} U.{v} U.{v} where
+def UMonomorphicPi : Model.UnstructuredUniverse.PolymorphicPi U.{v} U.{v} U.{v} where
   Pi := UPi.Pi
   Pi_comp := UPi.Pi_comp
   lam _ b _ := UPi.lam b

HoTTLean/Groupoids/Sigma.lean

@@ -1,8 +1,6 @@
 import HoTTLean.Groupoids.UnstructuredModel
 import HoTTLean.ForMathlib.CategoryTheory.RepPullbackCone
 
-universe v u v₁ u₁ v₂ u₂ v₃ u₃
-
 noncomputable section
 
 namespace GroupoidModel
@@ -13,17 +11,22 @@ attribute [local simp] eqToHom_map Grpd.id_eq_id Grpd.comp_eq_comp Functor.id_co
 
 namespace FunctorOperation
 
+/-! We first define Sigma formation as an operation on functors into Grpd. -/
+
+universe v₁ u₁ v₂ u₂ v₃ u₃ v₄ u₄
+
 section
-variable {Γ : Type u₂} [Category.{v₂} Γ] {A : Γ ⥤ Grpd.{v₁,u₁}}
-    (B : ∫ A ⥤ Grpd.{v₁,u₁}) (x : Γ)
+
+variable {Γ : Type u₁} [Category.{v₁} Γ] {A : Γ ⥤ Grpd.{v₂,u₂}} (B : ∫ A ⥤ Grpd.{v₃,u₃})
+
 /--
 For a point `x : Γ`, `(sigma A B).obj x` is the groupoidal Grothendieck
   construction on the composition
   `ι _ x ⋙ B : A.obj x ⥤ Groupoidal A ⥤ Grpd`
 -/
-def sigmaObj : Grpd := Grpd.of (∫ι A x ⋙ B)
+def sigmaObj (x : Γ) : Grpd := Grpd.of (∫ι A x ⋙ B)
 
-variable {x} {y : Γ} (f : x ⟶ y)
+variable {x y : Γ} (f : x ⟶ y)
 /--
 For a morphism `f : x ⟶ y` in `Γ`, `(sigma A B).map y` is a
 composition of functors.
@@ -111,8 +114,7 @@ variable {z : Γ} {f} {g : y ⟶ z}
       ιNatTrans_comp_app, Functor.map_comp, eqToHom_map, Grpd.comp_eq_comp, Grpd.eqToHom_obj, cast_heq_iff_heq, heq_eq_eq]
     aesop_cat
 
-@[simp] theorem sigmaMap_comp_map {A : Γ ⥤ Grpd.{v₁,u₁}}
-    {B : ∫(A) ⥤ Grpd.{v₁,u₁}} {x y z : Γ} {f : x ⟶ y} {g : y ⟶ z}
+@[simp] theorem sigmaMap_comp_map {B : ∫(A) ⥤ Grpd.{v₃,u₃}} {x y z : Γ} {f : x ⟶ y} {g : y ⟶ z}
     {p q : sigmaObj B x} (hpq : p ⟶ q)
     {h1 : (sigmaMap B (f ≫ g)).obj p = (sigmaMap B g).obj ((sigmaMap B f).obj p)}
     {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
   unfolded into operations between functors.
   See `sigmaObj` and `sigmaMap` for the actions of this functor.
  -/
-@[simps] def sigma (A : Γ ⥤ Grpd.{v₁,u₁})
-    (B : ∫(A) ⥤ Grpd.{v₁,u₁}) : Γ ⥤ Grpd.{v₁,u₁} where
+@[simps] def sigma (A : Γ ⥤ Grpd.{v₂,u₂}) (B : ∫(A) ⥤ Grpd.{v₃,u₃}) :
+    Γ ⥤ Grpd.{max v₂ v₃, max u₂ u₃} where
   -- NOTE using Grpd.of here instead of earlier speeds things up
   obj x := sigmaObj B x
   map := sigmaMap B
   map_id _ := sigmaMap_id
   map_comp _ _ := sigmaMap_comp
 
-variable (B) {Δ : Type u₃} [Category.{v₃} Δ] (σ : Δ ⥤ Γ)
+variable (B) {Δ : Type u₄} [Category.{v₄} Δ] (σ : Δ ⥤ Γ)
 theorem sigma_naturality_aux (x) :
     ι (σ ⋙ A) x ⋙ pre A σ ⋙ B = ι A (σ.obj x) ⋙ B := by
   rw [← ι_comp_pre]
@@ -214,8 +216,7 @@ namespace sigma
 
 section
 
-variable {Γ : Type u₂} [Groupoid.{v₂} Γ] {A : Γ ⥤ Grpd.{v₁,u₁}}
-    (B : ∫(A) ⥤ Grpd.{v₁,u₁})
+variable {Γ : Type u₁} [Groupoid.{v₁} Γ] {A : Γ ⥤ Grpd.{v₂,u₂}} (B : ∫(A) ⥤ Grpd.{v₃,u₃})
 
 @[simp] def assocFib (x : Γ) : sigmaObj B x ⥤ ∫(B) :=
   pre _ _
@@ -504,7 +505,7 @@ lemma assoc_inv_map_fiber {x y} (f : x ⟶ y) : ((assoc B).inv.map f).fiber =
   simp [assoc]
   rfl
 
-lemma assocFibMap_pre_pre_map {Δ : Type u₃} [Groupoid.{v₃} Δ] {σ : Δ ⥤ Γ} {x y} (f : x ⟶ y) :
+lemma assocFibMap_pre_pre_map {Δ : Type u₄} [Groupoid.{v₄} Δ] {σ : Δ ⥤ Γ} {x y} (f : x ⟶ y) :
     assocFibMap ((pre B (pre A σ)).map f) ≍ assocFibMap f := by
   have pre_pre_obj_base_base (x) : ((pre B (pre A σ)).obj x).base.base = σ.obj x.base.base := by
     rw [pre_obj_base, pre_obj_base]
@@ -533,7 +534,7 @@ lemma assocFibMap_pre_pre_map {Δ : Type u₃} [Groupoid.{v₃} Δ] {σ : Δ ⥤
     rfl
   · simp
 
-lemma assoc_comp_fiber {Δ : Type u₃} [Groupoid.{v₃} Δ] (σ : Δ ⥤ Γ) {x y} (f : x ⟶ y) :
+lemma assoc_comp_fiber {Δ : Type u₄} [Groupoid.{v₄} Δ] (σ : Δ ⥤ Γ) {x y} (f : x ⟶ y) :
     Hom.fiber (((assoc (pre A σ ⋙ B)).hom ⋙ map (eqToHom (sigma_naturality ..).symm) ⋙
     pre (sigma A B) σ).map f) ≍ Hom.fiber ((pre B (pre A σ) ⋙ (assoc B).hom).map f) := by
   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
   rw! [assocFibMap_pre_pre_map]
   simp
 
-lemma assoc_comp {Δ : Type u₃} [Groupoid.{v₃} Δ] (σ : Δ ⥤ Γ) :
+lemma assoc_comp {Δ : Type u₄} [Groupoid.{v₄} Δ] (σ : Δ ⥤ Γ) :
     (sigma.assoc ((pre A σ) ⋙ B)).hom ⋙
     map (eqToHom (by simp [sigma_naturality])) ⋙ pre (sigma A B) σ =
     pre B (pre A σ) ⋙ (sigma.assoc B).hom := by
@@ -574,62 +575,14 @@ lemma assoc_comp {Δ : Type u₃} [Groupoid.{v₃} Δ] (σ : Δ ⥤ Γ) :
   · intro x y f
     apply assoc_comp_fiber B σ f
 
-lemma assoc_comp' {Δ : Type u₃} [Groupoid.{v₃} Δ] {σ : Δ ⥤ Γ} (Aσ) (eq : Aσ = σ ⋙ A) :
+lemma assoc_comp' {Δ : Type u₄} [Groupoid.{v₄} Δ] {σ : Δ ⥤ Γ} (Aσ) (eq : Aσ = σ ⋙ A) :
     (sigma.assoc ((map (eqToHom eq) ⋙ pre A σ) ⋙ B)).hom ⋙
     map (eqToHom (by subst eq; simp [sigma_naturality, map_id_eq])) ⋙ pre (sigma A B) σ =
     (pre (pre A σ ⋙ B) (map (eqToHom eq)) ⋙ pre B (pre A σ)) ⋙ (sigma.assoc B).hom := by
   subst eq
   rw! [eqToHom_refl, map_id_eq]
   simp [assoc_comp]
 
-section
-
--- def fstAux' : ∫(sigma A B) ⥤ ∫(A) :=
-  -- (assoc B).inv ⋙ forget
-
--- /-- `fst` projects out the pointed groupoid `(A,a)` appearing in `(A,B,a : A,b : B a)` -/
--- def fst : ∫(sigma A B) ⥤ PGrpd :=
---   fstAux' B ⋙ toPGrpd A
-
--- theorem fst_forgetToGrpd : fst B ⋙ PGrpd.forgetToGrpd = forget ⋙ A := by
---   dsimp only [fst, fstAux']
---   rw [Functor.assoc, (Functor.Groupoidal.isPullback A).comm_sq,
---     ← Functor.assoc]
---   conv => left; left; rw [Functor.assoc, assoc_inv_comp_forget_comp_forget]
-
-def fstNatTrans : sigma A B ⟶ A where
-  app x := forget
-  naturality x y f:= by simp [sigmaMap_forget]
-
-@[simp]
-lemma fstNatTrans_app (x) : (fstNatTrans B).app x = Functor.Groupoidal.forget :=
-  rfl
-
-lemma map_fstNatTrans_eq : map (fstNatTrans B) = (assoc B).inv ⋙ forget := by
-  apply Functor.Groupoidal.FunctorTo.hext
-  · simp [Functor.assoc, assoc_inv_comp_forget_comp_forget, map_forget]
-  · intro x
-    simp only [fstNatTrans, map_obj_fiber, sigma_obj, Functor.Groupoidal.forget_obj, assoc,
-      Functor.Iso.symm_inv, Functor.comp_obj, functorIsoFrom_hom_obj, assocFib, heq_eq_eq]
-    rw! (castMode := .all) [pre_obj_base]
-    simp
-    rfl
-  · intro x y f
-    simp only [fstNatTrans, map_map_fiber, sigma_obj, Grpd.comp_eq_comp, Functor.comp_obj,
-      Functor.Groupoidal.forget_obj, sigma_map, sigmaMap_obj_base, eqToHom_refl, forget_map,
-      Category.id_comp, assoc, Functor.Iso.symm_inv, functorIsoFrom_hom_obj, assocFib,
-      Functor.comp_map, functorIsoFrom_hom_map, comp_base, Functor.Groupoidal.comp_fiber,
-      heq_eqToHom_comp_iff]
-    rw! [pre_map_base]
-    simp only [ι_map_base, ι_obj_base, assocHom, assocFib, assocIso, ι_map_fiber, ι_obj_fiber]
-    rw [preNatIso_hom_app_base, ιNatIso_hom, ιNatTrans_app_base]
-    simp only [Functor.comp_obj, Pi.id_apply, homMk_base, homMk_fiber]
-    erw [CategoryTheory.Functor.map_id (A.map (𝟙 y.base))]
-    erw [Category.id_comp]
-    simp
-    rfl
-
-end
 end
 
 end sigma
@@ -638,24 +591,41 @@ end FunctorOperation
 
 open FunctorOperation
 
-section
-
 namespace USig
 
+universe v₁ v₂ u
+
+/-! We now define Sigma on small types (represented as arrows into universes).
+
+Type `A` is `v₁`-sized. Type `B` depending on `A` is `v₂`-sized.
+The context category has to fit `ΣA. B` which is `max v₁ v₂`-sized,
+but it can also be larger.
+Thus the context category is `max u (max v₁ v₂ + 1)`-sized. -/
+
+variable {X : Type (v₂ + 1)} [LargeCategory.{v₂} X]
+  {Y : Type (max v₁ v₂ + 1)} [LargeCategory.{max v₁ v₂} Y]
+
+variable
+  (S : ∀ {Γ : Ctx.{max u (max v₁ v₂ + 1)}} (A : Γ ⥤ Grpd.{v₁,v₁}), (∫(A) ⥤ X) → (Γ ⥤ Y))
+  (S_naturality : ∀ {Γ Δ : Ctx.{max u (max v₁ v₂ + 1)}} (σ : Δ ⟶ Γ) {A : Γ ⥤ Grpd.{v₁,v₁}}
+    {B : ∫(A) ⥤ X}, σ ⋙ S A B = S (σ ⋙ A) (pre A σ ⋙ B))
+  {Γ Δ : Ctx.{max u (max v₁ v₂ + 1)}}
+  (σ : Δ ⟶ Γ)
+  {A : Γ ⟶ U.{v₁, max u (max v₁ v₂ + 1)}.Ty}
+  {σA : Δ ⟶ U.{v₁, max u (max v₁ v₂ + 1)}.Ty}
+  (eq : σ ≫ A = σA)
+  (B : U.ext A ⟶ U.{v₂, max u (max v₁ v₂ + 1)}.Ty)
+
 @[simp]
-abbrev SigAux {X : Type (v + 1)} [Category.{v} X]
-    (S : ∀ {Γ : Ctx} (A : Γ ⥤ Grpd.{v,v}) (B : ∫(A) ⥤ X), Γ ⥤ X)
-    {Γ : Ctx} {A : Γ ⟶ U.{v}.Ty} (B : U.ext A ⟶ Ctx.coreAsSmall X) :
-    Γ ⟶ Ctx.coreAsSmall X :=
+abbrev SigAux
+    (B : U.ext A ⟶ Ctx.coreAsSmall.{v₂, max u (max v₁ v₂ + 1)} X) :
+    Γ ⟶ Ctx.coreAsSmall.{max v₁ v₂, max u (max v₁ v₂ + 1)} Y :=
   toCoreAsSmallEquiv.symm (S (toCoreAsSmallEquiv A) (toCoreAsSmallEquiv B))
 
-theorem SigAux_comp {X : Type (v + 1)} [Category.{v} X]
-    (S : ∀ {Γ : Ctx} (A : Γ ⥤ Grpd.{v,v}) (B : ∫(A) ⥤ X), Γ ⥤ X)
-    (S_naturality : ∀ {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⥤ Grpd}
-      {B : ∫(A) ⥤ X}, σ ⋙ S A B = S (σ ⋙ A) (pre A σ ⋙ B))
-    {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U.{v}.Ty} {σA : Δ ⟶ U.Ty}
-    (eq : σ ≫ A = σA) (B : U.ext A ⟶ Ctx.coreAsSmall X) :
-    SigAux S (U.substWk σ A σA eq ≫ B) = σ ≫ SigAux S B := by
+include S_naturality in
+theorem SigAux_comp
+    (B : U.ext A ⟶ Ctx.coreAsSmall.{v₂, max u (max v₁ v₂ + 1)} X) :
+    SigAux.{v₁,v₂,u} S (U.substWk σ A σA eq ≫ B) = σ ≫ SigAux.{v₁,v₂,u} S B := by
   simp only [SigAux, Grpd.comp_eq_comp]
   rw [← toCoreAsSmallEquiv_symm_apply_comp_left]
   congr 1
@@ -667,27 +637,24 @@ theorem SigAux_comp {X : Type (v + 1)} [Category.{v} X]
   simp [U.substWk_eq, map_id_eq]
   rfl
 
-def Sig {Γ : Ctx} {A : Γ ⟶ U.{v}.Ty} (B : U.ext A ⟶ U.{v}.Ty) : Γ ⟶ U.{v}.Ty :=
-  SigAux sigma B
+def Sig : Γ ⟶ U.{max v₁ v₂, max u (max v₁ v₂ + 1)}.Ty :=
+  SigAux.{v₁,v₂,u} sigma B
 
 /--
 Naturality for the formation rule for Σ-types.
 Also known as Beck-Chevalley.
 -/
-theorem Sig_comp {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U.{v}.Ty} {σA : Δ ⟶ U.Ty}
-    (eq : σ ≫ A = σA) (B : U.ext A ⟶ U.{v}.Ty) :
-    Sig (U.substWk σ A σA eq ≫ B) = σ ≫ Sig B :=
-  SigAux_comp sigma (by intros; rw [sigma_naturality]) σ eq B
+theorem Sig_comp : Sig.{v₁,v₂,u} (U.substWk σ A σA eq ≫ B) = σ ≫ Sig.{v₁,v₂,u} B :=
+  SigAux_comp.{v₁,v₂,u} sigma (by intros; rw [sigma_naturality]) σ eq B
 
-def assoc {Γ : Ctx} {A : Γ ⟶ U.{v}.Ty} (B : U.ext A ⟶ U.Ty) : U.ext B ≅ U.ext (USig.Sig B) :=
+def assoc : U.ext B ≅ U.ext (Sig.{v₁,v₂,u} B) :=
   Grpd.mkIso' (sigma.assoc (toCoreAsSmallEquiv B)) ≪≫
     eqToIso (by dsimp [U.ext, Sig]; rw [toCoreAsSmallEquiv.apply_symm_apply])
 
-set_option maxHeartbeats 300000 in
-lemma assoc_comp {Γ Δ : Grpd} (σ : Δ ⟶ Γ) {A : Γ ⟶ U.Ty} {σA : Δ ⟶ U.Ty} (eq : σ ≫ A = σA)
-    (B : U.ext A ⟶ U.Ty) : (USig.assoc (U.substWk σ A σA eq ≫ B)).hom ≫ U.substWk σ (USig.Sig B)
-    (USig.Sig (U.substWk σ A σA eq ≫ B)) (Sig_comp ..).symm =
-    U.substWk (U.substWk σ A σA eq) B (U.substWk σ A σA eq ≫ B) rfl ≫ (USig.assoc B).hom := by
+set_option maxHeartbeats 400000 in
+lemma assoc_comp : (assoc (U.substWk σ A σA eq ≫ B)).hom ≫ U.substWk σ (Sig.{v₁,v₂,u} B)
+    (Sig.{v₁,v₂,u} (U.substWk σ A σA eq ≫ B)) (Sig_comp.{v₁,v₂,u} ..).symm =
+    U.substWk (U.substWk σ A σA eq) B (U.substWk σ A σA eq ≫ B) rfl ≫ (assoc B).hom := by
   dsimp [assoc]
   simp only [Sig, SigAux, U.substWk_eq, eqToHom_refl, map_id_eq, Cat.of_α]
   rw! (castMode := .all) [toCoreAsSmallEquiv_apply_comp_left]
@@ -697,17 +664,17 @@ lemma assoc_comp {Γ Δ : Grpd} (σ : Δ ⟶ Γ) {A : Γ ⟶ U.Ty} {σA : Δ ⟶
   simp only [pre_comp, Functor.id_comp]
   apply sigma.assoc_comp' (toCoreAsSmallEquiv B) (σ := σ) (toCoreAsSmallEquiv σA)
 
-lemma assoc_disp {Γ : Ctx} {A : Γ ⟶ U.{v}.Ty} (B : U.ext A ⟶ U.Ty) :
-    (USig.assoc B).hom ≫ U.disp (USig.Sig B) = U.disp B ≫ U.disp A := by
+lemma assoc_disp : (assoc B).hom ≫ U.disp (Sig.{v₁,v₂,u} B) = U.disp B ≫ U.disp A := by
   simpa [assoc] using sigma.assoc_hom_comp_forget _
 
 end USig
 
 open USig in
-def USig : PolymorphicSigma U.{v} U.{v} U.{v} :=
-  .mk' Sig Sig_comp assoc assoc_comp assoc_disp
-
-end
+def USig.{v₁,v₂,u} : PolymorphicSigma
+    U.{v₁, max u (max v₁ v₂ + 1)}
+    U.{v₂, max u (max v₁ v₂ + 1)}
+    U.{max v₁ v₂, max u (max v₁ v₂ + 1)} :=
+  .mk' Sig.{v₁,v₂,u} Sig_comp assoc assoc_comp assoc_disp
 
 end GroupoidModel
 end