diff --git a/blueprint/lean_decls b/blueprint/lean_decls
index ef9d9c6..288779e 100644
--- a/blueprint/lean_decls
+++ b/blueprint/lean_decls
@@ -1,6 +1,12 @@
 SimplexCategory.smallCategory
+SimplexCategory.δ
+SimplexCategory.σ
 SSet
 SSet.largeCategory
+SSet.standardSimplex
+SSet.boundary
+SSet.horn
+SSet.yonedaEquiv
 SSet.hasLimits
 SSet.hasColimits
 SSet.Quasicategory
@@ -8,9 +14,12 @@ 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