nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq2h0xy3u7mmdy6huzs5tfzs48rgvq0csvsxnahqmcpgz0f5vv0n7qqqz6t6 (nprofile…z6t6) that's just terminology that i've heard. by the (-1)-truncation of type i mean the type
\[
\sum_{T:\text{Type}}\prod_{x,y:T}(x=_{T}y)
\]
set is then the 0-truncation, and so on. referring to type above is a bit weird to me, since i'm used to thinking about a hierarchy of universes, but based on jon's earlier posts it seems like he's imagining \(\mathcal{U}_{i} \hookrightarrow_{\text{el}_{i}} \text{Type}\), or something similar? again, i'm not super well-equipped to understand a lot of what i'm reading here
Morgan Arnold
npub1uk…aauja
2025-10-07 18:47:51 UTC
in reply to nevent1q…k00h
Author Public Key
npub1ukp2yqn3atafgxsldwv7483qu6mmvl7s5lgeqtararwzqucgwkuqlaaujaSeen on
wss://relay.ditto.pubPublished at
2025-10-07 18:47:51 UTCEvent JSON
{
"id": "bf6683d0d37ff22e0ff6eaf65a3f4ca022251d851d8d9f9db032a2ff85867746",
"pubkey": "e582a20271eafa941a1f6b99ea9e20e6b7b67fd0a7d1902fa3e8dc20730875b8",
"created_at": 1759862871,
"kind": 1,
"tags": [
[
"p",
"55de62479ededa4d5f8285169142a71a1807e20c81a7db83780a04f4d18c7cfc",
"wss://relay.mostr.pub"
],
[
"p",
"a859a34b101281dd2f0bcb9f1ac28e84a8151b97d5007d033a40728ec3f05e34",
"wss://relay.mostr.pub"
],
[
"e",
"4fb6815d549ed75e9af8df254d0e022e02f74d76eece9f15159e15b09e214bb6",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/mra/statuses/115334373152197911",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.mostr.pub"
]
],
"content": "nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq2h0xy3u7mmdy6huzs5tfzs48rgvq0csvsxnahqmcpgz0f5vv0n7qqqz6t6 that's just terminology that i've heard. by the (-1)-truncation of type i mean the type\n\\[\n\\sum_{T:\\text{Type}}\\prod_{x,y:T}(x=_{T}y)\n\\]\n\nset is then the 0-truncation, and so on. referring to type above is a bit weird to me, since i'm used to thinking about a hierarchy of universes, but based on jon's earlier posts it seems like he's imagining \\(\\mathcal{U}_{i} \\hookrightarrow_{\\text{el}_{i}} \\text{Type}\\), or something similar? again, i'm not super well-equipped to understand a lot of what i'm reading here",
"sig": "5f53f199c1f1bec81b5d2387ff61d0122d518cdeb43a6b8504d78a05b6a3c731db586022efe29cea92144a4dab97b0f7e07912b7711e01c20d8a731f48357d1a"
}