[ new ] Fin n as a refinement

[gallais]

This version has a better runtime representation
This version lets us have efficient implementations of things like splitAt and quotRem

I have been using this definition in my https://github.com/gallais/agda-tiling DSL and
it makes the library a lot faster.

I almost have feature parity with Data.Fin.Base (I have not implemented e.g. punchOut).

[jamesmckinna]

I think that this all looks great (but see also #2257 and #2292 which took a different angle of attack, focusing on modular arithmetic), but I'm a bit concerned about like-for-like emulation of the existing Data.Fin.Base API, when there are still many open issues drawing attention to... things which could be improved there. So I'm not sure I'd want to saddle us with the maintenance headache of fixing those issues on the new additions.

Also: where does this leave us wrt the 'propaganda' for DTFP with eg using Fin for type-safe/bounds-safe Data.Vec.Base.lookup?

[jamesmckinna]

This all looks fine; lots of potential downstream uses/improvements, but worth landing this sooner rather than later.

[jamesmckinna]

@gallais do you want this badged for v2.4?

[gallais]

I am in no rush but also happy to see it included. I have a deadline today but should be able to have
a look (and merge your proposals; glad the sniping worked!) later this week.

[jamesmckinna]

Lambda extends to rightmost scope so this can simplify to

Suggested change

	¬T-≡ {true} = mk⇔ (contradiction _) (λ ())
	¬T-≡ {true} = mk⇔ (contradiction _) λ()

where moreover I personally prefer λ() as a single unspaced lexeme (except it is in fact two!) for this distinguished use...

[gallais]

Lambda extends to rightmost scope so this can simplify to

I hate this though.

Edit: more details; these two arguments play symmetric roles and I find it strange to break
the symmetry by using this quirk of the language (which I happen to hate).

[jamesmckinna]

The scoping, or the grouping? (That you hate)

[gallais]

The scoping!

[jamesmckinna]

I was persuaded that rightmost made more sense back in the 1990s by Randy, but no longer quite sure how/why. True it's annoying forEquivalence etc, but that's an artefact of using a record constructor rather than a record binding?

[jamesmckinna]

Nice cleanup operation!