agda
Field names for RegularEpi/RegularMono are nondescriptive
Currently, RegularEpi and RegularMono are defined like so:
record RegularMono (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
field
{ C } : Obj
g : B ⇒ C
h : B ⇒ C
equalizer : IsEqualizer f h g
record RegularEpi (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
field
{ C } : Obj
h : C ⇒ A
g : C ⇒ A
coequalizer : IsCoequalizer h g f
Using h and g for the field names here is kind of annoying, as it means that you can't open them without renaming, and
variable blocks in Category.Morphism.Regular can't use those names.
We should probably pick some better names for these fields, I can't think of anything great beyond mor₁ and mor₂. Perhaps others have some insight.
I don't have any good suggestions for g and h, but shouldn't the records themselves be called IsRegularEpi and IsRegularMono? They're not bundles, are they?
OK, I'm gonna give it a go anyway: we could call them witness₁ and witness₂. Or predecessor{₁,₂} for regular epis and successor{₁,₂} for monos?
It's a bit weird for sure, but consistent with Epi/Mono et. al. In #340 I adopted the convention that IsExtremalEpi denotes a property of an epi, not a morphism, and ExtremalEpi f denotes a bundled record of e : Epi f + IsExtremalEpi e. Regular morphisms are even wonkier due to the fact that they don't have an epi/mono field, so I think what we have now makes sense.
At the very least we could go with g₁, g₂ to mirror the names in Epi/Mono. It also avoids the shadowing issues.
I agree that g₁, g₂ would already be better. In some ways, the original mor suggestions might have been better?
I'm glad for the suggestions, but I'm not feeling witness or predecessor/successor (although I can definitely see the reasoning!)
The various reference textbooks that I've checked seem to all go out of their way to not name these! Basically the textbooks all go for a kind of raw Sigma type, but usually drawn as a diagram.
Lean's mathlib has a formalization too; they call them 'left' and 'right', which I think is considerably worse.
