On function spaces for orbit-finite sets

Joint work with Tito Nguyen and Rafał Stefański. Orbit-finite sets are a generalisation of finite sets, and as such support many operations allowed for finite sets, such as pairing, quotienting, or taking subsets. However, they do not support function spaces, i.e. if X and Y are orbit-finite sets, then the space of functions from X to Y is not orbit-finite. We propose two solutions to this problem: one generalises the notion of orbit-finite set, and the other one restricts it. Curiously, both solutions are “linear": the generalisation is based on linear algebra, while the restriction is based on linear logic.