nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzyx3a4ez5l8q73npff5dtjy62j60wjgxduy7e3398qesmafk2eqqnwxk2w (nprofile…xk2w)
In may be a "sensible Agda feature", but it is not MLTT, and it is not how you prove things in HoTT/UF. This is certainly not a proof "without K".
nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe)
Martin Escardo
npub1t3…fg3z4
2025-12-20 12:27:56 UTC
in reply to nevent1q…g6h0
Author Public Key
npub1t3n4le6kr3f09s823keer5kr53j4d0kf50q2fd83pu35lcpltr9q0fg3z4Seen on
wss://relay.ditto.pubPublished at
2025-12-20 12:27:56 UTCEvent JSON
{
"id": "388286df9f4907ab610f12856c32961fb985df006035732c25d63da6066f8ef8",
"pubkey": "5c675fe7561c52f2c0ea8db391d2c3a46556bec9a3c0a4b4f10f234fe03f58ca",
"created_at": 1766233676,
"kind": 1,
"tags": [
[
"p",
"8868f6b9153e707a330a5346ae44d2a5a7ba4833784f663129c1986fa9b2b200",
"wss://relay.ditto.pub/"
],
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.ditto.pub/"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.ditto.pub/"
],
[
"p",
"7d1b25dd93c0a2bdc356cc7cead3c56bc00da559d19650f854bc7a403dcb0783",
"wss://relay.ditto.pub/"
],
[
"e",
"caceb2fe9811b5a50c9d51a734e98e82a8dfdc36c82279738f99373cb6d0d2b3",
"wss://relay.ditto.pub/",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/MartinEscardo/statuses/115751890216142091",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzyx3a4ez5l8q73npff5dtjy62j60wjgxduy7e3398qesmafk2eqqnwxk2w \n\nIn may be a \"sensible Agda feature\", but it is not MLTT, and it is not how you prove things in HoTT/UF. This is certainly not a proof \"without K\".\n\nnostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe",
"sig": "b4ba1c456b5274897eaf619f239f97b33a2e6beb1d0d260b2141e40718837661deba3eb5dc576ce103a2694f0988e9ee557d223a86643f976fbc221f041a7dee"
}