Greg PfeilMar 15
Alex G

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.

Mar 15 at 10:14pmWeb
Show threadJ CarrMar 16

@clayrat Is it not just that K-finite is exactly a quotient of Bishop-finite?
I would use K-finite when you need a listing and Bishop-finite when you need decidable equality. But that's pretty much the entire distinction afaik

For nominal settings you'd want Bishop-finite since you want all the names to be distinct. Or you could use the definition in terms of permutations of N.

Show threadAlex GMar 16
@jac Kidney proves that K-fin is a truncation of manifest enumerability, which a surjection from Fin. I think K-fin is weaker, as it needs discreteness (decidable equality) to compute intersections and cardinality, but it might be that working with membership/subset relations for K-fin is easier, while manifest enum / B-fin (this nomenclature doesn't feel very established) is better for cardinality manipulations?
Show threadJ CarrMar 16

@clayrat A K-fin value is discrete iff it is B-fin. A quotient of a B-fin value is K-fin.
B-finite is precisely the same as having a cardinality which is a natural number.

K-finite is definitely established, I haven't seen B-finite very much as sometimes people just say "finite" I believe.

Show threadWouter Swierstra Mar 16
@clayrat Have you seen this paper by Denis Firsov? https://firsov.ee/finset/
Dependently typed programming with finite sets

Show threadAlex GMar 16
@wouter Yes, this and the follow-up "Variations on Noetherianness", thank you! Kidney's work is more-or-less based on them, and he cites them. I'm working in a setting with quotients/HITs, so I'm mostly interested in the ergonomics of various definitions using those.
Show threadJeremy GibbonsMar 16
@clayrat Paging @oisdk
Show threadDonnacha Oisín KidneyMar 16
@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
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.