Kan complexes

In this file we give the definition of Kan complexes. In Mathlib/AlgebraicTopology/Quasicategory/Basic.lean we show that every Kan complex is a quasicategory.

TODO

• Show that the singular simplicial set of a topological space is a Kan complex.

class SSet.KanComplex (S : SSet) : Prop

A simplicial set S is a Kan complex if it satisfies the following horn-filling condition: for every nonzero n : ℕ and 0 ≤ i ≤ n, every map of simplicial sets σ₀ : Λ[n, i] → S can be extended to a map σ : Δ[n] → S.

• hornFilling ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (σ₀ : horn (n + 1) i ⟶ S) : ∃ (σ : stdSimplex.obj (SimplexCategory.mk (n + 1)) ⟶ S), σ₀ = CategoryTheory.CategoryStruct.comp (hornInclusion (n + 1) i) σ