nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyp2aucj8nm0d5n2ls2z3dy2z5udpsplzpjq60kur0q9qfax33370cyndand (nprofile…dand) OK, well a moment's glance more: they acknowledge the use of AI (good! though not in writing, which I'm still suspicious of). However, they just straight up postulate univalence which is inconsistent in Lean. So uh. yeah, this is indeed going to be a very powerful framework for homotopy theory. Perhaps a smidge too powerful.
https://github.com/Arthur742Ramos/ComputationalPathsLean/blob/324ecc421fab12978e913e583135b7d8d9e470b3/ComputationalPaths/Path/Basic/Univalence.lean#L24
daniel gratzer
npub1p6…kevjm
2025-11-27 13:22:43 UTC
in reply to nevent1q…595t
Author Public Key
npub1p6adh0fwyx6303tm7amv3sjv2nzn9ak0umwtd7n39lvq0rqhdj7slkevjmSeen on
wss://relay.mostr.pubPublished at
2025-11-27 13:22:43 UTCEvent JSON
{
"id": "df405e3f69bd47735e8d8779cc628fe07cbfefc504cd3debaec4e2754299f1c0",
"pubkey": "0ebadbbd2e21b517c57bf776c8c24c54c532f6cfe6dcb6fa712fd8078c176cbd",
"created_at": 1764249763,
"kind": 1,
"tags": [
[
"p",
"55de62479ededa4d5f8285169142a71a1807e20c81a7db83780a04f4d18c7cfc",
"wss://relay.ditto.pub/"
],
[
"p",
"a859a34b101281dd2f0bcb9f1ac28e84a8151b97d5007d033a40728ec3f05e34",
"wss://relay.ditto.pub/"
],
[
"e",
"99e9006fe74f726b6fece2a5a55db21fb1417f34df60b33f8436c039ac075200",
"wss://relay.ditto.pub/",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/danielgratzer/statuses/115621872490665816",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyp2aucj8nm0d5n2ls2z3dy2z5udpsplzpjq60kur0q9qfax33370cyndand OK, well a moment's glance more: they acknowledge the use of AI (good! though not in writing, which I'm still suspicious of). However, they just straight up postulate univalence which is inconsistent in Lean. So uh. yeah, this is indeed going to be a very powerful framework for homotopy theory. Perhaps a smidge too powerful.\n\nhttps://github.com/Arthur742Ramos/ComputationalPathsLean/blob/324ecc421fab12978e913e583135b7d8d9e470b3/ComputationalPaths/Path/Basic/Univalence.lean#L24",
"sig": "981488c1b54279b70f664067a2b75b5ef6d76f90be646c067994bf4f483c954ca67f7f5093a3f274ca7104dea8068ea57948d4ac42b3093813d857af43320354"
}