Owen Lynch on Nostr: How do typeclasses interact with univalence? It seems like the point of typeclasses ...
How do typeclasses interact with univalence? It seems like the point of typeclasses is to distinguish between isomorphic types, as we might want to put different structures on such types. But this contradicts univalence; is this bad?
Published at
2025-11-01 15:30:02 UTCEvent JSON
{
"id": "3bdfe5fe4f6c4a9aad676500ca24fabf1dd970fdf2ca81d1d649eccb4f221f06",
"pubkey": "c4884ff89ad14becbadc2a822632f6267158dbd86e6b51dd1d219ae77f51e99a",
"created_at": 1762011002,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/users/olynch/statuses/115475153063096624",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "How do typeclasses interact with univalence? It seems like the point of typeclasses is to distinguish between isomorphic types, as we might want to put different structures on such types. But this contradicts univalence; is this bad?",
"sig": "3592f1a6114030d965d97c7985360186b202b1c467c776844ab5c477a3fb47ee8a798e5d3bd2f0bdecf59f9f0ec93783a0e2e887c881a38f9f113d425255d026"
}
