9
$\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$
  • 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$ – Derek Elkins left SE Apr 22 '17 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 Apr 22 '17 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$ – Derek Elkins left SE Apr 22 '17 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 Apr 22 '17 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$ – Derek Elkins left SE Apr 22 '17 at 1:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.