chore: bump Poly (#77)

Vtec234 · web-flow · commit 195abfad6c97 · 2025-03-26T11:48:32.000-04:00
* chore: bump Poly

* chore: use new simp rules
diff --git a/GroupoidModel.lean b/GroupoidModel.lean
@@ -1,9 +1,7 @@
 -- This module serves as the root of the `GroupoidModelInLean4` library.
 -- Import modules here that should be built as part of the library.
-import GroupoidModel.Tarski.NaturalModel
 import GroupoidModel.Russell_PER_MS.UHom
 import GroupoidModel.Russell_PER_MS.Interpretation
-import GroupoidModel.Groupoids.TarskiNaturalModel
 import GroupoidModel.Groupoids.NaturalModelBase
 
 /- There should be at least three separate files here for three separate developments:
diff --git a/GroupoidModel/ForMathlib.lean b/GroupoidModel/ForMathlib.lean
@@ -28,8 +28,6 @@ or redesigned.
 
 namespace CategoryTheory
 
-attribute [reassoc (attr := simp)] Limits.terminal.comp_from
-attribute [reassoc (attr := simp)] Limits.initial.to_comp
 attribute [reassoc (attr := simp)] Limits.IsTerminal.comp_from
 attribute [reassoc (attr := simp)] Limits.IsInitial.to_comp
 
@@ -781,9 +779,9 @@ def Equiv.psigmaCongrProp {α₁ α₂} {β₁ : α₁ → Prop} {β₂ : α₂
 
 namespace CategoryTheory.Limits
 
-variable {𝒞 : Type u} [Category.{v} 𝒞] [HasPullbacks 𝒞]
+variable {𝒞 : Type u} [Category.{v} 𝒞]
 
-noncomputable def pullbackHomEquiv {A B C: 𝒞} {Γ : 𝒞} {f : A ⟶ C} {g : B ⟶ C} :
+noncomputable def pullbackHomEquiv {A B C: 𝒞} {Γ : 𝒞} {f : A ⟶ C} {g : B ⟶ C} [HasPullback f g] :
     (Γ ⟶ pullback f g) ≃
     (fst : Γ ⟶ A) × (snd : Γ ⟶ B) ×' (fst ≫ f = snd ≫ g) where
   toFun h := ⟨h ≫ pullback.fst f g, h ≫ pullback.snd f g, by simp[pullback.condition]⟩
diff --git a/GroupoidModel/ForPoly.lean b/GroupoidModel/ForPoly.lean
@@ -1,68 +1,42 @@
-import Poly.UvPoly
-import Poly.LCCC.Presheaf
-import Poly.LCCC.Basic
+import Poly.UvPoly.Basic
 import GroupoidModel.ForMathlib
 
 open CategoryTheory Limits
 
 noncomputable section
 
-namespace UvPoly
+namespace CategoryTheory.UvPoly
 
 variable {𝒞} [Category 𝒞] [HasTerminal 𝒞] [HasPullbacks 𝒞]
 
 variable {E B : 𝒞} (P : UvPoly E B) (A : 𝒞)
 
--- TODO (JH) make issue
-theorem pair_proj {Γ} (b : Γ ⟶ B) (e : pullback b P.p ⟶ A) :
-    P.pairPoly b e ≫ P.proj _ = b := by
-  sorry
-
-def genPb.snd : P.genPb A ⟶ E :=
-  pullback.snd (f := P.proj A) (g := P.p)
-
-variable {A}
-theorem genPb.condition :
-    genPb.snd P A ≫ P.p = genPb.fst P A ≫ P.proj A := by
-  simp [genPb.fst,genPb.snd,pullback.condition]
-
 def compDomEquiv {Γ E B D A : 𝒞} {P : UvPoly E B} {Q : UvPoly D A} :
-    (Γ ⟶ compDom P Q)
-    ≃ (AB : Γ ⟶ P.functor.obj A) × (α : Γ ⟶ E) × (β : Γ ⟶ D)
-    ×' (h : AB ≫ P.proj A = α ≫ P.p)
-    ×' (β ≫ Q.p = pullback.lift AB α h ≫ genPb.u₂ P A) :=
+    (Γ ⟶ compDom P Q) ≃
+      (AB : Γ ⟶ P.functor.obj A) × (α : Γ ⟶ E) × (β : Γ ⟶ D) ×'
+      (w : AB ≫ P.fstProj A = α ≫ P.p) ×'
+      (β ≫ Q.p = pullback.lift AB α w ≫ (PartialProduct.fan P A).snd) :=
   calc
-  _ ≃ (β : Γ ⟶ D) × (αB : Γ ⟶ genPb P A)
-  ×' (β ≫ Q.p = αB ≫ genPb.u₂ P A) := pullbackHomEquiv
-  _ ≃ (β : Γ ⟶ D) × (αB : (AB : Γ ⟶ P.functor.obj A) × (α : Γ ⟶ E) ×' AB ≫ P.proj A = α ≫ P.p) ×'
-      β ≫ Q.p = pullback.lift αB.1 αB.2.1 αB.2.2 ≫ genPb.u₂ P A :=
-    Equiv.sigmaCongrRight (fun β =>
-    calc
-    _ ≃
-    (αB : (AB : Γ ⟶ P.functor.obj A)
-    × (α : Γ ⟶ E)
-    ×' (AB ≫ P.proj A = α ≫ P.p))
-    ×' (β ≫ Q.p = pullback.lift αB.1 αB.2.1 αB.2.2 ≫ genPb.u₂ P A) :=
-      Equiv.psigmaCongrProp pullbackHomEquiv (fun αB => by
-        apply Eq.congr_right
-        congr 1
-        apply pullback.hom_ext
-        · simp [pullbackHomEquiv]
-        · simp [pullbackHomEquiv]))
+  _ ≃ (β : Γ ⟶ D) × (αB : Γ ⟶ pullback (PartialProduct.fan P A).fst P.p) ×'
+      β ≫ Q.p = αB ≫ (PartialProduct.fan P A).snd :=
+    pullbackHomEquiv
+  _ ≃ (β : Γ ⟶ D) × (αB : (AB : Γ ⟶ P.functor.obj A) × (α : Γ ⟶ E) ×'
+        AB ≫ P.fstProj A = α ≫ P.p) ×'
+      β ≫ Q.p = pullback.lift αB.1 αB.2.1 αB.2.2 ≫ (PartialProduct.fan P A).snd :=
+    Equiv.sigmaCongrRight (fun β => calc
+      _ ≃ (αB : (AB : Γ ⟶ P.functor.obj A) × (α : Γ ⟶ E) ×' (AB ≫ P.fstProj A = α ≫ P.p)) ×'
+          (β ≫ Q.p = pullback.lift αB.1 αB.2.1 αB.2.2 ≫ (PartialProduct.fan P A).snd) :=
+        Equiv.psigmaCongrProp pullbackHomEquiv (fun αB => by
+          apply Eq.congr_right
+          congr 1
+          apply pullback.hom_ext
+          · simp [pullbackHomEquiv]
+          · simp [pullbackHomEquiv]))
   _ ≃ _ := {
       -- TODO should be general tactic for this?
       toFun x := ⟨ x.2.1.1, x.2.1.2.1 , x.1 , x.2.1.2.2, x.2.2 ⟩
       invFun x := ⟨ x.2.2.1 , ⟨ x.1, x.2.1 , x.2.2.2.1 ⟩ , x.2.2.2.2 ⟩
       left_inv _ := rfl
       right_inv _ := rfl }
 
-end UvPoly
-
-variable {𝒞 : Type*} [SmallCategory 𝒞] [HasTerminal 𝒞]
-
-instance : LCC (Psh 𝒞) :=
-  @LCCC.mkOfOverCC _ _ _ ⟨CategoryOfElements.presheafOverCCC⟩
-
-instance {X Y : Psh 𝒞} (f : X ⟶ Y) : CartesianExponentiable f where
-  functor := LCC.pushforward f
-  adj := LCC.adj _
+end CategoryTheory.UvPoly
diff --git a/GroupoidModel/Grothendieck/Groupoidal.lean b/GroupoidModel/Grothendieck/Groupoidal.lean
@@ -311,7 +311,7 @@ theorem var'_uLiftToPCat :
 
 theorem var'_forget :
     var' A ≫ (uLiftGrothendieckForget (Grpd.forgetToCat.{u,u}))
-    = uLiftGrothendieckForget (Groupoid.compForgetToCat.{u} A) ≫ uLiftA A := 
+    = uLiftGrothendieckForget (Groupoid.compForgetToCat.{u} A) ≫ uLiftA A :=
   (Grothendieck.isPullback (Grpd.forgetToCat.{u,u})).lift_snd
     (IsPullback.uLiftToPCat (Groupoid.compForgetToCat.{u} A)) ((IsPullback.uLiftGrothendieckForget (Groupoid.compForgetToCat.{u} A)) ≫ uLiftA A)
     (Grothendieck.isPullback (Groupoid.compForgetToCat.{u} A)).cone.condition_one
@@ -338,7 +338,7 @@ by pullback pasting
         ↑Γ----------------------> ↑Grpd.{u,u} ----------------> ↑Cat.{u,u}
 -/
 theorem
-  isPullback_uLiftGrothendieckForget_Groupoid.compForgetToCat_uLiftGrothendieckForget_grpdForgetToCat : 
+  isPullback_uLiftGrothendieckForget_Groupoid.compForgetToCat_uLiftGrothendieckForget_grpdForgetToCat :
     IsPullback
     (Cat.homOf (var' A))
     (IsPullback.uLiftGrothendieckForget (Groupoid.compForgetToCat.{u} A))
diff --git a/GroupoidModel/Russell_PER_MS/NaturalModelBase.lean b/GroupoidModel/Russell_PER_MS/NaturalModelBase.lean
@@ -1,3 +1,5 @@
+import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Presheaf
+import Poly.UvPoly.UPFan
 import GroupoidModel.ForPoly
 
 universe v u
@@ -191,17 +193,7 @@ theorem inst_wk {Γ : Ctx} {X : Psh Ctx}
 
 variable (M : NaturalModelBase Ctx)
 
--- TODO(WN): move to ForMathlib or somewhere
-instance : HasFiniteWidePullbacks (Psh Ctx) := hasFiniteWidePullbacks_of_hasFiniteLimits _
-
-instance : LCC (Psh Ctx) := @LCCC.mkOfOverCC _ _ _ ⟨CategoryOfElements.presheafOverCCC⟩
-
-instance {Tm Ty : Psh Ctx} (tp : Tm ⟶ Ty) : CartesianExponentiable tp where
-  functor := LCC.pushforward tp
-  adj := LCC.adj _
-
 @[simps] def uvPolyTp : UvPoly M.Tm M.Ty := ⟨M.tp, inferInstance⟩
-def uvPolyTpT : UvPoly.Total (Psh Ctx) := ⟨_, _, M.uvPolyTp⟩
 def Ptp : Psh Ctx ⥤ Psh Ctx := M.uvPolyTp.functor
 
 -- TODO: establish a profunctor iso to replace `P_equiv` here.
diff --git a/GroupoidModel/Russell_PER_MS/NaturalModelSigma.lean b/GroupoidModel/Russell_PER_MS/NaturalModelSigma.lean
@@ -38,7 +38,7 @@ def uvPolyTpEquiv {Γ : Ctx} {X : Psh Ctx} :
 
 @[simp] theorem uvPolyTpEquiv_fst {Γ : Ctx} {X : Psh Ctx}
     (AB : y(Γ) ⟶ M.uvPolyTp.functor.obj X) :
-    (M.uvPolyTpEquiv AB).1 = AB ≫ M.uvPolyTp.proj _ :=
+    (M.uvPolyTpEquiv AB).1 = AB ≫ M.uvPolyTp.fstProj _ :=
   rfl
 
 @[simp] theorem uvPolyTpEquiv_symm_snd {Γ : Ctx} {X : Psh Ctx}
@@ -52,14 +52,13 @@ def uvPolyTpEquiv {Γ : Ctx} {X : Psh Ctx} :
 theorem uvPolyTpEquiv_symm {Γ : Ctx} {X : Psh Ctx}
     (A : y(Γ) ⟶ M.Ty) (B : y(M.ext A) ⟶ X) :
     M.uvPolyTpEquiv.symm ⟨ A, B ⟩ =
-    M.uvPolyTp.pairPoly A ((pullbackIsoExt _ _).hom ≫ B) :=
+    M.uvPolyTp.lift A ((pullbackIsoExt _ _).hom ≫ B) :=
   rfl
 
 @[simp] theorem uvPolyTpEquiv_symm_proj
     {Γ : Ctx} {X : Psh Ctx} (A : y(Γ) ⟶ M.Ty) (B : y(M.ext A) ⟶ X):
-    M.uvPolyTpEquiv.symm ⟨A, B⟩ ≫ M.uvPolyTp.proj _ = A := by
-  simp only [uvPolyTpEquiv_symm]
-  apply M.uvPolyTp.pair_proj
+    M.uvPolyTpEquiv.symm ⟨A, B⟩ ≫ M.uvPolyTp.fstProj _ = A := by
+  simp [uvPolyTpEquiv_symm]
 
 /-- `sec` is the universal lift in the following diagram,
   which is a section of `Groupoidal.forget`
@@ -88,8 +87,8 @@ def sec {Γ : Ctx} (α : y(Γ) ⟶ M.Tm) :
   (M.disp_pullback (α ≫ M.tp)).lift_snd _ _ _
 
 theorem lift_ev {Γ : Ctx} {AB : y(Γ) ⟶ M.uvPolyTp.functor.obj M.Ty}
-    {α : y(Γ) ⟶ M.Tm} (hA : AB ≫ M.uvPolyTp.proj M.Ty = α ≫ M.tp)
-    : pullback.lift AB α hA ≫ UvPoly.genPb.u₂ M.uvPolyTp M.Ty
+    {α : y(Γ) ⟶ M.Tm} (hA : AB ≫ M.uvPolyTp.fstProj M.Ty = α ≫ M.tp)
+    : pullback.lift AB α hA ≫ (UvPoly.PartialProduct.fan M.uvPolyTp M.Ty).snd
     = M.sec α ≫ eqToHom (by rw [← hA]; rfl) ≫ (M.uvPolyTpEquiv AB).2 :=
   sorry
 
diff --git a/GroupoidModel/Russell_PER_MS/UHom.lean b/GroupoidModel/Russell_PER_MS/UHom.lean
@@ -1,7 +1,6 @@
 import GroupoidModel.Russell_PER_MS.NaturalModelSigma
 import GroupoidModel.ForMathlib
 import Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
-import Poly.UvPoly
 
 /-! Morphisms of natural models, and Russell-universe embeddings. -/
 
diff --git a/GroupoidModel/attic/Display.lean b/GroupoidModel/attic/Display.lean
diff --git a/GroupoidModel/attic/Russell_PER_MS/NaturalModelPi.lean b/GroupoidModel/attic/Russell_PER_MS/NaturalModelPi.lean
diff --git a/GroupoidModel/attic/Tarski/NaturalModel.lean b/GroupoidModel/attic/Tarski/NaturalModel.lean
@@ -13,13 +13,8 @@ import Mathlib.CategoryTheory.Yoneda
 import Mathlib.CategoryTheory.Limits.Shapes.Terminal
 import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
 import Mathlib.CategoryTheory.Limits.Presheaf
-import Mathlib.CategoryTheory.Adjunction.Over
 
---import Poly
-import Poly.LCCC.Basic
-import Poly.LCCC.Presheaf
-import Poly.Exponentiable
-import Poly.UvPoly
+import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Presheaf
 
 import GroupoidModel.ForPoly
 
@@ -79,23 +74,17 @@ variable [M : NaturalModelBase Ctx]
 
 instance : HasFiniteWidePullbacks (Psh Ctx) := hasFiniteWidePullbacks_of_hasFiniteLimits _
 
-instance : LCC (Psh Ctx) := @LCCC.mkOfOverCC _ _ _ ⟨CategoryOfElements.presheafOverCCC⟩
-
-instance {Tm Ty : Psh Ctx} (tp : Tm ⟶ Ty) : CartesianExponentiable tp where
-  functor := LCC.pushforward tp
-  adj := LCC.adj _
-
 @[reducible]
 def uvPoly {Tm Ty : Psh Ctx} (tp : Tm ⟶ Ty) : UvPoly Tm Ty := ⟨tp, inferInstance⟩
-def uvPolyT {Tm Ty : Psh Ctx} (tp : Tm ⟶ Ty) : UvPoly.Total (Psh Ctx) := ⟨_, _, uvPoly tp⟩
+def uvPolyT {Tm Ty : Psh Ctx} (tp : Tm ⟶ Ty) : UvPoly.Total (Psh Ctx) := ⟨uvPoly tp⟩
 
 def P {Tm Ty : Psh Ctx} (tp : Tm ⟶ Ty) : Psh Ctx ⥤ Psh Ctx := (uvPoly tp).functor
 
 def P_naturality {E B E' B' : Psh Ctx}
     {f : E ⟶ B} {f' : E' ⟶ B'} (α : uvPolyT f ⟶ uvPolyT f') : P f ⟶ P f' :=
   UvPoly.naturality (P := uvPolyT f) (Q := uvPolyT f') α
 
-def proj {Tm Ty : Psh Ctx} (tp : Tm ⟶ Ty) : (P tp).obj Ty ⟶ Ty := (uvPoly tp).proj _
+def proj {Tm Ty : Psh Ctx} (tp : Tm ⟶ Ty) : (P tp).obj Ty ⟶ Ty := (uvPoly tp).fstProj _
 
 -- def PolyTwoCellBack {Tm Ty : Psh Ctx} (tp : Tm ⟶ Ty) := sorry
 
diff --git a/GroupoidModel/attic/Tarski/TarskiNaturalModel.lean b/GroupoidModel/attic/Tarski/TarskiNaturalModel.lean
@@ -2,10 +2,6 @@ import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
 import GroupoidModel.Tarski.NaturalModel
 import GroupoidModel.Grothendieck.IsPullback
 import GroupoidModel.Grothendieck.Groupoidal
-import Poly.LCCC.Basic
-import Poly.LCCC.Presheaf
-import Poly.Exponentiable
-import Poly.UvPoly
 
 /-!
 Here we construct the natural model for groupoids.
diff --git a/GroupoidModel/attic/Tarski/TypeTheory.lean b/GroupoidModel/attic/Tarski/TypeTheory.lean
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -11,21 +11,31 @@
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/sinhp/Poly.git",
+  {"url": "https://github.com/Vtec234/Poly.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7e224fb1f749fd8c9fccc756983c9b9bd7b68d39",
+   "rev": "b514a5adebd8046abbf93ad22109bace6c9faf2b",
    "name": "Poly",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "profunctor-naturality",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/Vtec234/lean4-seq",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "b6b76a5d7cc1c8b11c52f12a7bd90c460b7cba5a",
+   "name": "seq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3685941cee510d07c956201c23a77c6a89b7857b",
+   "rev": "fbe595fc740ee7a1789c6e6ebefa322e054a41c0",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -35,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "59a8514bb0ee5bae2689d8be717b5272c9b3dc1c",
+   "rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
+   "rev": "ba020ed434b9c5877eb62ff072a28f5ec56eb871",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5013810061a18ca1f5510106172b94c6fbd0a2fc",
+   "rev": "c96401869916619b86e2e54dbb8e8488bd6dd19c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,17 +75,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8fff3f074da9237cd4e179fd6dd89be6c4022d41",
+   "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v0.0.53",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ba9a63be53f16b3b6e4043641c6bad4883e650b4",
+   "rev": "ec060e0e10c685be8af65f288e23d026c9fde245",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b1311119f5f7c79c818d3e06621cc81f4bb8973f",
+   "rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -95,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "512d7fa38234139a34c04e3b3438fc142b51bbee",
+   "rev": "f2fb9809751c4646c68c329b14f7d229a93176fd",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc",
+   "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.lean b/lakefile.lean
@@ -10,7 +10,7 @@ package groupoid_model where
   ]
   -- add any additional package configuration options here
 
-require Poly from git "https://github.com/sinhp/Poly.git"
+require Poly from git "https://github.com/Vtec234/Poly.git" @ "profunctor-naturality"
 
 @[default_target]
 lean_lib GroupoidModel where
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.17.0-rc1
+leanprover/lean4:v4.18.0-rc1
