mechvel
mechvel
`Algebra.Properties.Magma.Divisibility` reexports several items from `Algebra.Definitions.RawMagma`, but not all of them. For example, if one needs `_∣ˡ_` (which is likely to happen) one is forced to add the import ```...
This is on lib-1.7. Having M : Magma, and needing to use the divisibility `_∣_`, one needs to import Algebra.Properties.Magma.Divisibility. To use other items of Magma, one will be forced...
For ``record IsGCD`` in Algebra.Divisibility, the constructor is ``gcdᶜ`` . But for some other records, the constructor is of kind ``mk``. Probably we need to make it uniform. Personally, I...
Relation.Binary.Structures is parameterized by ``_≈_ : Rel A ℓ``, and it puts ``` record IsEquivalence : Set (a ⊔ ℓ) where field refl : Reflexive _≈_ ... reflexive : _≡_...
Suppose that one has to use ``_+_, divMod, gcd, +-comm`` -- all for Nat. One is forced to write ``` open import Data.Nat ... open import Data.Nat.DivMod ... open import...
I suggest to add to ``Algebra.Definitions.RawMagma `` the proofs for ``_∤_`` which are similar to the proofs ``∣-respʳ, ∣-respˡ, ∣-resp`` . For example, like this: ``` ∤-respˡ : {x :...
lib-2.0 has in Algebra.Properties.CommutativeMagma.Divisibility: ``` ∣-factors : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y) ``` This means "each of factors divides the...
May be ``lib-2.0`` could return to the definition of general divisibility ``_∣_`` to its definition in ``lib-1.7.3`` ? I could not ask this in time, when testing the candidate release,...
lib-2.0-rc1 has Algebra/Properties/Semiring/Exp I undertsand it so that it defines `_^_` for a semiring via importing `_^_` from `*-monoid'. If so, than this has sense, because most of the properties...
`lib-2.0` needs a proof for the following lemma. ``` map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) → (map f) Preserves _⊆_ ⟶ _⊆'_ ```...