nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) Here's a thought for definitionally irrelevant propositions which have good support for unification: use a phase distinction!
Specifically, there is a phase distinction for refinement types whose open modality erases the refinement. If the typing judgment is "open-modal" with respect to this, then during conversion checking anything that is purely closed-modal can be treated as a singleton.
Then, you can have a universe of propositions SProp for which El P is always closed-modal and so definitional proof-irrelevance for El P doesn't mess with unification at all.
The problem, of course, is that (following up from a recent toot) a function
(1/-) : { x : R | x != 0 } -> R
must in fact be defined on all of R in the base type theory... So this doesn't do everything that one might wish for from strict propositions, but perhaps this is still an improvement.
I think the trick would be to figure out the right interaction between SProp and Prop; I will think about this a bit but perhaps you already have some ideas.
Owen Lynch
npub1cj…fxs07
2025-11-24 17:17:11 UTC
Author Public Key
npub1cjyyl7y66997ewku92pzvvhkyec43k7cde44rhgayxdwwl63axdqafxs07Seen on
wss://relay.ditto.pubPublished at
2025-11-24 17:17:11 UTCEvent JSON
{
"id": "8161446f16efd9952c803259d02057d5016764cfd1b7db26e1bd8adb23cfadd6",
"pubkey": "c4884ff89ad14becbadc2a822632f6267158dbd86e6b51dd1d219ae77f51e99a",
"created_at": 1764004631,
"kind": 1,
"tags": [
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.ditto.pub/"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.ditto.pub/"
],
[
"proxy",
"https://mathstodon.xyz/users/olynch/statuses/115605807526615183",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe Here's a thought for definitionally irrelevant propositions which have good support for unification: use a phase distinction!\n\nSpecifically, there is a phase distinction for refinement types whose open modality erases the refinement. If the typing judgment is \"open-modal\" with respect to this, then during conversion checking anything that is purely closed-modal can be treated as a singleton.\nThen, you can have a universe of propositions SProp for which El P is always closed-modal and so definitional proof-irrelevance for El P doesn't mess with unification at all.\n\nThe problem, of course, is that (following up from a recent toot) a function\n\n(1/-) : { x : R | x != 0 } -\u003e R\n\nmust in fact be defined on all of R in the base type theory... So this doesn't do everything that one might wish for from strict propositions, but perhaps this is still an improvement.\n\nI think the trick would be to figure out the right interaction between SProp and Prop; I will think about this a bit but perhaps you already have some ideas.",
"sig": "0cffd0f3bab59592818df17a8792c59ea1cf4e1226ef54dc8d644dbd546c2889428b44afcf982edc68d3070dc1c74fc4b79ff9d5848602c94e39002292376b31"
}