Commit 2024-02-24 00:18 9a891c30

chore(CategoryTheory): remove an unnecessary instance and golf a proof in the effective epi file (#10734) We remove an instance saying that Sigma.desc is an Epi, because we have the stronger instance that it's an EffectiveEpi. We also give the corresponding result using general colimit API, and prove the old one using that.