Basic

📁 Source: Mathlib/AlgebraicTopology/Quasicategory/Basic.lean

Statistics

Metric	Count
Definitions Quasicategory	1
Theorems hornFilling, hornFilling', instQuasicategoryOfKanComplex, quasicategory_of_filler	4
Total	5

SSet

Definitions

Name	Category	Theorems
Quasicategory 📖	CompData	5 math math: StrictSegal.quasicategory, quasicategory_of_filler, CategoryTheory.Nerve.quasicategory, instQuasicategoryOfKanComplex, StrictSegal.quasicategory'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instQuasicategoryOfKanComplex 📖	mathematical	—	Quasicategory	—	KanComplex.hornFilling
quasicategory_of_filler 📖	mathematical	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op CategoryTheory.SimplicialObject.δ CategoryTheory.NatTrans.app Subcomplex.toSSet SSet CategoryTheory.Functor.category stdSimplex horn horn.face	Quasicategory	—	horn.hom_ext CategoryTheory.NatTrans.comp_app

SSet.Quasicategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hornFilling 📖	mathematical	—	Quiver.Hom SSet CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet.stdSimplex CategoryTheory.CategoryStruct.comp SSet.Subcomplex.toSSet SSet.horn SSet.Subcomplex.ι	—	zero_add hornFilling'
hornFilling' 📖	mathematical	—	Quiver.Hom SSet CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet.stdSimplex CategoryTheory.CategoryStruct.comp SSet.Subcomplex.toSSet SSet.horn SSet.Subcomplex.ι	—	—

---

← Back to Index