nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 (nprofile…6kk0) I eventually plan to relax "convertable" to "is a subtelescope".
The point is though that there is a phase distinction whose open modality "forgets singletons", and first we check subtyping (or convertability) with respect to that, and then we check whether an eta-expanded element of A is an element of B. The eta-expansion "observes" whatever refinements have been put on, in any order, because eta expanding a neutral in a singleton type gives you the unique element of that singleton type.
Owen Lynch
npub1cj…fxs07
2025-10-01 15:19:31 UTC
in reply to nevent1q…9mku
Author Public Key
npub1cjyyl7y66997ewku92pzvvhkyec43k7cde44rhgayxdwwl63axdqafxs07Seen on
wss://relay.ditto.pubPublished at
2025-10-01 15:19:31 UTCEvent JSON
{
"id": "da513b24d6a7c014a0a4de5d6c62ee6b173f48b04f1ffd49936e08af5b7d9052",
"pubkey": "c4884ff89ad14becbadc2a822632f6267158dbd86e6b51dd1d219ae77f51e99a",
"created_at": 1759331971,
"kind": 1,
"tags": [
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.mostr.pub"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.mostr.pub"
],
[
"e",
"55a0b2e0b388fa191b6009b88e07f7246b7003e691b47b55b7e1ea3d70eae0f2",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/olynch/statuses/115299580062666617",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.mostr.pub"
]
],
"content": "nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 I eventually plan to relax \"convertable\" to \"is a subtelescope\".\n\nThe point is though that there is a phase distinction whose open modality \"forgets singletons\", and first we check subtyping (or convertability) with respect to that, and then we check whether an eta-expanded element of A is an element of B. The eta-expansion \"observes\" whatever refinements have been put on, in any order, because eta expanding a neutral in a singleton type gives you the unique element of that singleton type.",
"sig": "261bfabc35c03b3577bd6e6d4a5cc8126ca19388671f36afcb8ba7a142a1cd9ca9826c8e7f99a222fdf6cdb7f267b1755de1161577b2cc831d58f80141826397"
}