mathlib

14e80e85 - feat(category_theory/filtered): generalize to allow empty categories (#18013)

feat(category_theory/filtered): generalize to allow empty categories (#18013) Also: + Create aliases so that we can write `is_filtered.cocone_objs` without the `_or_empty`. + Fix misnomers `is_cofiltered.cocone_objs/maps`; `cocone` should be replaced by `cone`. + Add special shapes `span`/`cospan` and lemma `ranges_directed` from #17905. + Golf `bowtie` and `tulip` using `span`. Co-authored-by: Rémi Bottinelli <remi.bottinelli@bluewin.ch>