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

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.

• I suspect you'll need more than naturality. Consider $\mathbf{Set}^2\simeq\mathbf{Set}\times\mathbf{Set}$. It is a complete and cocomplete Boolean Grothendieck topos with NNO. It has natural transformations $\Delta\to Id$ beyond the projections, namely taking the inner or outer sets of each pair of sets. $X\times X$ being a pair of pairs of sets in $\mathbf{Set}^2$. Commented Apr 22, 2017 at 0:24
• @DerekElkins Ah, that's a good reasonably simple example (even if I'm not yet familiar with topoi), thanks. I also believe I need more than naturality, but perhaps not so much more. At the moment ($*$) plus extensionality is the best (in my very own opinion) sufficient criterion I could find. But maybe there's something even simpler or more standard (?)
– chi
Commented Apr 22, 2017 at 0:35
• Note that (famously) $\mathbf{Set}$ is not a model of System F. However, my point was that if you consider any class of categories that contains $\mathbf{Set}^2$, e.g. you consider, say, lextensive categories then the statement won't hold. Now there are properties that exclude $\mathbf{Set}^2$ and include $\mathbf{Set}$ (for which the statement does hold) such as being two-valued, and there are properties that exclude both such as being a model of System F, requiring all of parametricity. Commented Apr 22, 2017 at 0:47
• @DerekElkins Sure. The only parametric System F models I read about so far are PER-based models, so I was trying to generalize a bit fomr there. Even if $\bf Set$-derived categories necessarily fail in being models (as Reynolds proved), it is interesting to see what happens there.
– chi
Commented Apr 22, 2017 at 0:59
• Agreed. My previous comment was to avoid a possible confusion that I was presenting $\mathbf{Set}^2$ as a counter-model that demonstrates that the statement couldn't possibly be generally true (and explain what I was trying to accomplish with that example.) It sounds like you understand this completely. It may be useful context for others. Commented Apr 22, 2017 at 1:57

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$$.