There's a paper just dropped on arXiv that claims to be able to do some synthetic homotopy theory like in HoTT but with UIP, specifically in Lean…
https://arxiv.org/pdf/2511.19142
using something called “computation paths”:
https://arxiv.org/pdf/1107.1901v3
Has anyone tried to read these and do they actually contain any interesting idea? A very cursory look makes me raise eyebrows; I suspect either it doesn't actually work (I don't see that they are giving a model anywhere) or it can be described in 1 line like “2-level type theory modified in $WAY” but they don't say it.
Jean Abou Samra (new account)
npub14p…htzwd
2025-11-27 12:29:47 UTC
Author Public Key
npub14pv6xjcsz2qa6tctew034s5wsj5p2xuh65q86qe6gpegaslstc6qjhtzwdPublished at
2025-11-27 12:29:47 UTCEvent JSON
{
"id": "f12a675488e22a9caa5b58924b971853748a5aff40375b272d83f742e9e99cf9",
"pubkey": "a859a34b101281dd2f0bcb9f1ac28e84a8151b97d5007d033a40728ec3f05e34",
"created_at": 1764246587,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/users/jeanas/statuses/115621664384780129",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "There's a paper just dropped on arXiv that claims to be able to do some synthetic homotopy theory like in HoTT but with UIP, specifically in Lean…\n\nhttps://arxiv.org/pdf/2511.19142\n\nusing something called “computation paths”:\n\nhttps://arxiv.org/pdf/1107.1901v3\n\nHas anyone tried to read these and do they actually contain any interesting idea? A very cursory look makes me raise eyebrows; I suspect either it doesn't actually work (I don't see that they are giving a model anywhere) or it can be described in 1 line like “2-level type theory modified in $WAY” but they don't say it.",
"sig": "7060f6c4c8b33f15d7fa04cff7cbe052cd89bd441e436eeb3f0ce065493c195693bafbd1df7eec8ec9471711695387ad5f25d152c62b258ad3b0ed4b216d1136"
}