nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) have not thought about it as much. (i've only really thought about this problem for PCAs, where that would be a very strange thing to ask for).
from a code reuse perspective, i think it'd make the most sense to allow fields to concretely specify an implementation of the inverse operation, constrained so the extent is equivalent to apartness from zero (or whatever). then in the case of a discrete field we can simply have the extent compute by cases on the denominator to either the unit or empty types.
tbh, even in the discrete case, i think it's somewhat strange to make inverses a total operation, since you still need to prove things are actually invertible when it comes to reasoning about them. i think keeping it as a "self-deciding" partial operation strikes a good balance between "i have to be honest when reasoning in context" and "i can ask the proof assistant to just normalise a number in anger", since if you're not normalising a stupid number the extent of any combination of field operations will have computed to a big tuple of unit values.
Amélia Liao 🍊😈
npub105…yvwnw
2025-12-02 12:28:57 UTC
in reply to nevent1q…4t9w
Author Public Key
npub105djthvncz3tms6ke37w4579d0qqmf2e6xt9p7z5h3ayq0wtq7pswyvwnwSeen on
wss://relay.ditto.pubPublished at
2025-12-02 12:28:57 UTCEvent JSON
{
"id": "075199a603e7c0274653e11fb789b2bc7d1ebf645e312612a3455f3ab6d69bff",
"pubkey": "7d1b25dd93c0a2bdc356cc7cead3c56bc00da559d19650f854bc7a403dcb0783",
"created_at": 1764678537,
"kind": 1,
"tags": [
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.ditto.pub/"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.ditto.pub/"
],
[
"e",
"7323b71865e598f4e21f91a5ac6efebf1772a94304f09120b7f98cf34115374e",
"wss://relay.ditto.pub/",
"reply"
],
[
"proxy",
"https://types.pl/users/amy/statuses/115649972655663315",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe have not thought about it as much. (i've only really thought about this problem for PCAs, where that would be a very strange thing to ask for).\n\nfrom a code reuse perspective, i think it'd make the most sense to allow fields to concretely specify an implementation of the inverse operation, constrained so the extent is equivalent to apartness from zero (or whatever). then in the case of a discrete field we can simply have the extent compute by cases on the denominator to either the unit or empty types.\n\ntbh, even in the discrete case, i think it's somewhat strange to make inverses a total operation, since you still need to prove things are actually invertible when it comes to reasoning about them. i think keeping it as a \"self-deciding\" partial operation strikes a good balance between \"i have to be honest when reasoning in context\" and \"i can ask the proof assistant to just normalise a number in anger\", since if you're not normalising a stupid number the extent of any combination of field operations will have computed to a big tuple of unit values.",
"sig": "0dc3c6328ea219c75322ee630a0e758614e1ad90e9c8ce44b6821e7c9832c69d5087a23946e8cbced5a8c58c6a2bf406df34bdf8979d715b4ec6870221702c33"
}