jamesmckinna
jamesmckinna
~~The first is~~ This seems clear, although I wonder a bit about how best we should add `Action`s to the `Algebra` hierarchy, so going via `Construct` seems the best... for...
(Extracted from #2350) Module `Data.List.Relation.Binary.Equality` defines the `Setoid` lifting of equality from a `Setoid` on `A` to one on `List A`. But nowhere that I can find is the `++-[]-monoid`...
This fell originally under #2348 but I think should be factored out on its own. Current issues: * where is the (binary) product of `Setoid`s defined? (plus currying etc.: cartesian-closedness...
I further conjecture on #2329 that all uses of `⊥-elim` can be replaced by their irrelevant version `⊥-elim-irr`... so question for the maintainers, are we prepared to embrace such a...
WORK IN PROGRESS: do not review! Of independent interest to the various competing proposals in #2311 for the 'right' representation, as it attempts to decouple the main properties of the...
(micro-issue arising in the course of #2317 / #2311 ) UPDATED: two instances of what might be considered parsing 'bugs', but might merely be 'peeves'... but the first does seem...
Cherry-picked and enhanced from #1962 . Fixes #1960 . TODO: - [x] the `Algebra.Morphism.Construct.{Identity|Composition}` material - [x] `RingWithoutOne` doesn't appear to export its own `Raw` substructure, so that should be...
This is a partial fix to #2353 but organised slightly differently, for consistency with existing uses of `reverse⁺` and `reverse⁻`, via a self-adjointness property of independent interest itself generalising the...
NB: * missing structures/bundles (I got bored) * `isEquivalence` might already be defined somewhere else, but defined in-place here for the time being
Fixes #1131 NB: no `CHANGELOG` (yet), but adds: * to `Data.List.Relation.Binary.Pointwise` ```agda ++⁺ʳ : Reflexive R → ∀ xs → Pointwise R ys zs → Pointwise R (xs ++ ys)...