Jon Sterling on Nostr: npub1ez3yy…exnxl I think you're right, this is what I have been starting to think ...
npub1ez3yya8tpgge7lk4jq2zxz0cj3d2mcgev9mffd4ec7tfy84hre4suexnxl (npub1ez3…xnxl) I think you're right, this is what I have been starting to think as well... And the non-portability is a big problem for me.
Here's the thing that made me think that cubical type theory was more than assembly language in the past, but about which I am not so sure anymore. In type theory, everything needs to be dependent eventually; paths / identifications are no different. Unfortunately, dependent paths are really awkward to work with in HoTT — in ways that cubical type theory handles more naturally IMO.
But the thing I noticed is that the place dependent paths usually arise is in sigma types, but one of the lessons of serious HoTT developments (both cubical and non-cubical) is that every time you have a sigma type you'll use more than once, you need to really characterize its identity type right away in terms of something more natural (using SIP, etc.). And doing this thing, which you always have to do anyway, tends to get rid of a lot of the very painful dependent path algebra anyway.
Here's the thing that made me think that cubical type theory was more than assembly language in the past, but about which I am not so sure anymore. In type theory, everything needs to be dependent eventually; paths / identifications are no different. Unfortunately, dependent paths are really awkward to work with in HoTT — in ways that cubical type theory handles more naturally IMO.
But the thing I noticed is that the place dependent paths usually arise is in sigma types, but one of the lessons of serious HoTT developments (both cubical and non-cubical) is that every time you have a sigma type you'll use more than once, you need to really characterize its identity type right away in terms of something more natural (using SIP, etc.). And doing this thing, which you always have to do anyway, tends to get rid of a lot of the very painful dependent path algebra anyway.