Fix a countably infinite set of names $𝔸$. A nominal set [1] is a set $𝑋$ equipped with an action by the group of finite permutations $\text{𝖯𝖾𝗋𝗆}(𝔸)$, such that every element $𝑥\in 𝑋$ has a finite support.

A finite set of names $𝑆\subseteq 𝔸$ supports $𝑥$ if any permutation fixing $𝑆$ pointwise also fixes $𝑥$.

The category of nominal sets is equivalent to the Schanuel topos. Under this equivalence, a nominal set $𝑋$ corresponds to a functor $𝕀\to \text{𝐒𝐞𝐭}$, where $𝕀$ is the category of finite sets and injections, given by mapping a finite set of names $𝑡$ to the set of elements supported by $𝑡$:

In the Schanuel topos, the underlying category for Day convolution is $𝐶={𝕀}^{\text{op}}$, where $𝕀$ is the category of finite sets and injections.

Given a nominal set $𝑋$, its presheaf action describes elements supported by $𝑡$:

Instead of taking $𝑋$ a priori as a presheaf, we can view it as a finitely- supported $\text{𝖯𝖾𝗋𝗆}(𝔸)$-set. We can restrict our attention to the groupoid core $𝐺=\text{𝖼𝗈𝗋𝖾}(𝕀)$, asking for the support to be exactly the input:

This family ${𝑋}_{•}:𝐺\to \text{𝐒𝐞𝐭}$ is functorial on finite sets and bijections.

By extending this functor along the inclusions described in Quotient Coincidence, we can extend ${𝑋}_{•}$ to both a presheaf $\text{𝗆𝗄𝖯𝗌𝗁}({𝑋}_{•})$ and a copresheaf $\text{𝗆𝗄𝖢𝗈𝗉𝗌𝗁}({𝑋}_{•})$ on $𝐶$. This suggests the equivalence:

I suspect this allows us to describe name abstraction $[𝑋]𝑌$ [1] —which ordinarily looks like an operation on two presheaves of the same variance—as the quotient of $𝑌$ by the induced copresheaf $\text{𝗆𝗄𝖢𝗈𝗉𝗌𝗁}({𝑋}_{•})$.

Concretely, $[𝑋]𝑌$ is usually given by the quotient of the product by an equivalence relation:

where $(𝑥,𝑦)\sim (𝜋𝑥,𝜋𝑦)$ for permutations $𝜋$ fixing $\text{𝗌𝗎𝗉𝗉}(𝑦)-\text{𝗌𝗎𝗉𝗉}(𝑥)$.

On the other hand, the Day quotient computes to a coend:

A priori, a coend over $𝑠$ of the product ${𝑋}_{𝑠}\times 𝑌(𝑠\uplus 𝑐)$ is expressed as the quotient of a set of triples by an equivalence relation $\approx$:

However, because the comprehension formula fixes $𝑠=\text{𝗌𝗎𝗉𝗉}(𝑥)$, we reduce to a quotient of pairs:

I suspect that this quotient will equate to the one given by $[𝑋]𝑌$, thus resolving the apparent issues with variance. I further suspect that one will need the sheaf condition (pullback-preservation) of nominal sets to establish this equivalence.

Let $𝕀$ be the category of finite sets and injections. The Schanuel topos is the category of pullback-preserving functors ${𝕀}^{\text{op}}\to \text{𝐒𝐞𝐭}$.

Equivalently, it is the category of nominal sets, which are sets equipped with an action by the group of permutations on a countable set of names $𝔸$, such that every element has finite support.