Simplicial sets #
A simplicial set is just a simplicial object in Type,
i.e. a Type-valued presheaf on the simplex category.
(One might be tempted to call these "simplicial types" when working in type-theoretic foundations, but this would be unnecessarily confusing given the existing notion of a simplicial type in homotopy type theory.)
The category of simplicial sets.
This is the category of contravariant functors from
SimplexCategory to Type u.
Equations
Instances For
Equations
The constant map of simplicial sets X ⟶ Y induced by a simplex y : Y _[0].
Equations
- SSet.const y = { app := fun (n : SimplexCategoryᵒᵖ) (x : X.obj n) => Y.map ((Opposite.unop n).const (SimplexCategory.mk 0) 0).op y, naturality := ⋯ }
Instances For
The ulift functor SSet.{u} ⥤ SSet.{max u v} on simplicial sets.
Equations
- SSet.uliftFunctor = (CategoryTheory.SimplicialObject.whiskering (Type ?u.7) (Type (max ?u.7 ?u.8))).obj CategoryTheory.uliftFunctor.{?u.8, ?u.7}
Instances For
Truncated simplicial sets.
Equations
Instances For
Equations
The ulift functor SSet.Truncated.{u} ⥤ SSet.Truncated.{max u v} on truncated
simplicial sets.
Equations
- SSet.Truncated.uliftFunctor k = (CategoryTheory.whiskeringRight (SimplexCategory.Truncated k)ᵒᵖ (Type ?u.17) (Type (max ?u.17 ?u.18))).obj CategoryTheory.uliftFunctor.{?u.18, ?u.17}
Instances For
The truncation functor on simplicial sets.
Equations
Instances For
The adjunction between the n-skeleton and n-truncation.
Equations
Instances For
The adjunction between n-truncation and the n-coskeleton.
Equations
Instances For
Since Truncated.inclusion is fully faithful, so is right Kan extension along it.
Equations
Instances For
Since Truncated.inclusion is fully faithful, so is left Kan extension along it.
Equations
Instances For
The category of augmented simplicial sets, as a particular case of augmented simplicial objects.