mathlib

78d67807 - chore(category_theory/pempty): use discrete pempty instead of a special pempty category (#3191)

chore(category_theory/pempty): use discrete pempty instead of a special pempty category (#3191) Use `discrete pempty` instead of a specialised `pempty` category. Motivation: Since we have a good API for `discrete` categories, there doesn't seem to be much point in defining a specialised `pempty` category with an equivalence, instead we might as well just use `discrete pempty`.