nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqcrf9w5kl4wd5c5dz52qp92ee6xm59naphqrn4s4decyc5cqch4aqdld423 (nprofile…d423) writes "Just finished an Agda proof that I started 3 years ago"
Congratulations!
Happens to me all the time.
What also happens is that I take several years to find time to write papers on what is already done there.
The backlog is giant.
But the frontlog, to use a neologism erroneously, is 26 papers already produced from TypeTopology (not all with me as a (co)author).
Martin Escardo
npub1t3…fg3z4
2026-02-02 20:03:12 UTC
in reply to nevent1q…p740
Author Public Key
npub1t3n4le6kr3f09s823keer5kr53j4d0kf50q2fd83pu35lcpltr9q0fg3z4Seen on
wss://relay.ditto.pubPublished at
2026-02-02 20:03:12 UTCEvent JSON
{
"id": "44d9a7c01b9b110161606a3f27fac835ec79813c30e1cd01682fb577f6b1f699",
"pubkey": "5c675fe7561c52f2c0ea8db391d2c3a46556bec9a3c0a4b4f10f234fe03f58ca",
"created_at": 1770062592,
"kind": 1,
"tags": [
[
"p",
"c0d25752dfab9b4c51a2a28012ab39d1b742cfa1b8073ac2adce098a6018bd7a",
"wss://relay.ditto.pub"
],
[
"p",
"6ee7a8bc68fd2815f988ce75f2c5ee48240d48642fa37024af4c3564184b134e",
"wss://relay.ditto.pub"
],
[
"e",
"c71f6347e97dcf6ba73005f710d8b222741f560c4c4cc85b9d2d28cac012b6b9",
"wss://relay.ditto.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/MartinEscardo/statuses/116002822074862778",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub"
]
],
"content": "nostr:nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqcrf9w5kl4wd5c5dz52qp92ee6xm59naphqrn4s4decyc5cqch4aqdld423 writes \"Just finished an Agda proof that I started 3 years ago\"\n\nCongratulations!\n\nHappens to me all the time.\n\nWhat also happens is that I take several years to find time to write papers on what is already done there.\n\nThe backlog is giant.\n\nBut the frontlog, to use a neologism erroneously, is 26 papers already produced from TypeTopology (not all with me as a (co)author).",
"sig": "29a96cf1efe7b92ca7e730cf301b6c2ca406eb0d77163e67586492f28ce023329b9a36c58f13c834072ad38960563e8798db97340d1d7114dd538e3a59af69c6"
}