The Day quotient, ${𝐷}_{𝐴}𝐵$, takes $𝐴$ to be a covariant functor and $𝐵$ to be a contravariant one. While the residual $𝐴⊸𝐵$ takes both to be contravariant.

This apparent variance mismatch disappears when we restrict to the groupoid core $𝐺=\text{𝖼𝗈𝗋𝖾}(𝐶)$, where variance is trivialized since $𝐺\cong {𝐺}^{\text{op}}$.

For any functor $𝐹:𝐺\to \text{𝐒𝐞𝐭}$ on the core, we can freely extend it to both a presheaf and a covariant copresheaf on $𝐶$ by left Kan extension along the respective inclusions $𝐺\to {𝐶}^{\text{op}}$ and $𝐺\to 𝐶$:

By substituting these extensions into the definitions of the residual and the quotient, we obtain a general coincidence for any $𝐹:𝐺\to \text{𝐒𝐞𝐭}$ and $𝐵:{𝐶}^{\text{op}}\to \text{𝐒𝐞𝐭}$:

This equivalence states that computing the residual against the presheaf extension of $𝐹$ is perfectly isomorphic to taking the quotient by its covariant extension.

The Representable Case

Instantiating the above theorem at a representable functor on the core, $𝐹=𝐺[𝑥,-]$: the co-Yoneda lemma says that the left Kan extensions compute to the representables on $𝐶$:

$$\text{𝗆𝗄𝖯𝗌𝗁}(𝐺[𝑥,-])\cong 𝐶[-,𝑥]$$

$$\text{𝗆𝗄𝖢𝗈𝗉𝗌𝗁}(𝐺[𝑥,-])\cong 𝐶[𝑥,-]$$

Applying the general coincidence theorem, the left and right adjoints coincide precisely on (opposite-variance) representables:

$$(𝐶[-,𝑥]⊸𝐵)(𝑐)\cong 𝐵(𝑥\otimes 𝑐)\cong ({𝐷}_{𝐶[𝑥,-]}𝐵)(𝑐)$$

When $𝐶$ is the discrete monoidal category of strings, this recovers the derivative of formal grammars.

In nominal sets, I suspect that this construction also describes name abstraction and the freshness quantifier, although I have not check all of the details of the proof.