chore: bump mathlib

emilyriehl · Jan 31, 2025 · 16ed3d4 · 16ed3d4
1 parent f749b5c
commit 16ed3d4
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 4 deletions.
diff --git a/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean b/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean
@@ -5,8 +5,8 @@ Authors: Johns Hopkins Category Theory Seminar
 -/
 
 import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialCategory.Basic
-import Mathlib.CategoryTheory.CodiscreteCategory
 import Mathlib.AlgebraicTopology.SimplicialSet.Nerve
+import Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
 
 universe u v u' v'
 

diff --git a/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean b/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean
@@ -1,5 +1,5 @@
-import Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
 import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplexCategory
+import Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
 
 universe u
 

diff --git a/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/MorphismProperty.lean b/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/MorphismProperty.lean
@@ -7,6 +7,7 @@ import InfinityCosmos.ForMathlib.CategoryTheory.MorphismProperty
 import InfinityCosmos.ForMathlib.AlgebraicTopology.Quasicategory.Basic
 import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.CoherentIso
 import Mathlib.AlgebraicTopology.SimplicialSet.Basic
+import Mathlib.AlgebraicTopology.SimplicialSet.Boundary
 
 namespace SSet
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "725eddcb98acf9b505220b6945a3b4a673a8a564",
+   "rev": "01a1707b7dff363729b99ba566d378bc77c0df9d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5b23a1297aba9683f231c4b1a7ab4076af4ad53d",
+   "rev": "9089cee37a32d51bc4aeea6506719a21b7a2d011",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",