Remove redundancy in ring morphisms etc #1540
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This redefines NearSemiring, Semiring, and Ring homomorphisms so that they each build up by adding a single new property to a smaller structure. This ensures there's only one proof that they're a Rel homomorphism. For the same reason, Lattice homomorphisms are defined directly rather than showing it's two magma homomorphisms. I've tried to make it so that each of these structures provides any smaller structure at its top level, so if we have a RingMonomorphism we can easily say that it's a MagmaHomomorphism by multiplication or whatever, but I might have missed one or two.
I didn't mean to rename that but I prefer this name
Also add that it's a raw near semiring and semiring while I'm at it
|
@Taneb given the number of great PRs recently, I've also added you to the list of Agda developers. You should now have permission to create PRs on this repo directly if you want to 👍 |
|
I'm going to make a subsequent PR adding modules like |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This redefines NearSemiring, Semiring, and Ring homomorphisms so that
they each build up by adding a single new property to a smaller
structure. This ensures there's only one proof that they're a Rel
homomorphism. For the same reason, Lattice homomorphisms are defined
directly rather than showing it's two magma homomorphisms.
I've tried to make it so that each of these structures provides any
smaller structure at its top level, so if we have a RingMonomorphism we
can easily say that it's a MagmaHomomorphism by multiplication or
whatever, but I might have missed one or two.
Closes #1539