Implementing finite structures in Mathematica via a skeletal topos of finite sets

To implement finite structures in a symbolic computation program such as Mathematica, we consider a skeletal toposN which is equivalent to the category Setf of finite sets. Objects of N are nonnegative integers, and morphismsf:n→m are lists (f1,…,fn) of integers such that 1≤fi≤m, for all i. A full and faithful functor from N to Setf is obtained by identifying n with the set [n]={1,…,n} and identifying (f1,…,fn) with the function i fi. A topos structure on N (appropriate for Mathematica) is obtained by transporting the topos structure of Setf along a suitable pseudo-inverse C of the functor from N to Setf described above. The code for the Mathematica implementation included below is also available as a Mathematica Notebook.