julesh on Nostr: As far as I can tell, HoTT is about making types into (∞,0)-categories (aka ...
As far as I can tell, HoTT is about making types into (∞,0)-categories (aka ∞-groupoids), and the directed HoTT folks want to make types into (∞,∞)-categories (aka ∞-categories), but I reckon you could already get a lot of mileage if you could make types into (∞,1)-categories (aka categories, up to the amount of weakness I expect to be necessary in type theory). And that sounds probably a bit easier.
Published at
2025-06-26 18:55:12 UTCEvent JSON
{
"id": "fbc47bf61d45bd545c77f4a28dfbe935ddfd8a507f6efcbb5223f60899ce2812",
"pubkey": "d2bac57e502c36f3456f190627f30396bbe7df233bf7edbfe35990f3e85cf447",
"created_at": 1750964112,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/users/julesh/statuses/114751184102212318",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.mostr.pub"
]
],
"content": "As far as I can tell, HoTT is about making types into (∞,0)-categories (aka ∞-groupoids), and the directed HoTT folks want to make types into (∞,∞)-categories (aka ∞-categories), but I reckon you could already get a lot of mileage if you could make types into (∞,1)-categories (aka categories, up to the amount of weakness I expect to be necessary in type theory). And that sounds probably a bit easier.",
"sig": "2337df33a255c3622e72bec0c733fb80709764366376898c607b94208d4c5bea707dbb6af79698b2dfd42550754f47a5d2e06320339b70f96cec6419e31e404e"
}
