{V : SSet.Truncated 2} →
  {D : Type u_1} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      (obj : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.OneTruncation₂._proof_1 }) → D) →
        (map :
            {x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.OneTruncation₂._proof_1 })} →
              SSet.Truncated.Edge x y → (obj x ⟶ obj y)) →
          (∀ (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.OneTruncation₂._proof_1 })),
              map (SSet.Truncated.Edge.id x) = CategoryTheory.CategoryStruct.id (obj x)) →
            (∀
                {x₀ x₁ x₂ :
                  V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.OneTruncation₂._proof_1 })}
                {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
                (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂) →
              CategoryTheory.Functor V.HomotopyCategory D