instQuasicategoryOfKanComplex — Mathlib

English

Every Kan complex is a quasicategory: if S is a Kan complex, then S is a quasicategory.

Русский

Каждый Кан-комплекс является квази-категорией: если S — Кан-комплекс, то S — квази-категория.

LaTeX

$$$\forall S, \big(S\text{.KanComplex} \Rightarrow S\text{.Quasicategory}\big)$$$

Lean4

/-- Every Kan complex is a quasicategory. -/
@[kerodon 003C]
instance (S : SSet) [KanComplex S] : Quasicategory S where hornFilling' _ _ σ₀ _ _ := KanComplex.hornFilling σ₀

Похожие утверждения