From: janburse@fastmail.fm   
      
   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?"   
    >    
    >   
    > To be continued...   
    >   
    > -Julio   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)