Mastodawn

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 thread

J Carr Mar 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 thread

Alex G Mar 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 thread

J Carr

@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.