nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyr2u6559vtv0nfk2m0995f4vcahyyktsy42ay7zdztq6e2uklmwqjwwp3nn (nprofile…p3nn)
Is Agda any better? I started using it because Lean doesn't do HoTT. Plus there is Cubical Agda.
Bartosz Milewski
npub15c…wczp5
2025-12-20 17:19:58 UTC
in reply to nevent1q…xsmd
Author Public Key
npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5Published at
2025-12-20 17:19:58 UTCEvent JSON
{
"id": "913e3e2f44e4d6858a0b16dc71b6b2293736c5c3ac87e86bd7c295588e1a55c5",
"pubkey": "a60a88374d8e1cf092c7ea93662aa784fb33b3e75be7725017032e6929ebc5d5",
"created_at": 1766251198,
"kind": 1,
"tags": [
[
"p",
"d5cd528562d8f9a6cadbca5a26acc76e4259702555d2784d12c1acab96fedc09",
"wss://relay.ditto.pub/"
],
[
"p",
"d2bac57e502c36f3456f190627f30396bbe7df233bf7edbfe35990f3e85cf447",
"wss://relay.ditto.pub/"
],
[
"e",
"a1858f32d79140a0c9c8a7b1030ce696c31b5d3bfe7d3a9b610a05c16139c339",
"wss://relay.ditto.pub/",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/BartoszMilewski/statuses/115753038552554192",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyr2u6559vtv0nfk2m0995f4vcahyyktsy42ay7zdztq6e2uklmwqjwwp3nn \nIs Agda any better? I started using it because Lean doesn't do HoTT. Plus there is Cubical Agda.",
"sig": "75de6ff805060b8c6fffcd58b613dc6eef906454768b34d5d1dd573c5a3e4944d58e9f24479ad51ed11f5de6f5502171ff188443d9bbc39b15ce91bd1ba74fc5"
}