Martin Escardo on Nostr: npub1zxcap…z6mh2 I do actually want to compute with univalence. Cubical type theory ...
npub1zxcapz0w49lnyu0u3gs5g63fevl9meuy6hykrhpu7muslwkdj9js6z6mh2 (npub1zxc…6mh2)
I do actually want to compute with univalence. Cubical type theory does that for me. I just don't want to *program* in cubical myself. I can use a univalence program supplied to me by the cubical library.
This is no different from what happens with the "print statement" in most languages: if it wasn't there as primitive, you wouldn't be able to implement it in the language itself. It is actually very complicated in practice, requiring interaction with the operating system, which does actually implement it.
Univalence as an axiom is no different from that.
You want to compute with it, but you don't necessarily want to see how it is implemented.
I do actually want to compute with univalence. Cubical type theory does that for me. I just don't want to *program* in cubical myself. I can use a univalence program supplied to me by the cubical library.
This is no different from what happens with the "print statement" in most languages: if it wasn't there as primitive, you wouldn't be able to implement it in the language itself. It is actually very complicated in practice, requiring interaction with the operating system, which does actually implement it.
Univalence as an axiom is no different from that.
You want to compute with it, but you don't necessarily want to see how it is implemented.