José A. Alonso on Nostr: Reconciling impredicative axiom and universe. ~ Stefan Monnier. ...
Reconciling impredicative axiom and universe. ~ Stefan Monnier. https://hal.science/hal-04859508v1/file/jfla2025-final76.pdf #ITP #Coq #Rocq #HoTT
José A. Alonso /
npub1pma…v8pw
2025-01-12 07:51:43
Author Public Key
npub1pmahhjgr7nr8zmx56purp56y6747tds859tdu0x7rtq6t0ez4cwqfnv8pwPublished at
2025-01-12 07:51:43Event JSON
{
"id": "418d9ba738b51e2ea9175972317e039cd128af1db6c1846db3e827bae5bfe2ea",
"pubkey": "0efb7bc903f4c6716cd4d07830d344d7abe5b607a156de3cde1ac1a5bf22ae1c",
"created_at": 1736668303,
"kind": 1,
"tags": [
[
"t",
"hott"
],
[
"t",
"rocq"
],
[
"t",
"coq"
],
[
"t",
"itp"
],
[
"proxy",
"https://mathstodon.xyz/users/Jose_A_Alonso/statuses/113814293937872788",
"activitypub"
]
],
"content": "Reconciling impredicative axiom and universe. ~ Stefan Monnier. https://hal.science/hal-04859508v1/file/jfla2025-final76.pdf #ITP #Coq #Rocq #HoTT",
"sig": "dbf4b894c0d58ddf18b0b00ffe00b63354dc137b94a851eafb3e285eaf6c6f976f9760dc55e8c051376a805dda56f97d60a7e9e56e330529f01fd1b1084f911f"
}