nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) Not very useful for mathematics for the reason I mentioned that you would still have to have 1/x defined for x = 0?
I do think that nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyz4g9497lls2ey4v3rxtld6a8m5rh7meav97tqfhnceyja6wn0lpgng99up (nprofile…99up)'s point that mainstream mathematicians really want proof irrelevance is a good one, but perhaps the answer is to teach them that they shouldn't want things they can't have...
Here's an idea to fix the above issue. What if we do something like postulate a neutral
inv : (x : R) -> (y : R) × (p : x ≠ 0) -> (y = 1/(x,p))
where 1/- : (x : R) × (x ≠ 0) -> R is the "normal" definition of inverse.
Then this serve as the "base function" for the refined inverse. Perhaps suitable elaborator support can make moving between two definitions (the definition which takes in the proof as a refinement and the real definition) smooth.
Owen Lynch
npub1cj…fxs07
2025-11-24 17:49:41 UTC
in reply to nevent1q…a8pk
Author Public Key
npub1cjyyl7y66997ewku92pzvvhkyec43k7cde44rhgayxdwwl63axdqafxs07Seen on
wss://relay.ditto.pubPublished at
2025-11-24 17:49:41 UTCEvent JSON
{
"id": "745e9c905a3e49739f0c8e397c417075e49d957c0a5d712c8bc75fb93dd95613",
"pubkey": "c4884ff89ad14becbadc2a822632f6267158dbd86e6b51dd1d219ae77f51e99a",
"created_at": 1764006581,
"kind": 1,
"tags": [
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.ditto.pub/"
],
[
"p",
"aa82d4beffe0ac92ac88ccbfb75d3ee83bfb79eb0be581379e3249774e9bfe14",
"wss://relay.ditto.pub/"
],
[
"p",
"406cda1605d9d95b1e39a78327c3891afba2baecd30a02b403c900e6d3f9bb58",
"wss://relay.ditto.pub/"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.ditto.pub/"
],
[
"e",
"c0eba1f2a77cd065d24e559e76fa8aa51f0c4649fb66825debb41a2b88abe8a5",
"wss://relay.ditto.pub/",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/olynch/statuses/115605935308418766",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe Not very useful for mathematics for the reason I mentioned that you would still have to have 1/x defined for x = 0?\n\nI do think that nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyz4g9497lls2ey4v3rxtld6a8m5rh7meav97tqfhnceyja6wn0lpgng99up's point that mainstream mathematicians really want proof irrelevance is a good one, but perhaps the answer is to teach them that they shouldn't want things they can't have...\n\nHere's an idea to fix the above issue. What if we do something like postulate a neutral\n\ninv : (x : R) -\u003e (y : R) × (p : x ≠ 0) -\u003e (y = 1/(x,p))\n\nwhere 1/- : (x : R) × (x ≠ 0) -\u003e R is the \"normal\" definition of inverse.\n\nThen this serve as the \"base function\" for the refined inverse. Perhaps suitable elaborator support can make moving between two definitions (the definition which takes in the proof as a refinement and the real definition) smooth.",
"sig": "f788b9adcabd6e5639abbe3d841beaaef4058866a3f0779194637e29a1c99e7898e5768f26187e6d61fe08711fcbc958b03e63514428127c678ed8fb70cc56e9"
}