Nathan van Doorn

Remove deprecation notice for binary_cache_secret_key_file

1

It's still used for signing `narinfo` files if using Hydra as a binary cache server. See https://github.com/NixOS/hydra/blob/master/src/lib/Hydra/View/NARInfo.pm#L37 See also issues #548 and #679

Its current location is inconsistent with the rest of the library

More or less copied from the F-Algebras category. I wanted this while I was messing around with recursion schemes a while back.

Add prime factorization and its properties

8

This PR proves that every non-zero natural number has a unique (up to permutation) prime factorization. To this end, it also adds a definition of "rough" numbers (numbers which don't...

Add surjective homomorphisms

1

In `Algebra.Morphism.Structures` and the similar modules for lattices and modules, we define `IsXHomomorphism`, `IsXMonomorphism`, and `IsXIsomorphism`. We do not currently define `IsXEpimorphism`, for morphisms that are surjective but not necessarily...

Consequences of module monomorphisms

11

Progess: - [x] Left semimodules - [x] Left modules - [x] Right semimodules - [x] Right modules - [x] Bisemimodules - [x] Bimodules - [x] Semimodules - [x] Modules Creating...

Mechanize the Algebra hierarchy

11

Many of the modules under `Algebra` (e.g. `Algebra.Structures`, `Algebra.Bundles`, `Algebra.Morphism.Structures`...) are highly structured and repetitive. This makes it a lot of work to add something new, and _very_ easy to...

CI check for changelog markdown syntax

2

As discussed in #2286, the changelog file often ends up with invalid markdown. We should add a CI check to ensure that it remains valid.

Missing reexports in function bundles

2

I've noticed: `LeftInverse`, `RightInverse`, and `Inverse` don't reexport `toFunction` and `fromFunction` from `Equivalence`. `Inverse` doesn't reexport or redefine `equivalence` from `LeftInverse` or `RightInverse`.

Add a vector type with logarithmic-time lookup

1

I haven't benchmarked this yet. I also want to add something corresponding to the standard `Vec`'s `_[_]=_`, and properties relating `head`, `tail`, and `lookup`.