chore(deprecated): delete deprecated folder

[ChrisHughes24]

---

Nothing depends on it any more, so I guess we can delete it.

[YaelDillies]

I think it makes sense because even if we end up swapping back to unbundled morphisms in Lean 4, we won't reuse this material.

Note you will also need to delete test.import_order_timeout.

[kbuzzard]

My understanding is that the idea was that "these are sometimes useful as structures" so we're not going to delete them, although the fact that we never use them is an indication that perhaps they're not as useful as we think.

[jcommelin]

#13506