I just wrote up a brief account of my (probably shaky) understanding of what Narya is doing with "canonical types" -- might be interesting to other people who are writing elaborators and are interested in Narya's strategy. I'd also like to know if this strategy is original to Narya; I haven't seen it anywhere else but I'm fairly new to this game so perhaps it appears in another guise elsewhere.
https://owenlynch.org/blog/nominal-types-via-energies
Owen Lynch
npub1cj…fxs07
2026-02-08 15:49:49 UTC
Author Public Key
npub1cjyyl7y66997ewku92pzvvhkyec43k7cde44rhgayxdwwl63axdqafxs07Seen on
wss://relay.ditto.pubPublished at
2026-02-08 15:49:49 UTCEvent JSON
{
"id": "63719de49bbf41a6c91e39fef644c232e2cae484acb7e01fbf5493a187ae75f0",
"pubkey": "c4884ff89ad14becbadc2a822632f6267158dbd86e6b51dd1d219ae77f51e99a",
"created_at": 1770565789,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/users/olynch/statuses/116035799570892261",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub"
]
],
"content": "I just wrote up a brief account of my (probably shaky) understanding of what Narya is doing with \"canonical types\" -- might be interesting to other people who are writing elaborators and are interested in Narya's strategy. I'd also like to know if this strategy is original to Narya; I haven't seen it anywhere else but I'm fairly new to this game so perhaps it appears in another guise elsewhere.\n\nhttps://owenlynch.org/blog/nominal-types-via-energies",
"sig": "434685e58eb596468b9407a00bb5284fbcbd6ce256d4baddc1a0e325ce5aa9522e92c3c1229635c480f3e02bafde3137319d7f14ec45f93c3ab1856e899d1481"
}