The setup: Given a formula $\varphi$ of intuitionistic propositional logic (i.e., made from the connectors $\Rightarrow$, $\land$, $\lor$, $\top$ and $\bot$ from propositional variables $A,B,C,\ldots$), by replacing the logical connectors $\Rightarrow$, $\land$, $\lor$, $\top$ and $\bot$ by $\mathop{\mathrm{Hom}}(—,—)$ (set of functions), $\times$ (cartesian product), $+$ (disjoint sum), $1$ (singleton set) and $0$ (empty set) respectively, we define a map $\hat\varphi$ from the class of $r$-tuples of finite sets, where $r$ is the number of free variables of $\varphi$ (or more precisely, from mappings of the free variables of $\varphi$ to finite sets), to finite sets. In more fancy terms, I think I'm supposed to say that $\hat\varphi$ is obtained by the Curry-Howard-Lambek correspondence applied to $\varphi$ for the bicartesian closed category of finite sets.

For example, if $\varphi$ is $\neg A \lor \neg\neg A$ (where $\neg P$ is an abbreviation for $P\Rightarrow \bot$), then $\hat\varphi(A) = \mathop{\mathrm{Hom}}(A,0) + \mathop{\mathrm{Hom}}(\mathop{\mathrm{Hom}}(A,0),0)$ is a singleton for every finite set $A$ (N.B.: the ambient set theory is classical).

Observation: if $\varphi$ is provable intutionistically, then $\hat\varphi$ is inhabited (i.e., nonempty) for every value of its arguments. The above example shows that the converse is not true.

Now define each variable occurrence in $\varphi$ to be either positive (=covariant) or negative (=contravariant): a variable alone is positive, the occurrences in $P\land Q$ and $P\lor Q$ have the same variance as in $P$ and $Q$, but for $P\Rightarrow Q$ the occurrences in $Q$ are the same whereas those in $P$ are flipped (I hope this is clear enough and standard anyway; for example in $((A\Rightarrow B)\Rightarrow A)\Rightarrow A$, the only occurrence of $B$ is positive, the two first occurrences of $A$ are negative and the last is positive).

Say that $\varphi$ has consistent variance when each variable occurs either always positively or always negatively (so $((A\Rightarrow B)\Rightarrow A)\Rightarrow A$ does not have consistent variance, but $(A\Rightarrow B)\Rightarrow A$ does; we agree that if a formula has no variable, it has consistent variance); also say that $\varphi,\psi$ jointly have consistent variance when $\varphi\land\psi$ has consistent variance.

Now when $\varphi$ has consistent variance, $\hat\varphi$ is not just a map of classes from $\mathbf{FinSets}^r$ to $\mathbf{FinSets}$, it's a functor (covariant or contravariant in each variable according to that variable's variance in $\varphi$).

Furthermore, if $\varphi,\psi$ jointly have consistent variance, and if $\psi\Rightarrow\varphi$ is provable intuitionistically (note that this generally does not have consistent variance), we get a natural transformation from $\hat\psi$ to $\hat\varphi$ from the proof (this follows from general nonsense, but it's easy to see by examining the proof rules).

Question: Is the converse of this statement true? That is, if $\varphi,\psi$ jointly have consistent variance and there is a natural transformation $\hat\psi \to \hat\varphi$, is $\psi\Rightarrow\varphi$ provable?

(For example, a positive answer to the question would let us say “there is no natural transformation from $\mathop{\mathrm{Hom}}(\mathop{\mathrm{Hom}}(A,B),A)$ to $A$ because Peirce's law $((A\Rightarrow B)\Rightarrow A)\Rightarrow A$ is not provable intuitionistically”.)

I would be surprised if this isn't a well-known construction in categorical logic, but I don't know the terminology well enough to search for it.

Note that I'm asking the question with finite sets because I thought it would be better behaved, but if you wish to remove “finite” throughout, be my guest.