Function spaces for orbit-finite sets
<|reference_start|>Function spaces for orbit-finite sets: 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 finitely supported functions from X to Y is not orbit-finite. In this paper we propose two solutions to this problem: one is obtained by generalising the notion of orbit-finite set, and the other one is obtained by restricting it. In both cases, function spaces and the original closure properties are retained. Curiously, both solutions are "linear": the generalisation is based on linear algebra, while the restriction is based on linear logic.<|reference_end|>
@article{bojańczyk2024function,
    title={Function spaces for orbit-finite sets},
    author={Miko{l}aj Boja'nczyk, L^e Th`anh D~ung Nguy^en, Rafa{l}
  Stefa'nski},
    journal={arXiv preprint arXiv:2404.05265},
    year={2024},
    archivePrefix={arXiv},
    eprint={2404.05265},
    primaryClass={cs.LO cs.FL math.LO}
}