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