English
Natural transformation unit respects morphisms between truncated nerves; i.e., applying f and then the unit equals applying the unit and then nerve map.
Русский
Естественность единицы сохраняется при переходе между нерфами: сначала применяем f, затем единицу, затем карту нерва, либо наоборот.
LaTeX
$$$\\text{naturality}: f \\circ \\mathrm{unit.app}Y = \\mathrm{unit.app}X \\circ \\mathrm{nerveFunctor}_2(\\mathrm{map} f)$$$
Lean4
@[reassoc]
theorem naturality {X Y : SSet.Truncated.{u} 2} (f : X ⟶ Y) :
f ≫ unit.app Y = unit.app X ≫ nerveFunctor₂.map (hoFunctor₂.map f) :=
toNerve₂.ext _ _
(by
have := (OneTruncation₂.ofNerve₂.natIso).inv.naturality (hoFunctor₂.map f)
dsimp at this ⊢
rw [Functor.map_comp, Functor.map_comp, nerve₂Adj.unit.map_app_eq, nerve₂Adj.unit.map_app_eq, ←
ReflQuiv.comp_eq_comp (Y := ReflQuiv.of _), ← ReflQuiv.comp_eq_comp (Y := ReflQuiv.of _), assoc, ← this]
rfl)
