-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Consequences of module monomorphisms #2276
base: master
Are you sure you want to change the base?
Conversation
Can we have a global comment about the purpose of the PR? IIUC, a |
@jamesmckinna I'm not sure what you're asking for there. I don't think |
I think I'd been trying to understand what you were doing in (something like) the following terms (a lifting property from
But it seems as though what you have is doing something else here? |
As for doing things generically, yes, your point is well-made. But I think the 'lifting' idea above is something to look out for generally when thinking about 'concrete categories' such as |
I think @jamesmckinna is simply asking: can you explain in plain English what you are trying to achieve here? It's not clear just from the code itself. |
What I'm trying to achieve here: I want a quick and easy way to prove that I have a module given that I have a raw module and a monomorphism to some other module. |
Re: the discussion above about |
Looking at the parametrisation of the various constructions, I can't help but see this as further argument in favour of #2252 , but in any case without having to address that issue head-on, you might still consider making all of these definitions inside anonymous modules which would allow you to avoid the [DRY] anti-pattern of But taking #2252 more seriously, your operations coul all be parametrised on If I had more time today, I'd re-draft a specimen instance for comparison... but that will have to wait for now. UPDATED: my proposal founders on the coupling of |
@jamesmckinna I've made things a bit simpler with modules. Thanks for the suggestion! I don't know how much #2252 will help, though |
Progess:
Creating this PR now to get feedback as soon as possible. I'm intending to add to it as I have the energy.