A Question on Apartness definitions -- particularly irrefl

[bsaul]

I have an observation/question about the apartness/inequality definitions (sorry if this is not a particularly well formed yet). As I read about apartness in constructive math texts, it's generally defined on top of a notion of inequality (though perhaps inequivalence is a better term). For example, in A Course in Constructive Algebra by Mines, Richman, and Ruitenberg on p.8 (1988 ed): "We regard the relation of inequality as conventional and not necessarily the denial of equality. ... A consistent [which is what they call irreflexive], symmetric, cotranstive inequality is called an apartness." On the surface, this all well and good and the definition of apartness seems to match what's in the stdlib (at least of v2.2 without looking back in history).

But after reading Apartness and Uniformity by Bridges and Vîţă, I began to wonder if the stdlib has the relation between inequivalence and equivalence correct. Here's how Bridges and Vîţă (p. 8) define inequality:

Note the condition that $\neq$ (which translates to _#_ in stdlib notation) implies the negation of equality (i.e. the "denial inequality" in the sense of Hines et al). Currently we have have an an ApartnessRelation is Irreflexive _≈_ _#_, which translates to ∀ {x y} → x ≈ y → ¬ (x # y), but this is the opposite of the Bridges definition, as I understand. Is the stdlib definition incorrect? or what am I missing here?

This is tangentially related to #2588 and Heyting algebra stuff more generally as that's were apartness starts to show up in the Algebra modules.

[Taneb]

I don't have access to that particular book, but this is the difference between an apartness relation and a tight apartness relation; see, for example, Wikipedia) and this library's definition of Tight.

[jamesmckinna]

Yes... #2588 defines (Is)TightApartnessRelation (and redefines Tight, hopefully for the final time), which should give you what Mines et al. are after. It's indeed moderately vexing that the old-timey literature on constructive mathematics (which I learnt from!) has so many 'non-standard' definitions, or at least ones where there never seemed to be a consistent nomenclature across authors.

So ... stdlib takes a 'naming by fiat' approach, but counter-arguments are also welcome!

[bsaul]

I don't have access to that particular book, but this is the difference between an apartness relation and a tight apartness relation; see, for example, Wikipedia) and this library's definition of Tight.

Sorry, I'm not completely following, what is "this"? (happy to email you a copy of the book, if you'd like FWIW).

Here's additional context from the Bridges book wherein they define tight:

I do agree that this definition of tight matches with the updated definition of Tight found in #2588. But the first condition of the inequality relation is different from Irreflexive _≈_ _#_, no? I take the first condition of Bridge's inequality relation to be Irreflexive _#_ _≈_.

Also, to be clear, the definition of Apartness that Bridges gives is different: they define apartness as a point-set relation (A -> Pred A -> Set), but at this point I trying to get clear on my understanding of inequality/inequivalence.

[jamesmckinna]

Re: inequality according to Bridges having 'opposite' first condition: both 'opposites' are definitionally equal to ∀ {x y} → x ≈ y → x # y → ⊥ (ie. Irreflexive is actually symmetric in its relational arguments!)

[bsaul]

Oh, duh, this is just flip.

Thanks y'all.