Nathan van Doorn

Some lemmas to do with transposition lists

5

This is largely preliminaries for #1741, which I'm still playing with how to implement.

Open Algebra.Properties.AbelianGroup for addition in Data.{Integer,Rational}.Properties

1

It contains a lot of properties that I keep reaching for but not finding, that we can add to those modules basically for free. It might also be worth making...

Algebraic structures with stable or decidable equality

1

In light of #1767, it might be useful to have copies of the algebraic hierarchy with _stable_ equality, and with _decidable_ equality Here's a very rough sketch of what this...

- [x] `ℚᵘ` is a `HeytingField` #1959 - [ ] `ℚ` is a `HeytingField` #2194

Parity of a permutation

5

For permutations on finite sets, as we have in `Data.Fin.Permutation`, it's possible to define their [parity](https://en.wikipedia.org/wiki/Parity_of_a_permutation). This isn't hard to define with what's in `Data.Fin.Permutation.Transposition.List`, something like ```agda parity :...

Add properties of the quotient to Data.Nat.Divisibility

2

I'd like there to be certain properties of the quotient of a proof of divisibility, for example: ```agda foo : ∀ {m n} → (m∣n : m ∣ n) →...

Add foldMap and fold

18

List is a free monoid I'd like to have some properties for bag-and-set equality. `foldMap f` is a commutative monoid morphism from lists with bag equality, and an idempotent commutative...

I haven't investigated to see how big this problem is, but `Algebra.Bundles.Ring` is missing at least `+-rawGroup` and `rawNearSemiring`

Add a function to show a rational number as a decimal, to a given precision.

2

I'd like a function to turn a rational into its decimal expansion at a given precision. Perhaps with type `showDecimalAtPrecision : (precision : ℕ) → ℚ → String`, although maybe...

systemd-analyze security reports Hydra's services as all highly exposed and unsafe

1

``` UNIT EXPOSURE PREDICATE HAPPY hydra-check-space.service 9.6 UNSAFE 😨 hydra-compress-logs.service 9.6 UNSAFE 😨 hydra-evaluator.service 9.2 UNSAFE 😨 hydra-notify.service 9.2 UNSAFE 😨 hydra-queue-runner.service 9.2 UNSAFE 😨 hydra-send-stats.service 9.2 UNSAFE 😨 hydra-server.service...