nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq9wddcelhs6gvweg09c8d53hjns2khzlmh4dgy2mqfjhqxx5nfepquflgwr (nprofile…lgwr) nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq65uwh044df57gvskvnzk8h3quenfsdym64rjymdfeav7xe7gfmsq42ktwk (nprofile…ktwk)
I am sure you can translate this Agda proof by induction on natural numbers to MLTT:
https://martinescardo.github.io/TypeTopology/UF.DiscreteAndSeparated.html#2460
Martin Escardo
npub1t3…fg3z4
2025-07-01 20:30:26 UTC
in reply to nevent1q…gs89
Author Public Key
npub1t3n4le6kr3f09s823keer5kr53j4d0kf50q2fd83pu35lcpltr9q0fg3z4Seen on
wss://relay.mostr.pubPublished at
2025-07-01 20:30:26 UTCEvent JSON
{
"id": "85e9affe09b8b47033cd4470f0fa6f8729b50a4b68f4c7659bb18ca7c25f570b",
"pubkey": "5c675fe7561c52f2c0ea8db391d2c3a46556bec9a3c0a4b4f10f234fe03f58ca",
"created_at": 1751401826,
"kind": 1,
"tags": [
[
"p",
"2b9adc67f78690c7650f2e0eda46f29c156b8bfbbd5a822b604cae031a934e42",
"wss://relay.mostr.pub"
],
[
"p",
"d538ebbeb56a69e4321664c563de20e66698349bd547226da9cf59e367c84ee0",
"wss://relay.mostr.pub"
],
[
"p",
"eb1cda06a29fa6db324928163835bdc74cfc337c90c9c5027f3637a9eff3071c",
"wss://relay.mostr.pub"
],
[
"p",
"1c9eafa564da64022d29e7ee9c06c44328cb1518acf71a50f82030348ba6cd24",
"wss://relay.mostr.pub"
],
[
"e",
"78a42b35c1239b1e7b8f2f46fe101083178aa29ce8a5ca9a3d620c650593309b",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/MartinEscardo/statuses/114779870109407818",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.mostr.pub"
]
],
"content": "nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq9wddcelhs6gvweg09c8d53hjns2khzlmh4dgy2mqfjhqxx5nfepquflgwr nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq65uwh044df57gvskvnzk8h3quenfsdym64rjymdfeav7xe7gfmsq42ktwk \n\nI am sure you can translate this Agda proof by induction on natural numbers to MLTT:\n\nhttps://martinescardo.github.io/TypeTopology/UF.DiscreteAndSeparated.html#2460",
"sig": "1fbe4423fc6279f27c48298b927cb31b830e40e46f7fa33fe8d3fed229fce2078dab81da94dc90fc8bcf5567ff2a87fa1c577bea8abc26bd652a10cba73e3ff8"
}