Nathan van Doorn

Can we unify Relation.Binary.Morphism.Definitions and Function.Definitions?

2

`Relation.Binary.Morphism.Definitions` has as module parameters the domain and codomain of the functions over which the definitions are made, whereas `Function.Definitions` has them in a `variable` block. The former module only...

"Non-exhaustive patterns in function render" for ElmConstructor

1

There is no pattern corresponding to `MultipleConstructors` in the `render` function in the `HasDecoder` instance of `ElmConstructor`

Clarify rule two

2

Rule 2 currently says: > _Non-breaking change_. Otherwise, if only new bindings, types, classes, non-orphan instances or modules (but see below) were added to the interface, then A.B **MAY** remain...

Real numbers, based on Cauchy sequences

18

***Very much work-in-progress*** From previous attempts, multiplication of real numbers will be the stalling point. But the HoTT book suggests this can be implemented in terms of addition, subtraction, and...

Implement ≤-total in terms of _≤?_

10

Fixes #2436

Data.Nat.Properties.≤-total should be implemented with _<ᵇ_

14

It's very slow for `≤-total` to decide which constructor to use, especially compared to `≤?`. This is an issue using `Data.Nat` with code generic over a `TotalOrder` - it's far...

Data.List.upTo/applyUpTo can be made faster

4

In a quick experiment, the following definition runs circles around the current implementation of `upTo` ```agda goUpTo : ℕ → ℕ → List ℕ goUpTo _ 0 = [] goUpTo...

Rename slice functors

1

Extracted from https://github.com/agda/agda-categories/pull/408

Opening this PR to share my WIP. I've got a messy proof of the Chinese remainder theorem for arbitrary rings, but in porting it from my standalone library to this...