Tidy up and expand morphism hierarchies #958
Conversation
| field | ||
| isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧ | ||
| homo : Homomorphic₂ ⟦_⟧ _∙_ _◦_ | ||
|
|
There was a problem hiding this comment.
I would expect a MagmaHomomorphism to be between two magmas.
Why are the bundles unpacked here?
There was a problem hiding this comment.
So yes, we could parameterise the structures with RawMagma, RawMonoid, RawRing etc. This would be much neater, particularly once we get up to rings, but I wasn't sure whether consistency was better as we don't have the corresponding "raw" structures for the Relation.Binary.Morphism hierarchy.
There was a problem hiding this comment.
If this is possible, I also would be in favor of parametrizing these algebraic morphisms by the raw structures, even if this is inconsistent with morphisms of relations.
Note that they cannot be parametrized by the non-raw structures Magma or Monoid in their current form, as the main purpose of Algebra.Morphism.MagmaMonomorphism is to prove that the domain of a monomorphism is a magma, etc. – although one could argue this is part of the definition of morphisms of magmas or monoids. On the other hand, one might argue that this rather is part of the definition of the corresponding category and not necessary in the definition of the morphisms themselves.
|
Thank you for putting this together. This looks pretty good to me and seems much more consistent than what I tried at #853. This PR removes the raw morphisms altogether. They did not form a mathematical category, as identity morphisms could not be defined, so I welcome this change. |
| {ℓ₁ ℓ₂} {_≈₁_ : Rel A ℓ₁} {_≈₂_ : Rel B ℓ₂} | ||
| {_∙_ : Op₂ A} {_◦_ : Op₂ B} {f : A → B} | ||
| (isMagmaMonomorphism : IsMagmaMonomorphism _≈₁_ _≈₂_ _∙_ _◦_ f) | ||
| (◦-isMagma : IsMagma _≈₂_ _◦_) |
There was a problem hiding this comment.
This ◦-isMagma argument is redundant for the structures isSemigroup, isBand, etc. below. Perhaps it could be added just for the properties section via an anonymous module, but not for the structures. The same applies for monoids.
There was a problem hiding this comment.
Fair enough. I was just trying to make my life easier for myself, but you're right we shouldn't have it everywhere if we don't need it!
| zero = map zeroˡ zeroʳ | ||
|
|
||
| ------------------------------------------------------------------------ | ||
| -- Properties |
There was a problem hiding this comment.
Should this be Structures?
|
There we go, addressed everyone's feedback I think. |
src/Data/List/#Properties.agda#
Outdated
| @@ -0,0 +1,1061 @@ | |||
| ------------------------------------------------------------------------ | |||
There was a problem hiding this comment.
It looks like this emacs file was committed by accident.
The library has added a lot of morphism code since
v1.1. This PR attempts to tidy it up before the release ofv1.2. In particular it:Definitions+Structures(withBundlesstill to come).Data.Nat.BinaryandData.Rationalto transfer properties) and isomorphisms (yet unused).@mwageringel what are your thoughts?