instCategoryHomotopyCategory — Mathlib

English

The homotopy category of a 2-truncated simplicial set V is the quotient of the corresponding free refl category by the homotopy relation HoRel₂.

Русский

Гомотопическая категория 2-отрезанного симпликсального множества V есть фактор-пространство свободной refl-категории над V по отношению гомотопии HoRel₂.

LaTeX

$$$\\mathrm{HomotopyCategory}(V) = \\operatorname{Quot}(\\mathrm{HoRel}_2(V))$$$

Lean4

instance (V : SSet.Truncated.{u} 2) : Category.{u} (V.HomotopyCategory) :=
  inferInstanceAs (Category (CategoryTheory.Quotient ..))

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