Commit 2020-06-26 23:51 78d67807

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.