[WIP] feat: CategoryTheory.RepMap.Universe

GroupoidModel/CwRGroupoids/Basic.lean

@@ -0,0 +1,168 @@
+import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
+import Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
+import Mathlib.CategoryTheory.Category.Cat.Limit
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
+
+import GroupoidModel.ForMathlib.CategoryTheory.Core
+import GroupoidModel.RepresentableMap.Universe
+import GroupoidModel.Grothendieck.Groupoidal.IsPullback
+
+/-!
+Here we construct universes for the groupoid natural model.
+-/
+
+universe w v u v₁ u₁ v₂ u₂ v₃ u₃
+
+noncomputable section
+
+open CategoryTheory ULift Functor Groupoidal
+  Limits MorphismProperty Universe CategoryTheory.Functor
+
+namespace CategoryTheory.PGrpd
+def pGrpdToGroupoidalAsSmallFunctor : PGrpd.{v, v} ⥤
+    ∫(Grpd.asSmallFunctor.{max w (v+1), v, v}) :=
+  Grothendieck.functorTo PGrpd.forgetToGrpd
+  (fun x => AsSmall.up.obj.{v, v, max w (v + 1)} x.fiber)
+  (fun f => AsSmall.up.map f.fiber)
+  (by aesop_cat)
+  (by aesop_cat)
+
+def groupoidalAsSmallFunctorToPGrpd :
+    ∫(Grpd.asSmallFunctor.{max w (v+1), v, v}) ⥤ PGrpd.{v,v} :=
+  PGrpd.functorTo Groupoidal.forget
+  (fun x => AsSmall.down.obj.{v, v, max w (v + 1)} x.fiber)
+  (fun f => AsSmall.down.map f.fiber)
+  (by aesop_cat)
+  (by aesop_cat)
+
+@[simp] def pGrpdToGroupoidalAsSmallFunctor_groupoidalAsSmallFunctorToPGrpd :
+    groupoidalAsSmallFunctorToPGrpd ⋙ pGrpdToGroupoidalAsSmallFunctor = 𝟭 _ :=
+  rfl
+
+@[simp] def groupoidalAsSmallFunctorToPGrpd_pGrpdToGroupoidalAsSmallFunctor :
+    pGrpdToGroupoidalAsSmallFunctor ⋙ groupoidalAsSmallFunctorToPGrpd = 𝟭 _ :=
+  rfl
+
+@[simp] def pGrpdToGroupoidalAsSmallFunctor_forget : pGrpdToGroupoidalAsSmallFunctor
+    ⋙ Groupoidal.forget = PGrpd.forgetToGrpd :=
+  rfl
+
+def asSmallFunctor : PGrpd.{v, v} ⥤ PGrpd.{max w (v+1), max w (v+1)} :=
+  pGrpdToGroupoidalAsSmallFunctor ⋙
+  toPGrpd Grpd.asSmallFunctor.{max w (v+1), v, v}
+
+end CategoryTheory.PGrpd
+
+namespace GroupoidModel
+
+/--
+Ctx is
+the category of
+{small groupoids - size u objects and size u hom sets}
+which itself has size u+1 objects (small groupoids)
+and size u hom sets (functors).
+-/
+@[reducible]
+def Ctx := Grpd.{u,u}
+
+instance : CartesianMonoidalCategory Ctx := inferInstanceAs (CartesianMonoidalCategory Grpd)
+
+instance : HasFiniteLimits Grpd.{u,u} := sorry
+
+instance : HasFiniteLimits Ctx := inferInstanceAs (HasFiniteLimits Grpd)
+
+namespace Ctx
+
+def coreAsSmall (C : Type (v+1)) [Category.{v} C] : Ctx.{max u (v+1)} :=
+  Grpd.of (Core (AsSmall C))
+
+def coreAsSmallFunctor {C : Type (v+1)} [Category.{v} C] {D : Type (w+1)} [Category.{w} D]
+    (F : C ⥤ D) : coreAsSmall.{v, max u (v+1) (w+1)} C
+    ⟶ coreAsSmall.{w, max u (v+1) (w+1)} D :=
+  Grpd.homOf $ Functor.core $ AsSmall.down ⋙ F ⋙ AsSmall.up
+
+end Ctx
+
+open Ctx
+
+section
+
+variable {Γ Δ : Type u} [Groupoid Γ] [Groupoid Δ] (σ : Δ ⥤ Γ) {C : Type (v+1)} [Category.{v} C]
+    {D : Type (v+1)} [Category.{v} D]
+
+def toCoreAsSmallEquiv : (Γ ⥤ coreAsSmall C) ≃ Γ ⥤ C :=
+  Core.functorToCoreEquiv.symm.trans functorToAsSmallEquiv
+
+theorem toCoreAsSmallEquiv_apply_comp_left (A : Γ ⥤ coreAsSmall C) :
+    toCoreAsSmallEquiv (σ ⋙ A) = σ ⋙ toCoreAsSmallEquiv A := by
+  rfl
+
+theorem toCoreAsSmallEquiv_apply_comp_right (A : Γ ⥤ coreAsSmall C) (F : C ⥤ D) :
+    toCoreAsSmallEquiv (A ⋙ coreAsSmallFunctor F) = toCoreAsSmallEquiv A ⋙ F := by
+  rfl
+
+theorem toCoreAsSmallEquiv_symm_apply_comp_left (A : Γ ⥤ C) :
+    toCoreAsSmallEquiv.symm (σ ⋙ A) = σ ⋙ toCoreAsSmallEquiv.symm A := by
+  dsimp only [toCoreAsSmallEquiv, Equiv.symm_trans_apply, Equiv.symm_symm, Grpd.comp_eq_comp]
+  erw [functorToAsSmallEquiv_symm_apply_comp_left, Core.functorToCoreEquiv_apply,
+    Core.functorToCore_comp_left]
+  rfl
+
+theorem toCoreAsSmallEquiv_symm_apply_comp_right (A : Γ ⥤ C) (F : C ⥤ D) :
+    toCoreAsSmallEquiv.symm (A ⋙ F) = toCoreAsSmallEquiv.symm A ⋙ coreAsSmallFunctor F := by
+  rfl
+
+end
+
+namespace U
+
+/-- `Ty.{v}` is the object representing the
+  universe of `v`-small types. -/
+def Ty : Ctx := coreAsSmall Grpd.{v,v}
+
+/-- `Tm.{v}` is the object representing `v`-small terms,
+  living over `Ty.{v}`. -/
+def Tm : Ctx := coreAsSmall PGrpd.{v,v}
+
+/-- `tp.{v}` is the morphism representing `v`-small `tp`,
+  for the universe `U`. -/
+def tp : Tm.{v} ⟶ Ty.{v} :=
+  coreAsSmallFunctor PGrpd.forgetToGrpd
+
+variable {Γ : Ctx} (A : Γ ⟶ Ty.{v})
+
+def ext : Ctx := Grpd.of (∫ toCoreAsSmallEquiv A)
+
+@[reducible, simp]
+def disp : ext A ⟶ Γ := forget
+
+def var : ext A ⟶ Tm.{v} :=
+  toCoreAsSmallEquiv.symm (toPGrpd (toCoreAsSmallEquiv A))
+
+/-- `liftTy` is the base map between two `v`-small universes
+               toE
+    E.{v} --------------> E.{v+1}
+    |                      |
+    |                      |
+  π |                      | π
+    |                      |
+    v                      v
+    Ty.{v}----liftTy-----> Ty.{v+1}
+ -/
+def liftTy : Ty.{v, max u (v+2)} ⟶ Ty.{v+1, max u (v+2)} :=
+  coreAsSmallFunctor.{v+1,v} Grpd.asSmallFunctor.{v+1}
+
+def liftTm : Tm.{v, max u (v+2)} ⟶ Tm.{v+1,max u (v+2)} :=
+  coreAsSmallFunctor.{v+1,v} PGrpd.asSmallFunctor.{v+1}
+
+end U
+
+def Ctx.IsIsofibration : MorphismProperty Ctx := Grpd.IsIsofibration
+
+instance : IsIsofibration.RepresentableMap where
+  __ := rlp_isStableUnderBaseChange _
+  exponentiableMorphism := sorry
+
+end GroupoidModel
+
+end

GroupoidModel/CwRGroupoids/IsPullback.lean

@@ -0,0 +1,216 @@
+import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
+import Mathlib.CategoryTheory.Category.Cat.Limit
+
+import GroupoidModel.Grothendieck.Groupoidal.IsPullback
+import GroupoidModel.CwRGroupoids.Basic
+
+/-!
+Here we construct universes for the groupoid natural model.
+
+-- TODO: flip all the diagrams in this file
+-/
+
+universe w v u v₁ u₁ v₂ u₂ v₃ u₃
+
+noncomputable section
+open CategoryTheory ULift Functor.Groupoidal
+  Limits GroupoidModel.Ctx GroupoidModel.U PGrpd
+
+namespace GroupoidModel
+namespace IsPullback
+
+def liftTy' : AsSmall.{max u (v+2)} Grpd.{v,v}
+    ⥤ AsSmall.{max u (v+2)} Grpd.{v+1,v+1} :=
+  AsSmall.down ⋙ Grpd.asSmallFunctor.{v+1} ⋙ AsSmall.up
+
+def liftTm' : AsSmall.{max u (v+2)} PGrpd.{v,v}
+    ⥤ AsSmall.{max u (v+2)} PGrpd.{v+1,v+1} :=
+  AsSmall.down ⋙ PGrpd.asSmallFunctor.{v+1} ⋙ AsSmall.up
+
+def tp' : AsSmall.{max u (v+1)} PGrpd.{v,v}
+    ⥤ AsSmall.{max u (v+1)} Grpd.{v,v} :=
+  AsSmall.down ⋙ PGrpd.forgetToGrpd ⋙ AsSmall.up
+
+theorem liftTm'_tp' : Cat.homOf liftTm'.{v,u} ≫ Cat.homOf tp'.{v+1, max u (v+2)} =
+  Cat.homOf tp'.{v, max u (v+2)} ≫ Cat.homOf liftTy'.{v,u} := rfl
+
+/--
+The following square is a meta-theoretic pullback
+
+PGrpd.{v} ------- asSmallFunctor ------> PGrpd.{v+1}
+    |                                     |
+    |                                     |
+forgetToGrpd                        forgetToGrpd
+    |                                     |
+    |                                     |
+    v                                     v
+Grpd.{v}  ------- asSmallFunctor ----->  Grpd.{v+1}
+
+-/
+def isPullback_forgetToGrpd_forgetToGrpd :
+  Functor.IsPullback
+    PGrpd.asSmallFunctor.{v+1}
+    PGrpd.forgetToGrpd.{v}
+    PGrpd.forgetToGrpd.{v+1}
+    Grpd.asSmallFunctor.{v+1} :=
+  Functor.IsPullback.ofIso (toPGrpd _) forget PGrpd.forgetToGrpd.{v+1}
+  Grpd.asSmallFunctor.{v+1} (isPullback _)
+  PGrpd.pGrpdToGroupoidalAsSmallFunctor
+  PGrpd.groupoidalAsSmallFunctorToPGrpd
+  PGrpd.groupoidalAsSmallFunctorToPGrpd_pGrpdToGroupoidalAsSmallFunctor
+  PGrpd.pGrpdToGroupoidalAsSmallFunctor_groupoidalAsSmallFunctorToPGrpd
+
+/--
+The following square is a pullback
+
+ AsSmall PGrpd.{v} ------- liftTm' ------> AsSmall PGrpd.{v+1}
+        |                                     |
+        |                                     |
+        tp'                                   tp'
+        |                                     |
+        |                                     |
+        v                                     v
+ AsSmall Grpd.{v}  ------- liftTy' -----> AsSmall Grpd.{v+1}
+
+in the category `Cat.{max u (v+2), max u (v+2)}`.
+Note that these `AsSmall`s are bringing two different sized
+categories into the same category.
+-/
+def isPullback_liftTm' : Functor.IsPullback
+    liftTm'.{v,max u (v+2)}
+    tp'.{_,max u (v+2)}
+    tp'.{v+1,max u (v+2)}
+    liftTy'.{v,max u (v+2)} :=
+  Functor.IsPullback.ofIso' PGrpd.asSmallFunctor.{v+1} PGrpd.forgetToGrpd.{v}
+    PGrpd.forgetToGrpd.{v+1} Grpd.asSmallFunctor.{v+1} isPullback_forgetToGrpd_forgetToGrpd
+    liftTm'.{v,max u (v+2)} tp'.{_,max u (v+2)} tp'.{v+1,max u (v+2)} liftTy'.{v,max u (v+2)}
+    AsSmall.downIso AsSmall.downIso AsSmall.downIso AsSmall.downIso rfl rfl rfl rfl
+
+theorem isPullback_liftTm'_in_Cat : IsPullback
+    (Cat.homOf liftTm'.{v,max u (v+2)})
+    tp'.{_,max u (v+2)}
+    tp'.{v+1,max u (v+2)}
+    (Cat.homOf liftTy'.{v,max u (v+2)}) :=
+  Cat.isPullback isPullback_liftTm'
+
+/--
+The small universes form pullbacks
+      Tm.{v} ------------ liftTm ---------> Tm.{v+1}
+        |                                     |
+        |                                     |
+      tp.{v}                                tp.{v+1}
+        |                                     |
+        v                                     v
+      Ty.{v} ------------ liftTy ---------> Ty.{v+1}
+-/
+theorem liftTm_isPullback : IsPullback U.tp.{v, max u (v+2)} liftTm.{v,max u (v+2)}
+    liftTy.{v,max u (v+2)} U.tp.{v+1, max u (v+2)} := by
+  apply IsPullback.flip
+  convert Functor.map_isPullback Core.map isPullback_liftTm'_in_Cat.{v,u}
+
+variable {Γ : Ctx} (A : Γ ⥤ Grpd)
+
+/--
+∫ toCor...iv A ----> PGrpd
+     |                  |
+     |                  |
+     |                  |
+     V                  V
+     Γ ------------> Grpd
+-/
+def isPullbackClassifier :
+    Functor.IsPullback (toPGrpd A) Functor.Groupoidal.forget
+    forgetToGrpd A :=
+  Functor.Groupoidal.isPullback A
+
+/--
+  AsSmall PGrpd ----> PGrpd
+     |                  |
+     |                  |
+     |                  |
+     V                  V
+  AsSmall Grpd ------> Grpd
+-/
+def isPullbackAsSmall :
+    Functor.IsPullback AsSmall.down (AsSmall.down ⋙ PGrpd.forgetToGrpd ⋙ AsSmall.up)
+    PGrpd.forgetToGrpd AsSmall.down :=
+  CategoryTheory.AsSmall.isPullback _
+
+/--
+∫ toCore...iv A ----> AsSmall PGrpd
+     |                  |
+     |                  |
+     |                  |
+     V                  V
+     Γ ------------> AsSmall Grpd
+-/
+def isPullbackClassifierOfAsSmall :
+    Functor.IsPullback (functorToAsSmallEquiv.symm (toPGrpd A))
+    Functor.Groupoidal.forget (AsSmall.down ⋙ PGrpd.forgetToGrpd ⋙ AsSmall.up)
+    (functorToAsSmallEquiv.symm A) :=
+  Functor.IsPullback.Paste.ofRight
+    (by simp [functorToAsSmallEquiv, ← Functor.assoc, ← toPGrpd_forgetToGrpd]; rfl)
+    (by rfl) isPullbackAsSmall
+    (isPullbackClassifier A)
+
+/--
+coreAsSmall PGrpd ----> AsSmall PGrpd
+     |                   |
+     |                   |
+     |                   |
+     V                   V
+coreAsSmall Grpd -----> AsSmall Grpd
+-/
+
+def isPullbackCoreAsSmall :
+    Functor.IsPullback (Core.inclusion _) (Ctx.coreAsSmallFunctor PGrpd.forgetToGrpd)
+    (AsSmall.down ⋙ PGrpd.forgetToGrpd ⋙ AsSmall.up) (Core.inclusion _) :=
+  Core.isPullback_map'_self _
+
+/--
+∫ toCo...iv A ----> coreAsSmall PGrpd
+     |                  |
+     |                  |
+     |                  |
+     V                  V
+     Γ ------------> coreAsSmall Grpd
+-/
+def isPullbackClassifierOfCoreAsSmall (A : Γ ⟶ Ty) :
+    Functor.IsPullback (var A) forget tp (toCoreAsSmallEquiv.symm (toCoreAsSmallEquiv A)) :=
+  Functor.IsPullback.Paste.ofRight' (so := toCoreAsSmallEquiv.symm (toCoreAsSmallEquiv A))
+  (by
+    dsimp [functorToAsSmallEquiv]
+    convert_to (toPGrpd (toCoreAsSmallEquiv A) ⋙ forgetToGrpd) ⋙ AsSmall.up = _
+    erw [toPGrpd_forgetToGrpd, Core.functorToCoreEquiv_apply, Core.functorToCore_comp_inclusion,
+      Functor.assoc])
+  (isPullbackClassifierOfAsSmall (toCoreAsSmallEquiv A))
+  (by
+    dsimp [Ctx.coreAsSmallFunctor, Grpd.homOf]
+    rw [Core.core_comp_inclusion])
+  isPullbackCoreAsSmall (var A)
+  (by
+    apply (isPullbackCoreAsSmall).lift_uniq
+    · simp only [U.var, toCoreAsSmallEquiv, Equiv.symm_trans_apply, Equiv.symm_symm]
+      erw [Core.functorToCoreEquiv_apply, Core.functorToCore_comp_inclusion]
+      rfl
+    · rw [U.var, ← toCoreAsSmallEquiv_symm_apply_comp_left,
+        ← toCoreAsSmallEquiv_symm_apply_comp_right, toPGrpd_forgetToGrpd])
+
+/--
+  The following square is a pullback in `Ctx`
+  Ty.ext A --- Ty.var A ---> Tm
+     |                     |
+     |                     |
+     |                     |
+  Ty.disp A                 tp
+     |                     |
+     |                     |
+     V                     V
+     Γ --------- A ------> Ty
+-/
+theorem disp_pullback (A : Γ ⟶ Ty) : IsPullback (var A) forget tp A := by
+  convert Grpd.isPullback (isPullbackClassifierOfCoreAsSmall A)
+  simp
+
+end IsPullback
+end GroupoidModel