nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyre3nlvve9v0ulm6elkwv5xpr6azl5f3n9u2c3fdjk4733lxa5ypgdzdh59 (nprofile…dh59) That looks exactly like what Coquand published under the name “paradox of trees” https://doi.org/10.1007/BF01995104 (he attributes the idea to De Bruijn).
In the abstract, he writes that it's open whether such a construction is possible without W-types. I'm not aware of any newer developments.
Jean Abou Samra (new account)
npub14p…htzwd
2025-12-18 23:27:13 UTC
in reply to nevent1q…ppmg
Author Public Key
npub14pv6xjcsz2qa6tctew034s5wsj5p2xuh65q86qe6gpegaslstc6qjhtzwdSeen on
wss://relay.ditto.pubPublished at
2025-12-18 23:27:13 UTCEvent JSON
{
"id": "58a3fd94ce172e1c72d40d7b0fbda4432be905fedb289a6611f7def24dbb541d",
"pubkey": "a859a34b101281dd2f0bcb9f1ac28e84a8151b97d5007d033a40728ec3f05e34",
"created_at": 1766100433,
"kind": 1,
"tags": [
[
"p",
"f319fd8cc958fe7f7acfece650c11eba2fd1319978ac452d95abe8c7e6ed0814",
"wss://relay.ditto.pub/"
],
[
"p",
"391c4888d658cd76271c2400f2fa79b51e881a99cf72a3a29c884c2cc71f49c7",
"wss://relay.ditto.pub/"
],
[
"e",
"8d6ee0108d82d111477d260459cc38accaba3348824034812378a0af6d31f3a1",
"wss://relay.ditto.pub/",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/jeanas/statuses/115743158028760524",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyre3nlvve9v0ulm6elkwv5xpr6azl5f3n9u2c3fdjk4733lxa5ypgdzdh59 That looks exactly like what Coquand published under the name “paradox of trees” https://doi.org/10.1007/BF01995104 (he attributes the idea to De Bruijn).\n\nIn the abstract, he writes that it's open whether such a construction is possible without W-types. I'm not aware of any newer developments.",
"sig": "a997040c49f3859507a5d92a06a99850b1be614f9091f8816f37bfa99480a05c62d8728574d41c2610962412c01924e8fb2cb8ed0e0092359d791a1762728bf7"
}