Julio: How to sort rational trees in Prolog? (Was: How to formalize dependent setoid morphisms?)

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