1. Forum
  2. Usenet
  3. SCI.LOGIC

  • How to formalize dependent setoid morphisms?

    From Julio Di Egidio@21:1/5 to All on Thu Jul 17 15:14:54 2025
    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)
  • From Mild Shock@21:1/5 to Julio Di Egidio on Sun Jul 20 23:21:24 2025
    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)