Alex GMar 15

Since we're on the subject, I'm curious if there's a resource that explains the practical difference between using the Bishop style (equivalence with Fin) and the Kuratowski style (list/tree quotient) for finite sets. Donnacha Kidney covers this topic in his master's thesis, but his approach is somewhat one-sided—he reduces the Kuratowski style to the Bishop style. For decidable types, the two approaches seem to be completely equivalent.

I’m trying to figure out the best way to define FinInj and FinSur, as well as how to build a metatheory on top of them for things that Simpson's framework relates to, such as the Schanuel topos and nominal algorithms. I suspect Bishop is more convenient for some things and Kuratowski for others.

Show threadDonnacha Oisín Kidney
@clayrat not aware of any specific resource, but when I formalised some nominal stuff in cubical Agda a while ago I definitely found the list-based definitions to be the most convenient. I think that working directly with surjections from Fin could be terser, but I found it more difficult to figure out the proofs in that setting. Also, I don’t know how true this is anymore, but it’s worth noting that the properties over quotiented trees I used ended up being extremely slow to typecheck
Mar 16 at 9:21pmWeb
Show threadAlex G5d ago
@oisdk Oh yes, I'm sticking to lists and quotiented lists for now, seems to work reasonably well. I think I finally get the picture with Listable analogues, although it's still a bit strange to me that finiteness can be separated from discreteness. I wonder what happens if one uses sets (as lists quotients) instead of lists in the various Noetherian-style predicates.