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