finite setoid

[HuStmpHrrr]

I am considering a definition of finite setoids, which is a setoid with a bijection to a Fin. then there are a few useful properties:

1. all finite setoids have decidable equality.
2. all finite setoids can be finitely enumerated.
3. there are other things like finite setoids are closed under finite products and sum.

[JacquesCarette]

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 problem here is that you don't want your bijection to be proof-relevant! If you want to see way more details about this, see Brent Yorgey's Ph.D. thesis (for the full repo with all the versions).

I'm not saying don't do this! I'm saying that what you really want is a "Finite" API that may contain a bijection as an implementation, but the API doesn't actually given access to the full details.

[JacquesCarette]

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.

[MatthewDaggitt]

Sounds like a great idea to me. I'd definitely use it! I would suggest maybe putting StronglyFinite under Relation.Nullary.Finite.Setoid with a corresponding module Relation.Nullary.Finite.Propositional?

[MatthewDaggitt]

Actually speaking of this, @HuStmpHrrr don't suppose you have a proof that transitive closure is decidable if the underlying relation is decidable over a strongly finite setoid do you? That's what I really need this for and I'm dreading doing it 😞 Interestingly I think this property may require strong finiteness rather than @JacquesCarette's alternative notion of finiteness.

[HuStmpHrrr]

@MatthewDaggitt I believe that's true. imagine a relation represented as a graph, then the graph is finite and this can be achieved by DFS or BFS. either case, however, seems difficult to implement in type theory.

[WolframKahl]

For “strongly finite”, any concrete (proven) implementation of transitive closure on `Fin n` will serve to “decide transitive closure”; I have section 5.5 “Simple Recursive Star Implementation on `Fin n`” in: ```` @InProceedings{Kahl-2012_AgdaGT1, author = {Wolfram Kahl}, title = {Towards Certifiable Implementation of Graph Transformation via Relation Categories}, pages = {82--97}, DOI = {10.1007/978-3-642-33314-9_6}, booktitle = {Relational and Algebraic Methods in Computer Science, {RAMiCS 2012}}, LNCSbooktitle = {{RAMiCS 2012}}, year = {2012}, editor = {Wolfram Kahl and Timothy G. Griffin}, volume = 7560, series = LNCS, publisher = Springer } ```` Unfortunately not all the code is in the currently-visible version of RATH-Agda yet --- hoping to get to that soon... For non-strongly finite, it will depend what exactly your interface to that is --- some recursive decomposition might still be part of that.

[MatthewDaggitt]

@gallais

In this paper Firsov and Uustalu give different definitions of "finite set"
and formally study their relationships. They also provide combinators to
define functions on finite sets & prove formulas quantified over finite sets.

https://dl.acm.org/citation.cfm?id=2808102

Paper on Firsov's page

[MatthewDaggitt]

See more discussion on this unmerged PR: #2005