Using naturality to prove $f: \forall\alpha. \alpha\times\alpha\to\alpha$ must be a projection

Question

Suppose we have a System F term $f : \forall \alpha. \alpha\times\alpha\to\alpha$, interpreted in a parametric model which is a bicartesian closed category.

I was wondering if in such context it is possible to prove that (in the model) $f$ must be a projection (either $\pi_1$ or $\pi_2$), exploiting the naturality of $f$ and little else.

So far, I got the following sketch.

By naturality, for all $g: A\to B$, we have $$ (g \times g); f_B = f_A ; g$$ In particular, we can take $A = 2 = 1+1$ (the coproduct of the final object with itself), and take ${\sf tt},{\sf ff}: 1\to 2$ to be the inclusions.

We get that, for all $g: 1\to B$, we have $$ \langle {\sf tt}, {\sf ff} \rangle ; (g \times g); f_B = \langle {\sf tt}, {\sf ff} \rangle ; f_2 ; g$$ Now, we have a morphism $$ h = \langle {\sf tt}, {\sf ff} \rangle ; f_2 : 1 \to 2 $$ and we assume that (*) in the model $h$ must be one of $\sf tt,ff$ -- i.e., that no other morphisms exist.

W.l.o.g., assume $h=\sf tt$ (the other case being symmetrical). Then, we have $$ \langle {\sf tt};g , {\sf ff};g \rangle ; f_B = {\sf tt} ; g$$ and, taking $g = [m,n]$ for some $m,n : 1\to B$ $$ \langle m , n \rangle ; f_B = m$$ which is "close" to stating that $f_B$ is the first projection.

Questions:

1) Can we weaken the assumption ($*$) in some way? Or, can we strengthen ($*$) by requiring some standard property that "usually" holds in known models? I mean, I could work in a specific model (e.g. PERs) where we only have two inclusions $1\to 2$, but maybe there's some more general standard-ish assumption which can guarantee that?

2) Can we prove that $f_B$ is really a projection? Proving that it is such seems to require a sort of extensionality principle like

$$ (\forall x:1\to A. x;f=x;g) \implies f=g $$

but this, I guess, might not hold in general.

A final note: I'm aware that one can prove $f$ to be $\beta\eta$ equivalent to a projection through syntactic means (Krivine does so, if I remember correctly), but I am really interested in the consequences of naturality.

Answer 1

Naturality is sufficient.

An easy way is to use the Yoneda lemma, which gives the equivalence:

$$ a\times a\to a \equiv (\mathbb2 \to a ) \to a \equiv \mathbb2 $$ where $\mathbb2$ denotes the Boolean type and it is assumed that the arrow $a\times a\to a$ is a natural transformation.

We can adapt the proof of the Yoneda lemma to this case and find a simple proof from naturality:

Suppose $$p : \forall a.\,a \times a \to a$$ is a function implemented somehow in System F, and suppose $p$ obeys its naturality law. (That assumption will follow from parametricity, but that's not the question here.) Set the type parameter as $a = \mathbb2$ and apply $p$ to the specially chosen value $x : \mathbb 2 \times \mathbb 2$, namely, $x = (true, false)$. The value $p(x)$ is again of type $\mathbb2$ and so we must have $p(x)=y$ where the Boolean value $y$ is either $y=false$ or $y=true$.

Now, use the naturality law of $p$: For any types $a$, $b$, any values $m:a$, $n:a$, and any function $f: a\to b$ we must have: $$ p(f(m), f(n)) = f(p(m, n))$$ Choose $a=\mathbb2$, $m=true$, $n=false$, but keep the type $b$ arbitrary. Then the naturality law says: $$ p(f(true), f(false)) = f(p(true, false)) = f(y) $$

This naturality law constrains $p$ enough to force $p = \pi_1$ or $p = \pi_2$. This is because $f(true)$ and $f(false)$ are arbitrary values of type $b$. Denote them by $b_1 = f(true)$ and $b_2 = f(false)$. We know that $y$ is either true or false. Suppose $y=false$. Then we have found that for arbitrary values $b_1$, $b_2$ of type $b$: $$ p(b_1, b_2) = f(false)=b_2$$ Similarly, if $y=true$ then for arbitrary values $b_1$, $b_2$ of type $b$: $$ p(b_1, b_2) = f(true)=b_1$$

We have shown that either $p = \pi_1$ or $p = \pi_2$.