feat: port CategoryTheory.Sites.Sieves (#2691)

leanprover-community · Mar 7, 2023 · 26763c5 · 26763c5
1 parent dcdfad2
commit 26763c5
Show file tree

Hide file tree

Showing 2 changed files with 818 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -330,6 +330,7 @@ import Mathlib.CategoryTheory.Products.Basic
 import Mathlib.CategoryTheory.Products.Bifunctor
 import Mathlib.CategoryTheory.Quotient
 import Mathlib.CategoryTheory.Sigma.Basic
+import Mathlib.CategoryTheory.Sites.Sieves
 import Mathlib.CategoryTheory.Skeletal
 import Mathlib.CategoryTheory.StructuredArrow
 import Mathlib.CategoryTheory.Sums.Associator