Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I’m not sure I understand. I think the “exists” on the page is meant to represent mere existence (truncated sigma in HoTT). Your example falls under this definition.
I think Steve is right. Check out finite object for a discussion of this local vs global distinction.
If “finite” is to be a mere property of a set, then the “global” notions cannot be defined inside the “usual” higher-order internal logic of a topos, which is why the page finite set only discusses the notions that internalize to the “local” ones. Steve is saying we can however define them if we regard finiteness as a structure. Equivalently, we can define them in the internal dependent type theory of the topos, as non-truncated “properties” using a $\Sigma$ instead of an $\exists$. If we want a consistent way to refer to the latter notions, I suppose “strongly” isn’t too bad, although a more descriptive word might be something like “algebraically”.
By the way, Steve, if you want to make [links](like this)
you need to select the “Markdown+Itex” radio button below the text box when you post (which should be the default).
Oh I see. But there’s still some further distinction, then, between finite sets of the form $Fin(n)$ for some element $n:Nat$, and those of the form $Fin(n)$ for an external natural number $n$. (These differ over disconnected bases.)
So maybe we can say strongly finite and externally finite, respectively?
Edit to add: Instead of strongly finite set we could also just say totally ordered finite set. That seems to be unambiguous.
Yes, that’s true.
I don’t like “totally ordered” because I wouldn’t want to consider the ordering part of the structure. That is, an isomorphism between strongly finite sets shouldn’t have to respect the orderings.
Now I’m confused again: If you want the identity type of StronglyFiniteSet to correspond to isomorphism, then you’re back to the usual (Bishop / decidable K) FinSet, right? (Form the pregroupoid of strongly finite sets and isomorphisms and Rezk/stack complete.)
I thought the point was that StronglyFiniteSet should be equivalent to (internal) Nat. But maybe the point is really that you’re interested in the pregroupoid (or precategory) structure on Nat/StronglyFiniteSet?
It’s true that if “strongly finite” has the total order as part of the structure, then the corresponding homomorphisms have to preserve it. However, that doesn’t stop you considering other morphisms and in fact that’s exactly what you do when constructing the classifying toposes for various theories. There are five examples in which each is classified by a presheaf topos $[C, Set]$ where $C$ has strongly finite sets as objects, but varied morphisms. More economically, we can take the objects to be natural numbers. Then $C$ can be constructed internally in any elementary topos with nno (or arithmetic universe, for that matter).
Sets $C$ has, for morphisms, arbitrary functions between the corresponding finite cardinals.
Sets with decidable equality. The corresponding structure, which must be preserved by homomorphisms, is the inequality relation. Hence homomorphisms are injective. The morphisms of $C$ are injective functions between the finite cardinals.
Kuratowski finite sets. The structure is the finite subset (element of the free semilattice) that contains all the elements, and homomorphisms preserve this and so are surjective. The morphisms of $C$ are surjective functions between the finite cardinals.
Kuratowski finite sets with decidable equality Homomorphisms are isomorphisms The morphisms of $C$ are isomorphisms between the finite cardinals, so $C$ is a groupoid.
Kuratowski finite sets with decidable equality and decidable total order. Homomorphisms are order preserving isos - so there’s at most one. The morphisms of $C$ are identity functions between the finite cardinals, so $C$ is just the discrete category on N.
A similar principle applies to theories of algebras, where the classifying topos is that of covariant functors to $Set$ from the category of finitely presented algebras. Again, “finitely” is interpreted in the strong way, so that we have the category of strongly finite presentations.
1 to 7 of 7