Jacques Carette
Jacques Carette
I certainly don't mind if a Draft PR, to shake things out, is built "in the wrong place" for parts of its contents.
Re: `∃[x∈xs] P xs = ∃ λ x → x ∈ xs × P x`. This still doesn't strongly hint to me that there's a `P` coming after that. Though...
```agda [_] : {I : Set} (I -> Set) -> Set [ P ] = forall {i} -> P i ``` It's really infix `Box` in ASCII.
Your first perspective (as true as it may be) doesn't seem to bear onto the problem: it's about usability. The fancier the explanation, the less likely it's going to communicate...
Needs a re-review by @MatthewDaggitt
There is a downside to that: a bijection to `Fin` also gives an ordering. Which means that all finite setoids inherit an ordering by transporting it along the bijection. The...
I guess what I'm saying is that maybe this should be called `StronglyFinite` rather than `Finite`. Then such a type would be quite useful indeed.
Good point: indeed there are times when we have no choice, because the implementation scheme for `where` is also sub-optimal.
That would be great - but we'd need to know how `using` is implemented to see if it's actually a win. Perhaps @jespercockx can enlighten us?
What's a 'tipped' list?