Add a notion of finite algebraic structures

[Taneb]

e.g. a group is finite if there exists order : ℕ with isFinite : Bijection setoid (≡-setoid (Fin order)).

There's also the constructive notion of subfinite structures, which only have an injection to some finite set, for example arbitrary subgroups of finite groups.

I was imagining this going somewhere like {Relation.Binary,Algebra}.Finite.{Structures,Bundles}

[gallais]

Is this #863?

[Taneb]

Is this #863?

I hadn't seen that issue! And it's definitely related. But this issue goes further, asking for finite groups and not just finite setoids. The discussion in #863 is relevant, though.