Structures · Topology
SSet.Finite
A simplicial set is finite if it has finitely many nondegenerate simplices.
- Shape
- One type argument · adds finite
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances8
- CategoryTheory.Functor.obj
- CategoryTheory.Limits.pullback
- CategoryTheory.Limits.coprod
- CategoryTheory.Limits.sigmaObj
- CategoryTheory.MonoidalCategoryStruct.tensorObj
- SSet.Subcomplex.toSSet
- CategoryTheory.MonoidalCategoryStruct.tensorUnit
- CategoryTheory.Limits.initial
How is a type an instance?
Loading the hierarchy index…
Assumed by16
- SSet.finite_of_mono
- SSet.hasDimensionLT_of_finite
- SSet.finite_of_iso
- SSet.Finite.instIsFinitelyPresentable
- SSet.instFinitePullback
- SSet.instFiniteElemObjOppositeSimplexCategoryOpMkNonDegenerateOfFinite
- SSet.instFiniteToSSet
- SSet.instFiniteTensorObj
- SSet.Finite.exists_epi_from_isCardinalPresentable
- SSet.finite_of_isPullback
- SSet.finite_range
- SSet.instFiniteObjOppositeSimplexCategoryOfFinite
- SSet.instFiniteSigmaObjOfFinite
- SSet.instFiniteCoprod
- SSet.Finite.finite
- SSet.finite_of_epi
Ancestors0
No ancestors.