Jon Sterling on Nostr: Does anyone know a *category-theoretic* description of the large elimination rule for ...
Does anyone know a *category-theoretic* description of the large elimination rule for W-types? Obviously I am interested in a treatment that doesn’t use a universe.
Published at
2025-07-02 11:44:37 UTCEvent JSON
{
"id": "30d42a1f45017999a861fcb5c10e13e01b6995d07b46d50ad295c20df4f53455",
"pubkey": "ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"created_at": 1751456677,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/users/jonmsterling/statuses/114783464789325207",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.mostr.pub"
]
],
"content": "Does anyone know a *category-theoretic* description of the large elimination rule for W-types? Obviously I am interested in a treatment that doesn’t use a universe.",
"sig": "0273c2e970f2bdbc9b82951bf3fe13fa7e3250b3569950ea3f79b851e8b9564aab473b5d797b1701e1156a10e2e19e0f45ae211818a923601f0b21e95c1a720e"
}
