On a Particular Condition for Regular Coequality Relations

The setting of this research is Bishop’s constructive mathematics, the mathematics developed on intuitionistic logic. If (X,=,≠,θ) is an anti-ordered set, for a coequality q on X we say that it is strongly regular if it is regular and θ∘q^C ⊆q^C ∘θ holds. In this case, θ∘q^C is a quasi-antiorder relation on X such that the relation Θ=π∘θ∘π^-1 on X/q is the maximal antiorder on X/q.