npub1jd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208rayscvt4jc (npub1jd8…t4jc) May I say, without trying to offend anybody, the cubical type theory feels like assembly language for homotopy theory?
As I discussed earlier here, I am glad it exists because I can use it to compute if I want to. But I prefer to write high-level code in the style of HoTT/UF, in Agda, knowing that the assumptions I make (univalence, HIT's) are implemented in cubical Agda and so I can supply them as inputs to my high-level proofs.
Also, at the moment, cubical type theory is not "portable": it applies to particular models rather than all models.
Martin Escardo /
npub1t3…fg3z4
2023-09-02 16:19:56
in reply to nevent1q…79fy
Author Public Key
npub1t3n4le6kr3f09s823keer5kr53j4d0kf50q2fd83pu35lcpltr9q0fg3z4Published at
2023-09-02 16:19:56Event JSON
{
"id": "620823a76a172a6d45f93736793f0006fee6992a94a9ad0176484bb270ab6edc",
"pubkey": "5c675fe7561c52f2c0ea8db391d2c3a46556bec9a3c0a4b4f10f234fe03f58ca",
"created_at": 1693671596,
"kind": 1,
"tags": [
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.mostr.pub"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.mostr.pub"
],
[
"e",
"aac82fa4a1f5cb7064c7dc9e7a0fddea4b2c31dd67148b17e6af0584a6c16c56",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/MartinEscardo/statuses/110996461759705407",
"activitypub"
]
],
"content": "nostr:npub1jd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208rayscvt4jc May I say, without trying to offend anybody, the cubical type theory feels like assembly language for homotopy theory?\n\nAs I discussed earlier here, I am glad it exists because I can use it to compute if I want to. But I prefer to write high-level code in the style of HoTT/UF, in Agda, knowing that the assumptions I make (univalence, HIT's) are implemented in cubical Agda and so I can supply them as inputs to my high-level proofs.\n\nAlso, at the moment, cubical type theory is not \"portable\": it applies to particular models rather than all models.",
"sig": "c756369234fda3e66ea2d43bdcfd6b8a80a75cc7d197e90d68be40c62ae33d32a60cc880eb7d30df626761eb5b6dfda9825eb7d58c0e73c8dcd40a7515cfec54"
}