Kan complexes

In this file we give the definition of Kan complexes. In Mathlib/AlgebraicTopology/Quasicategory.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.
• Generalize the definition to higher universes. Since Λ[n, i] is an object of SSet.{0}, the current definition of a Kan complex S requires S : SSet.{0}.

class SSet.KanComplex (S : SSet) : Prop

A simplicial set S is a Kan complex 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.

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

theorem SSet.KanComplex.hornFilling {S : SSet} [self : S.KanComplex] ⦃n : ℕ⦄ ⦃i : Fin (n + 1)⦄ (σ₀ : SSet.horn n i ⟶ S) : ∃ (σ : SSet.standardSimplex.obj (SimplexCategory.mk n) ⟶ S), σ₀ = CategoryTheory.CategoryStruct.comp (SSet.hornInclusion n i) σ