nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 (nprofile…6kk0) OK, this was roughly my understanding so I'm glad I wasn't missing something.
By the way, this all reminds me of nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqtc5szsf8gs54cuursvgzkp8t04thtvr7ytgxcr88w6kxnkn83tls4euzsf (nprofile…uzsf)'s Coda project, which sadly got more or less abandoned. https://github.com/ekmett/coda/. The way he explained it to me was roughly that typeclasses should be a poset along with a (not necessarily injective) functor to the category of module signatures and functors between them. Adding new ways of deriving typeclasses from other type classes involves also proving as a side condition that any introduced diamonds are trivial.
Owen Lynch
npub1cj…fxs07
2025-10-02 19:02:07 UTC
in reply to nevent1q…xx0z
Author Public Key
npub1cjyyl7y66997ewku92pzvvhkyec43k7cde44rhgayxdwwl63axdqafxs07Seen on
wss://relay.ditto.pubPublished at
2025-10-02 19:02:07 UTCEvent JSON
{
"id": "bbc41feffe60a2c4ccda7065ae2d4c279da07e7635fba04d758649afb748db24",
"pubkey": "c4884ff89ad14becbadc2a822632f6267158dbd86e6b51dd1d219ae77f51e99a",
"created_at": 1759431727,
"kind": 1,
"tags": [
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.mostr.pub"
],
[
"p",
"5e2901412744295c738383102b04eb7d5775b07e22d06c0ce776ac69da678aff",
"wss://relay.mostr.pub"
],
[
"p",
"13c3f804574a24fb732f9bbcf2f162740f64171fe906ada0c746e09d71c1fad9",
"wss://relay.mostr.pub"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.mostr.pub"
],
[
"e",
"a5de87a2495dd6f64898ec6299573ec958001e8204ea07bcb17196451c789908",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/olynch/statuses/115306117686751549",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.mostr.pub"
]
],
"content": "nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 OK, this was roughly my understanding so I'm glad I wasn't missing something.\n\nBy the way, this all reminds me of nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqtc5szsf8gs54cuursvgzkp8t04thtvr7ytgxcr88w6kxnkn83tls4euzsf's Coda project, which sadly got more or less abandoned. https://github.com/ekmett/coda/. The way he explained it to me was roughly that typeclasses should be a poset along with a (not necessarily injective) functor to the category of module signatures and functors between them. Adding new ways of deriving typeclasses from other type classes involves also proving as a side condition that any introduced diamonds are trivial.",
"sig": "9f54673f833813e5123c4418f594a30d2523d0682891e802f6052568e2b06a2bf04465ca8fea656e92c8acdcad920e0cdac7b30148cb6dfadc8891bb2ee5ccfe"
}