npub1ez3yya8tpgge7lk4jq2zxz0cj3d2mcgev9mffd4ec7tfy84hre4suexnxl (npub1ez3…xnxl) So I think the search still continues for [a computational version of HoTT that is not 10x more complicated than HoTT]. it might be that this search leads us to think differently about computation too…
(For instance, one thing that people usually ignore is the fact that "computationalness” in principle does not require that all computation steps are judgmental: what matters in some of these cases is *effectiveness*.)
Jon Sterling /
npub1hf…9ls8k
2023-09-02 16:32:56
in reply to nevent1q…junq
Author Public Key
npub1hfga8wmley5fzqtttpeupd8hc6s92rykfmzktm8zfdhu9h8exvqsj9ls8kSeen on
wss://relay.nostr.bandPublished at
2023-09-02 16:32:56Event JSON
{
"id": "13cea57e862ecb8ee52045ae24ca1f1d8010ac384c6a0e4c3aeb02d633883f3d",
"pubkey": "ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"created_at": 1693672376,
"kind": 1,
"tags": [
[
"p",
"c8a24274eb0a119f7ed590142309f8945aade119617694b6b9c796921eb71e6b",
"wss://relay.mostr.pub"
],
[
"p",
"5c675fe7561c52f2c0ea8db391d2c3a46556bec9a3c0a4b4f10f234fe03f58ca",
"wss://relay.mostr.pub"
],
[
"e",
"3a61db822ca2ccf0bb6e40cf587713a851b6276ea240eda25521fa0bedc4de1a",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/jonmsterling/statuses/110996512840140813",
"activitypub"
]
],
"content": "nostr:npub1ez3yya8tpgge7lk4jq2zxz0cj3d2mcgev9mffd4ec7tfy84hre4suexnxl So I think the search still continues for [a computational version of HoTT that is not 10x more complicated than HoTT]. it might be that this search leads us to think differently about computation too…\n\n(For instance, one thing that people usually ignore is the fact that \"computationalness” in principle does not require that all computation steps are judgmental: what matters in some of these cases is *effectiveness*.)",
"sig": "c8e3954dbe35539a094c6c1bca52e278c8b3ee2501a5257ecdeda2a96c0243a28f031d7a9846e456bf844babfb5c32041ee815efbc50a31eba1a9491d35ee7af"
}