funsplit and polarity of Pi-types In a recent thread on the Agda mailing list, the
question of $\eta$ laws popped up, in which Peter Hancock made thought-provoking remark. 

My understanding is that $\eta$ laws come with negative
types, ie. connectives which introduction rules are invertible. To disable $\eta$ for functions, Hank suggests using a custom-made eliminator, funsplit, instead of the usual application rule. I would like to understand Hank's remark in terms of polarities.

For example, there are two presentations $\Sigma$-types. There is the
traditional Martin-Löf split eliminator, in a positive style:

$$
\begin{array}{l}
\Gamma \vdash f : (a : A)(b : B\: a) \to C (a , b) \\
\Gamma \vdash p : \Sigma a : A. B \\
\hline \\
\Gamma \vdash \mathrm{split}\: f\: p : C\: p
\end{array}
$$

And there is the negative version:

$$
\begin{array}{l}
\Gamma \vdash p : \Sigma a : A. B \\
\hline \\
\Gamma \vdash \pi_0\: p : A
\end{array}
\qquad
\begin{array}{l}
\Gamma \vdash p : \Sigma a : A. B \\
\hline \\
\Gamma \vdash \pi_1\: p : B[\pi_0\: p / a]
\end{array}
$$

This latter presentation makes it easy to obtain $\eta$ for pairs,
ie. $(\pi_0 p , \pi_1 p) == p$ for any pair $p$ (where == stands for the definitional equality). In terms of provability, this difference does not matter: intuitionistically, you can implement projections with split, or the
other way around.

Now, $\Pi$-types are usually (and uncontroversially, I believe) taken negatively:

$$
\begin{array}{l}
\Gamma \vdash f : \Pi a : A. B \\
\Gamma \vdash s : A \\
\hline \\
\Gamma \vdash f s : B[s / a] 
\end{array}
$$

Which gives us $\eta$ for functions: $\lambda x. f x == f$.

However, in that mail, Hank recalls
the funsplit eliminator (Programming in ML type theory, [http://www.cse.chalmers.se/research/group/logic/book/], p.56). It is
described in the logical framework by:

$$
\begin{array}{l}
f \in \Pi(A, B) \\
C(v)\: Set [v \in \Pi(A, B)] \\
d(y) \in C(\lambda(y)) [y(x) \in B(x) [x \in A]] \\
\hline \\
\mathrm{funsplit}(f, d) \in C(f)
\end{array}
$$

Interestingly, Nordstrom et al. motivate this definition by saying that
"[this] alternative non-canonical form is based on the principle of
structural induction". There is a strong smell of positivity to this statement: functions would be 'defined' by their constructor, $\lambda$.

However, I cannot quite nail down a satisfactory presentation of that
rule in natural deduction (or, even better, sequent calculus). The
(ab)use of the logical framework to introduce $y$ seems crucial here.

So, is funsplit a positive presentation of $\Pi$-types? Do we also have something similar in the
(non dependent) sequent calculus? What would it look like? 

How common/curious is that for the proof theorists in the field?
Here's a slightly different perspective on Fredrik's answer. It's generally the case that impredicative Church encodings of types will satisfy the relevant $\beta$ laws, but will not satisfy the $\eta$ laws. 

So this means we can define a dependent pair as follows:

$$
\exists x:X.\;Y[x] \triangleq \forall \alpha:\ast.\; (\Pi x:X.\;Y[x] \to \alpha) \to \alpha
$$
Now, note that $\pi_1$ is easily definable:
$$
\pi_1 : \exists x:X.\;Y[x] \to X \triangleq \lambda p:(\exists x:X.\;Y[x]).\;p\;X\;(\lambda x\;y.x)
$$
However, you cannot define the second projection $\pi_2 : \Pi p:(\exists x:X.\;Y[x]).\; Y[\pi_1\;p]$ -- try it! You can only define a weak eliminator for it, which is why I wrote it with an existential. 

However, the second projection is realizable, and in a parametric model you can show that it has the right behavior, too. (See my recent draft with Derek Dreyer on parametricity in the Calculus of Constructions for more on this.) So I think that the $\pi_2$ projection fundamentally demands some strong extensionality properties for it to make sense. 

In terms of the sequent calculus, the weak eliminator has a rule that looks a bit like:

$$
\frac{\Gamma, x:X, y:Y[x],\; \Gamma' \vdash e' : C}
     {\Gamma, p:\exists x:X.\,Y[x],\; \Gamma' \vdash \mathsf{let}(x,y)=p\;\mathsf{in}\;e' : C}
$$
Here, the implicit well-formedness conditions imply that $p$ cannot occur free in $\Gamma'$ or $C$. If we relax that condition, we get the split rule, which has a left-rule that looks like
$$
\frac{\Gamma, x:X, y:Y[x],\; [(x,y)/p]\Gamma' \vdash e' : [(x,y)/p]C}
     {\Gamma, p:\exists x:X.\,Y[x],\; \Gamma' \vdash \mathsf{let}(x,y)=p\;\mathsf{in}\;e' : C}
$$
That substitution reminds me an awful lot of the Girard/Schroeder-Heister elimination rule for equality. I asked a question about this rule a while back, and David Baelde and Gopalan Nadathur give the state-of-the-art version in their LICS 2012 paper, Combining Deduction Modulo and Logics of Fixed-Point Definitions. I think Conor McBride has spent some time thinking about the relationship between the identity type and the Schroeder-Heister equality, so you might want to see what he thinks.