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.SimplicialObject.δ CategoryTheory.types CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Subcomplex.toSSet CategoryTheory.Functor.obj SSet largeCategory stdSimplex horn Opposite.op horn.face	Quasicategory	—	horn.hom_ext CategoryTheory.NatTrans.comp_app

SSet.Quasicategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hornFilling 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory SSet.Subcomplex.toSSet CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.horn SSet.Subcomplex.ι	—	zero_add hornFilling'
hornFilling' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory SSet.Subcomplex.toSSet CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.horn SSet.Subcomplex.ι	—	—

---

← Back to Index