Update lean_decls

mckoen · Sep 4, 2024 · e714ae4 · e714ae4
1 parent cf62434
commit e714ae4
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/blueprint/lean_decls b/blueprint/lean_decls
@@ -1,16 +1,25 @@
 SimplexCategory.smallCategory
+SimplexCategory.δ
+SimplexCategory.σ
 SSet
 SSet.largeCategory
+SSet.standardSimplex
+SSet.boundary
+SSet.horn
+SSet.yonedaEquiv
 SSet.hasLimits
 SSet.hasColimits
 SSet.Quasicategory
 SSet.KanComplex
 CategoryTheory.nerve
 CategoryTheory.nerveFunctor
 CategoryTheory.Nerve.cosk2Iso
+SSet.oneTruncation
+CategoryTheory.ReflQuiv.adj
 CategoryTheory.SSet.hoCat
 CategoryTheory.nerveCounit_isIso
 CategoryTheory.nerveAdjunction
+nerveFunctor.fullyfaithful
 CategoryTheory.SimplicialCategory
 CategoryTheory.SimplicialCategory.HasCotensors
 CategoryTheory.SimplicialCategory.cotensor_bifunctoriality