∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Nerve.nerveFunctor₂.comp SSet.oneTruncation₂).map F)
      (SSet.OneTruncation₂.ofNerve₂ ↑Y).hom =
    CategoryTheory.CategoryStruct.comp (SSet.OneTruncation₂.ofNerve₂ ↑X).hom (CategoryTheory.ReflQuiv.forget.map F)