feat: GroupoidModel polymorphic type formers #166

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged

Vtec234 merged 15 commits into master from poly-sigma

Nov 10, 2025

HoTTLean/Groupoids/Pi.lean

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -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

-Original file line number
+Diff line change
@@ -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
@@ Expand All @@
     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.
@@ Expand Down Expand Up / @@ -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}
@@ Expand Down Expand Up @@
       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]
@@ Expand Down Expand Up / @@ -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 _ _
@@ Expand Down Expand Up @@
       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]
@@ Expand Down Expand Up @@
         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,
@@ Expand All @@
       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
@@ Expand Down Expand Up @@
       · 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
@@ Expand All / @@ -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
@@ Expand All / @@ -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]
@@ Expand All @@
       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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: GroupoidModel polymorphic type formers #166

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!