Nathan van Doorn

Thank you, this seems to fix the issue for me!

The main thing that's missing from the new `Function.Structures/Bundles`, as I see it, is a notion of equality of functions, analogous to `Function.Equality.setoid` in the old style. I'm not sure...

I think this is a good idea. It should probably also be done for Integers and Rationals, if it hasn't already.

I accept the argument that it shouldn't be in `.Base` but `.Categorical` doesn't feel like the right place to me. Maybe a new `Data.List.Algebraic`?

I'm revisiting is. Was there any problem with putting the properties in `Data.List.Properties`?

I've looked into this a little bit more. `Data.Fin.Permutation.Transposition.List` isn't quite what I expected, in that its "transpositions" can include transpositions between two equal elements, like `1F , 1F`. This...

I was planning on changing the definition of `decompose` along with this change. I don't expect that that'll be too hard

Looking into this some more, a lot of the little lemmas about parity of a permutation are lemmas about the parity of a natural number, and that'll require a bit...

I'm... uncomfortable with this definition of vector spaces. It's really not what literature means by "vector space", like, at all. If anything I'd call this a free inner-product module, but...

I'd also prefer `Equivalence`. There's a lot of equivalence relation that aren't equality (equivalence modulo n, for one, and `Always` for another). The downside of that name is `Equivalence.Propositional` is...