∀ {X : SSet.Truncated 2}
  {x y : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f : SSet.Truncated.Edge x y}, SSet.Truncated.HomotopicR f f