Skip to content

Add algebra morphism identity and composition constructions #1502

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 6 commits into from
Jun 20, 2021
Merged

Add algebra morphism identity and composition constructions #1502

merged 6 commits into from
Jun 20, 2021

Conversation

Taneb
Copy link
Member

@Taneb Taneb commented May 14, 2021

Closes #1500

I made slight changes to the IsLattice and Lattice records.

Parts of this PR worry me that the definition of RingHomomorphism etc is incorrect, as they carry two proofs that the function is congruent modulo the equivalence relation, and as such don't provide any directly

MatthewDaggitt
MatthewDaggitt reviewed May 16, 2021
View reviewed changes
Copy link
Contributor

@MatthewDaggitt MatthewDaggitt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the PR! Looks like quite a tedious one so cheers for doing it.

I've added a few comments that should help reduce some the code needed.

src/Algebra/Structures.agda Outdated
@@ -250,6 +250,42 @@ record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
∨-congʳ : RightCongruent ∨
∨-congʳ y≈z = ∨-cong y≈z refl

∨-isMagma : IsMagma ∨
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm these already exist in Algebra.Properties.Lattice. Not saying that's the right place for them, but using them from there minimises the changes need in this particular PR.

@MatthewDaggitt MatthewDaggitt added this to the v1.7 milestone May 16, 2021
@MatthewDaggitt
Copy link
Contributor

@Taneb apologies I somehow missed your comment. I've now answered that. Just to say that if you would like to get this included in the upcoming v1.7 release, it'd be great to get this wrapped up relatively soon so I can include it in the release candidate 👍

@MatthewDaggitt MatthewDaggitt removed this from the v1.7 milestone May 27, 2021
@MatthewDaggitt
Copy link
Contributor

Parts of this PR worry me that the definition of RingHomomorphism etc is incorrect, as they carry two proofs that the function is congruent modulo the equivalence relation, and as such don't provide any directly

Yes, the situation is not very pleasing, I agree. If you have any practical suggestions to fix it, please do open an issue or a PR?

@MatthewDaggitt MatthewDaggitt added this to the v1.8 milestone Jun 13, 2021
@MatthewDaggitt MatthewDaggitt merged commit d8d9248 into agda:master Jun 20, 2021
@MatthewDaggitt MatthewDaggitt modified the milestones: v1.8, v2.0 Jul 6, 2021
@Taneb Taneb mentioned this pull request Apr 27, 2023
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@MatthewDaggitt MatthewDaggitt MatthewDaggitt left review comments

Assignees
No one assigned
Labels
addition
Projects
None yet
Milestone
v2.0
Development

Successfully merging this pull request may close these issues.

Proofs that identity and composition of homomorphisms are homomorphisms
2 participants
@Taneb @MatthewDaggitt