English
There is a natural isomorphism between nerve functor and nerve functor₂ composed with Truncated.cosk 2, with components built via standard universal maps.
Русский
Существует естественная изоморфия между nerve-функтором и nerve₂, композиция с Truncated.cosk 2, собираемая стандартными универсальными отображениями.
LaTeX
$$$ \text{cosk}_2\text{Iso} : \mathrm{nerve\,Functor} \cong \mathrm{nerve\,Functor}_2 \circ \mathrm{Truncated.cosk}(2) $$$
Lean4
/-- The natural isomorphism between `nerveFunctor` and `nerveFunctor₂ ⋙ Truncated.cosk 2` whose
components `nerve C ≅ (Truncated.cosk 2).obj (nerveFunctor₂.obj C)` shows that nerves of categories
are 2-coskeletal. -/
noncomputable def cosk₂Iso : nerveFunctor.{v, u} ≅ nerveFunctor₂.{v, u} ⋙ Truncated.cosk 2 :=
NatIso.ofComponents (fun C ↦ (nerve C).isoCoskOfIsCoskeletal 2) (fun _ ↦ (coskAdj 2).unit.naturality _)
