bump mathlib

Author: sinhp

Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean

@@ -304,11 +304,6 @@ def starPullbackIsoStar [HasBinaryProducts C] [HasPullbacks C] {X Y : C} (f : X
     star Y ⋙ pullback f ≅ star X :=
   conjugateIsoEquiv ((mapPullbackAdj f).comp (forgetAdjStar Y)) (forgetAdjStar X) (mapForget f)
 
--- from Over.Basic
-theorem iteratedSliceBackward_forget {X : C} (A : Over X) :
-    iteratedSliceBackward A ⋙ forget A = Over.map A.hom :=
-  rfl
-
 /-- The functor `Over.pullback f : Over Y ⥤ Over X` is naturally isomorphic to
 `Over.star : Over Y ⥤ Over (Over.mk f)` post-composed with the
 iterated slice equivlanece `Over (Over.mk f) ⥤ Over X`. -/

Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sina Hazratpour
 -/
 import Poly.ForMathlib.CategoryTheory.Comma.Over.Pullback
-import Mathlib.CategoryTheory.Closed.Cartesian
+import Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
 
 /-!
 # The section functor as a right adjoint to the star functor
@@ -13,6 +13,7 @@ We show that if `C` is cartesian closed then `star I : C ⥤ Over I`
 has a right adjoint `sectionsFunctor` whose object part is the object of sections
 of `X` over `I`.
 
+
 -/
 
 noncomputable section

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Sina Hazratpour. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sina Hazratpour, Emily Riehl
+Authors: Sina Hazratpour, Mario Carneiro
 -/
 import Mathlib.CategoryTheory.Adjunction.Lifting.Right
 import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Basic
@@ -54,7 +54,7 @@ def exponentiableMorphism : ExponentiableMorphism (g f u) := by infer_instance
 
 namespace ExponentiableMorphism
 
-instance mapPullbackAdj_regularMono {C} [Category C] [HasPullbacks C] {A B : C} (F : A ⟶ B)
+def mapPullbackAdj_regularMono {C} [Category C] [HasPullbacks C] {A B : C} (F : A ⟶ B)
     (X : Over A) : RegularMono ((mapPullbackAdj F).unit.app X) := by
   let FU := Over.map F ⋙ Over.pullback F
   set η := (mapPullbackAdj F).unit
@@ -73,6 +73,7 @@ theorem of_isPullback {C' : Type u} [Category.{v} C'] [HasPullbacks C'] [HasTerm
   have : IsLeftAdjoint _ :=
     ⟨_, ⟨(mapPullbackAdj f).comp (adj g) |>.ofNatIsoLeft (pullbackMapIsoSquare H.flip).symm⟩⟩
   isLeftAdjoint_triangle_lift (Over.pullback fst) (mapPullbackAdj snd)
+    (mapPullbackAdj_regularMono _)
 
 end ExponentiableMorphism
 

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Steve Awodey, Sina Hazratpour
 -/
 
-import Mathlib.CategoryTheory.Closed.Types
+import Mathlib.CategoryTheory.Monoidal.Closed.Types
 import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
 import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Basic
-import Mathlib.CategoryTheory.Closed.FunctorCategory.Basic
+import Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
 
 
 noncomputable section

Poly/ForMathlib/CategoryTheory/PartialProduct.lean

@@ -6,7 +6,7 @@ Authors: Sina Hazratpour
 import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
 import Mathlib.CategoryTheory.Comma.Over.Pullback
 import Poly.ForMathlib.CategoryTheory.Comma.Over.Pullback
-import Mathlib.CategoryTheory.Closed.Cartesian
+import Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
 import Mathlib.CategoryTheory.EqToHom
 
 /-! ## Partial Products

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "32bd6c7c8ca4a4be1c71bc04df0c9cf929d04818",
+   "rev": "3cfe59e73325809509831ef285891b6ebd02da62",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8864a73bf79aad549e34eff972c606343935106d",
+   "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
+   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "451499ea6e97cee4c8979b507a9af5581a849161",
+   "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d",
+   "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.77",
+   "inputRev": "v0.0.84",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1fa48c6a63b4c4cda28be61e1037192776e77ac0",
+   "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "95c2f8afe09d9e49d3cacca667261da04f7f93f7",
+   "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c44068fa1b40041e6df42bd67639b690eb2764ca",
+   "rev": "dff865b7ee7011518d59abfc101c368293173150",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "72ae7004d9f0ddb422aec5378204fdd7828c5672",
+   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.0-rc2",
+   "inputRev": "v4.27.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Poly",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.25.0-rc2
+leanprover/lean4:v4.27.0-rc1