epi_comp not an instance

Stream: maths

[Kevin Buzzard]

import algebra.homology.homology
import category_theory.abelian.homology

#print category_theory.mono_comp -- @[instance]
#print category_theory.epi_comp -- not an instance

When docs#category_theory.mono_comp and docs#category_theory.epi_comp are defined, neither of them are instances. But regex searches for instance.*epi_comp and instance.*mono_comp show that epi_comp is made a local instance in a couple of mathlib files, whereas mono_comp is made a global instance in category_theory/subobject with no explanation of why this was not done when it was defined. Is there a reason we're asymmetric here? Perhaps because nobody made the lattice of quotient objects?

[Yaël Dillies]

Hasn't @Bhavik Mehta done it in the topos project?

[Bhavik Mehta]

Nope, quotient objects aren't useful for toposes, at least not nearly as useful as for abelian categories

[Yaël Dillies]

AH okay, got myself confused then.

[Adam Topaz]

The fact that we don't have the lattice of quotient objects is yet another reason why using subobjects is terrible -- you can't dualize anything, and if you have to deal with op at any time you're out of luck.

(Maybe I'm just bitter)