10
$\begingroup$

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.

$\endgroup$
5
  • 3
    $\begingroup$ 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$. $\endgroup$ Commented Apr 22, 2017 at 0:24
  • 1
    $\begingroup$ @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 (?) $\endgroup$
    – chi
    Commented Apr 22, 2017 at 0:35
  • 1
    $\begingroup$ 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. $\endgroup$ Commented Apr 22, 2017 at 0:47
  • 1
    $\begingroup$ @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. $\endgroup$
    – chi
    Commented Apr 22, 2017 at 0:59
  • 1
    $\begingroup$ 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. $\endgroup$ Commented Apr 22, 2017 at 1:57

1 Answer 1

0
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.