Field names for RegularEpi/RegularMono are nondescriptive

[TOTBWF]

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.

[sstucki]

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?

[sstucki]

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?

[TOTBWF]

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.

[TOTBWF]

At the very least we could go with g₁, g₂ to mirror the names in Epi/Mono. It also avoids the shadowing issues.

[JacquesCarette]

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.

[t-wissmann]

On pen & paper, I usually call them as follows:

record RegularEpi (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
  field
    { R } : Obj
    pr₁ : R ⇒ A
    pr₂ : R ⇒ A
    coequalizer : IsCoequalizer pr₁ pr₂ f

This underpins the intuition that R is an internal relation on A (with projections pr₁, pr₂) for which A quotiented by (the equivalence closure of) R yields B and f sends elements to their equivalence class.

Unfortunately, this really only applies to RegularEpi. Viewing RegularMono via internal relations doesn't help too much, because RegularMono existentially quantifies over the set C: "there exists a set C for which B can be viewed as a relation on it such that A is the intersection of this relation and the diagonal on C"