{X Y : SSet.Truncated 2} →
  (f₀ :
      X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) →
        Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ })) →
    (f₁ :
        X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) →
          Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })) →
      (∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })),
          f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) =
            Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) →
        (∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })),
            f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) =
              Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) →
          Y.StrictSegal → CategoryTheory.MorphismProperty (SimplexCategory.Truncated 2)