English
Given a simplicial set S and a filler operation that assigns, for every σ0 on a certain horn, a filling σ on Δ[n], the construction yields a quasicategory structure on S.
Русский
Пусть дано дополняющее отображение, которое каждому заполнителю рога σ0 ставит соответствующий заполнитель σ на Δ[n]; тогда S становится квази-категорией.
LaTeX
$$$\text{quasicategory}(S)$, если существует функционал заполнения для всех рогов: \forall n,i, \; σ_0, \exists σ : Δ[n] \to S, σ_0 = Λ[n,i].ι σ$$$
Lean4
theorem quasicategory_of_filler (S : SSet)
(filler :
∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : (Λ[n + 2, i] : SSet) ⟶ S) (_h0 : 0 < i) (_hn : i < Fin.last (n + 2)),
∃ σ : S _⦋n + 2⦌, ∀ (j) (h : j ≠ i), S.δ j σ = σ₀.app _ (horn.face i j h)) :
Quasicategory S where
hornFilling' n i σ₀ h₀
hₙ := by
obtain ⟨σ, h⟩ := filler σ₀ h₀ hₙ
refine ⟨yonedaEquiv.symm σ, ?_⟩
apply horn.hom_ext
intro j hj
rw [← h j hj, NatTrans.comp_app]
rfl
