Structures · Topology
SSet.Quasicategory
A simplicial set S is a quasicategory if it satisfies the following horn-filling condition:
for every n : ℕ and 0 < i < n,
every map of simplicial sets σ₀ : Λ[n, i] → S can be extended to a map σ : Δ[n] → S.
- Shape
- One type argument · adds hornFilling'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances2
- CategoryTheory.Functor.obj
- CategoryTheory.nerve
How is a type an instance?
Loading the hierarchy index…
Assumed by9
- SSet.Quasicategory.hasLiftingProperty
- SSet.Quasicategory.hornFilling'
- SSet.Quasicategory.hornFilling
- SSet.quasicategory_of_innerFibration
- SSet.Quasicategory.from_innerFibrations
- SSet.instInnerFibrationFromOfQuasicategory
- SSet.instInnerFibrationAppPreOfMonoOfQuasicategory
- SSet.instQuasicategoryObjIhom
- SSet.quasicategory_of_innerFibration_quasicategory
Ancestors0
No ancestors.