What is Nostr?
Martin Escardo /
npub1t3n…g3z4
2023-09-02 16:48:14
in reply to nevent1q…0uw0

Martin Escardo on Nostr: npub1jd874…vt4jc I am actually very happy with HoTT/UF that is not obliged to ...

npub1jd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208rayscvt4jc (npub1jd8…t4jc) I am actually very happy with HoTT/UF that is not obliged to compute "directly". I like high-level thinking, both when I think about computation and when I think about mathematics.

As I said, if I want to compute, I can "plug" cubical type theory inputs to my programs.

I think it is misguided to insist that a foundation of constructive mathematics has to "compute directly". I like abstractions. They make my life less painful.
Author Public Key
npub1t3n4le6kr3f09s823keer5kr53j4d0kf50q2fd83pu35lcpltr9q0fg3z4