agda-stdlib
agda-stdlib copied to clipboard
agda
The Agda standard library
The definitions of `RawFunctor`, `RawApplicative`, &c, by necessity, make it so that their fields (like `__`) only work on functions between types at the same level. This means, for example,...
Currently, whenever we have a generic proof that involves both a non-strict and a strict order we translate from one to the other using `Relation.Binary.Construct.NonStrictToStrict`/`StrictToNonStrict`. This works fine for generic...
The `map` lemmas in `Data.List.Relation.Unary.Grouped.Properties` use functional equivalence rather than relational equivalence, and therefore require a bunch of additional and unnecessary equality constraints. https://github.com/agda/agda-stdlib/blob/8da085e032ce50db75a7bbb63bfa56bddaf8e4ad/src/Data/List/Relation/Unary/Grouped/Properties.agda#L37
Every other property in the algebraic (not to mention in `Relation.Binary` etc.) structures are simply named `assoc`/`comm` etc. unless the structure contains two operators in which case they are prepended...
`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 ```...
Following the structure for non-indexed containers. Putting this out for a first review. I also added an `Example` development: multi-sorted algebras. This should be refactored after also adding a setoid...
Here is a small example that currently fails: ```agda open import Data.Maybe.Base public using (Maybe; nothing; just) open import Data.Unit public using (⊤; tt) open import Reflection.Term public open 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...
I find that the current `Total` for binary relations is a misnomer: Currently there is: ```agde Total : ∀ {a ℓ} {A : Set a} → Rel A ℓ →...
There's been some talk on [Zulip](https://agda.zulipchat.com/#narrow/stream/264623-stdlib/topic/Relation.2EArity/near/242519564) of removing the distinction between `Nullary/Unary/Binary/Ternary` in the `Relation` sub-hierarchies as they are long, noisy and sometimes not very meaningful. I'm broadly in favour...