M Theory Lesson 83

Underlying the Abel summation game is the concept of stuff type, discussed in the context of quantum mechanics by Baez and Morton.

Now as Tony Smith points out, we are not necessarily interested in groupoids as a basis for cardinality. With types as functors into Set, the source is the category FinSetB of finite sets and bijections, which looks a lot like the ordinals $\mathbb{N}$ except that there are many sets representing each $n \in \mathbb{N}$. Is this a nice category? Not really. In contrast, the category FinSet of finite sets and all functions is a topos: it is closed under Cartesian product, function sets Hom(A,B) act as exponential objects, and the usual characterising squares for Boolean logic are still pullbacks. A functor $G$ from FinSet to Set is a functor between toposes, albeit not a special topos kind of functor.

Could we replace a functor $F$ from FinSetB to Set with a functor $G$? It doesn't look like there is any nice way to do this: FinSet has an awful lot more arrows in it than FinSetB, because there are a lot of functions between two sets that don't happen to give a bijection. Nonetheless, it looks like an interesting question about the universality of a functor $I$ from FinSetB to FinSet, and if we view this question from the undefined world of higher topos (or logos) theory then perhaps there is a way to axiomatise a category of categories so that such a special functor exists.

Note also that a major motivation for the higher logos theory was the chance to view categorical dimension itself as cardinality in an abstract sense, which means a constructive approach to weak n-category theory as a whole. I think the Crans paper (which Schreiber is suddenly keen on) is one of few interesting attempts to understand higher categories in this way.