concrete_category): Delete empty file (#18653)

Commit

2 years ago

chore(category_theory/limits/shapes/concrete_category): Delete empty file (#18653) This file was made empty in #9864 but not deleted.

Author

YaelDillies

Parents