map_app_eq — Mathlib

English

A computation shows that applying one-truncation to the Mk' construction yields back the original F, up to canonical identifications.

Русский

Вычисление показывает, что применение oneTruncation2 к Mk' возвращает исходный F с каноническими идентификациями.

LaTeX

$$$\text{oneTruncation}_2\text{ map} (\mathrm{toNerve}_2.mk' F\;\text{hyp}) = F$$$

Lean4

theorem map_app_eq (X : SSet.Truncated.{u} 2) :
    SSet.oneTruncation₂.map (nerve₂Adj.unit.app X) =
      ReflQuiv.adj.{u}.unit.app (SSet.oneTruncation₂.obj X) ⋙rq
          (SSet.Truncated.HomotopyCategory.quotientFunctor X).toReflPrefunctor ⋙rq
        (OneTruncation₂.ofNerve₂.natIso).inv.app (hoFunctor₂.obj X) :=
  by apply oneTruncation₂_toNerve₂Mk'

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