Joey Eremondi on Nostr: npub1ez3yy…exnxl Right but making a foundation of mathematics is not the only thing ...
npub1ez3yya8tpgge7lk4jq2zxz0cj3d2mcgev9mffd4ec7tfy84hre4suexnxl (npub1ez3…xnxl)
Right but making a foundation of mathematics is not the only thing people are using dependent types for.
I wonder if the solution is just to allow univalence to be used at quantity 0, so even if it interferes with reduction, it never interferes with program behavior.
npub1jd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208rayscvt4jc (npub1jd8…t4jc)
Right but making a foundation of mathematics is not the only thing people are using dependent types for.
I wonder if the solution is just to allow univalence to be used at quantity 0, so even if it interferes with reduction, it never interferes with program behavior.
npub1jd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208rayscvt4jc (npub1jd8…t4jc)