mechvel
mechvel
Two more notes: Algebra/Operations/ is a wrong folder. Its contents needs to merge to the *-theory modules in the files Algebra/Structures*.agda. The same is with Algebra/Properties/.
To separate "Properties" and "Operations" and such to other folders is a wrong idea. A natural approach is to follow the style of the textbooks on algebra: define a Setoid,...
> I'm afraid I'm not a fan of the `Algebra.Structures0`, `Algebra.Structures1` etc. approach as it fails > the meaningful name test. I's impossible to know what is in each module...
I would like more ``_PreservesPred_``.
In mathematics, they say just during centuries "a map f preserves the relation R" (at least in Russian translation).
For example, consider ``` suc-injective : ∀ {m n} → suc m ≡ suc n → m ≡ n suc-injective refl = refl ``` in Data.Nat.Properties. Why does not it...
Can you point concretely, may be with example: what harm can do using the above ``GenericInjective`` or ``InjectiveBy≡`` ? I have shown the advantage, now, please, show a drawback. For...
> I'm afraid tackling the function hierarchy isn't on anyone's immediate list of priorities I do not know precisely whether I am in the _anyone_ list, but for any occasion,...
This is better than ``Injective`` of lib-1.0. The drawback is pushed one level down. The matter is that for a _theory with equality_ injectivity has sense not only for congruent...
I vote for the suggestion by @gallais. Also `pos-*-commute` do exist in lib-1.5. Also even if it is `pos-distrib-*` then at least the equality parts in the signature need to...