Hi,

Some people like Juglio post references to
wonderful meandering along terminology like:

If X has decidable equality and negation
of equality is an apartness relation, then
the negation of equality is a (in fact the
unique) decidable tight apartness relation
on X, and any function from X to any set
Y with a tight apartness relation on Y
must be strongly extensional.

https://ncatlab.org/nlab/show/strongly+extensional+function#examples

Still they are clueless how to sort rational
trees in Prolog. I am pretty sure such people
don't know how to do it practically in a Prolog system.

Bye

Julio Di Egidio schrieb:

In fact, how to constructive mathematics a la Bishop.

I haven't got to the bottom of it, it turns out to be
a long term project in itself, for both theoretical and
technical reasons, but here are few notes and mainly the
references that I have managed to collect.

"How to formalize dependent setoid morphisms?" <https://discourse.rocq-prover.org/t/2759>

To be continued...

-Julio

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)