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.
Using naturality to prove $f: \forall\alpha. \alpha\times\alpha\to\alpha$ must be a projection
programming languages;lambda calculus;category theory