English
A canonical functor that sends a 2-truncated simplicial set to its homotopy category.
Русский
Канонический функтор, переводящий 2-отрезанный симпликсальный множество к его гомотопической категории.
LaTeX
$$$hoFunctor_2 : SSet.Truncated\\, 2 \\to Cat$$$
Lean4
/-- The functor that takes a 2-truncated simplicial set to its homotopy category. -/
def hoFunctor₂ : SSet.Truncated.{u} 2 ⥤ Cat.{u, u}
where
obj V := Cat.of (V.HomotopyCategory)
map {S T} F := mapHomotopyCategory F
map_id
S := by
apply Quotient.lift_unique'
simp [mapHomotopyCategory, Quotient.lift_spec]
exact Eq.trans (Functor.id_comp ..) (Functor.comp_id _).symm
map_comp {S T U} F
G := by
apply Quotient.lift_unique'
simp [mapHomotopyCategory, SSet.Truncated.HomotopyCategory.quotientFunctor]
rw [Quotient.lift_spec, Cat.comp_eq_comp, Cat.comp_eq_comp, ← Functor.assoc, Functor.assoc, Quotient.lift_spec,
Functor.assoc, Quotient.lift_spec]
