<p>The surjective pairing rule is really just as written there by Wadler. Andrej's interpretation is correct. What the equation <code>h t = case t of { (X, y) -&gt; h (X, y) }</code> buys you is that on the left, <code>h</code> is applied to a variable, whereas on the right, <code>h</code> is applied to a constructor. That lets you lift any property you can prove about <code>h</code> on terms that are constructed using the constructor to a property on any input <code>t</code>, which is precisely what you want out of a property called &quot;surjectivity of constructor&quot;.</p>
<pre><code>t = case t of { (X, y) -&gt; (X, y) }                             -- by surjective pairing (h = id)
  = case t of { (X, (k, x)) -&gt; (X, (k, x)) }                   -- by surjective pairing for products
  = case t of { (X, (k, x)) -&gt; unfold X k x }                  -- by definition of unfold
  = case t of { (X, (k, x)) -&gt; unfold T out (unfold X k x) }   -- by unfold X k x = unfold T out (unfold X k x)
  = case t of { (X, (k, x)) -&gt; unfold T out (X, (k, x)) }      -- by definition of unfold
  = unfold T out t                                             -- by surjective pairing (h = unfold T out)
</code></pre>

CC BY-SA 4.0
2024-06-04T06:40:35.523Z
Thank you, I will have to go through this in more detail. For now I have two questions: 1) What is the type of `h`, and how can it be that the same `h` is applied on the left to a variable `t` of type `∃X. P X`, but on the right the same `h` is applied to a pair `(X, y)`? 2) To "lift any property on constructed terms to a property on any input" seems the same to me as to introduce `∃-intro` as Andrej did and then say that any `t : ∃X. P X` must be of the form `t = ∃-intro X y` for some `X : *` and `y : P X`. Or, the same as to say that `unfold` is surjective. How can we prove that in System F?
winitzki
CC BY-SA 4.0
2024-06-04T07:13:10.163Z
1) `h : E P -> R` for some `R`. 2) You can't. You can imagine a model where every value is tagged with 0 or 1, and the semantics of terms are tagged with 0. Thus constructors are not surjective since they can't construct 1-tagged values, and yet the tag is unobservable, which allows equations like surjective pairing as an approximation of surjectivity.
Li-yao Xia
CC BY-SA 4.0
2024-06-04T08:11:38.257Z
1) If `h : E P -> R` then `h` cannot be applied to the pair `(X, y)`, and `h` can only be applied to opaque values of type `E P`. What am I missing here? 2) Wadler says that the "surjective pairing rule" follows in parametric models. Can it be proved then?
winitzki
CC BY-SA 4.0
2024-06-04T08:22:31.340Z
@winitzki: What is the type of `(X, y)`? If its type is the same as the domain of `h`, then `h (X, y)` is valid by the typing rule for application. The typing rules do not have any side conditions or extra premisess requiring one to check "opaqueness".
Andrej Bauer
CC BY-SA 4.0
2024-06-04T09:03:07.733Z
@AndrejBauer Apparently, Wadler's notation `(X, y)` is too confusing to me and hinders my reasoning about those terms. Your notation (`∃-intro X y`) is clearer, as it shows that we are actually using a constructor to build a value of type `E P`. But to make things actually quite clear, I'd like to encode Wadler's notation in System F. Then $E~P=\forall R.~(\forall X.~P~X\to R)\to R$, Wadler's constructor `(X, y)` becomes $\Lambda R.~\lambda(k:\forall A.~P~A\to R).~k~X~y$, and Wadler's eliminator `(case t of {(X,y) -> w}) : W` becomes $t~W~(\Lambda X.~\lambda(y:P~X).~w)$. Is that right?
winitzki
CC BY-SA 4.0
2024-06-04T09:05:42.267Z
You're changing the subject. May we first resolve the question as to whether `h (X, y)` is valid? Do you see that it is (modulo confusing notation)?
Andrej Bauer
CC BY-SA 4.0
2024-06-04T09:18:42.133Z
@AndrejBauer  I'd love to resolve that question. But for me, the resolution using the notation `h (X, y)` proved to be very difficult despite prolonged effort. That's why I'm hoping to get more clarity by encoding everything in System F. Let me think about this. Right now, I see one source of confusion: The notation `case t of {(X, y) -> w}` uses `(X, y)` in a different way than the notation `(X, y)`. Perhaps, Wadler should have written `case t of { X -> y -> w }` instead?
winitzki
CC BY-SA 4.0
2024-06-04T09:28:27.707Z
And changing the notation to `∃-intro X y` doesn't help? To my mind you're blocked by a rather trivial notational quirk.
Andrej Bauer
CC BY-SA 4.0
2024-06-04T09:39:44.467Z
@AndrejBauer 1) Yes, I feel that I am unable to use Wadler's "surjective rule" in a proof because I don't understand the notation of that rule. That rule should have allowed me to replace something by something else in a proof, but I do not see what I am now allowed to replace by what. 2) Consider your notation, `case t of {∃-intro X y -> h (∃-intro X y)}`. Is it not true that `X` and `y` are bound variables inside the curly braces? Would it not be clearer to write them as such, for example: `case t of {`$\Lambda X.~\lambda (y: P~X).$`h (∃-intro X y)}`?
winitzki
CC BY-SA 4.0
2024-06-04T09:49:31.417Z
Actually, translating to System F helped a lot. In System F, after the translation I showed in a previous comment, I can prove the "surjectivity rule" by using the properties established in https://cstheory.stackexchange.com/questions/54124 Translating back into Wadler's notation, I can see that `case t of {Λ. y. h (∃-intro X y) } = h t`. Thank you for help!
winitzki
CC BY-SA 4.0
2024-06-04T11:50:32.033Z
Ok! Regarding notation, you may want to familiarize yourself with the syntax of `match` and `case` statements in OCaml, Haskell, Coq, Agda and Lean.
Andrej Bauer
CC BY-SA 4.0
2024-06-03T22:56:03.947Z
2024-06-04T13:37:27.177Z
2024-06-04T13:37:27.177Z
Li-yao Xia
<p>Is this not just confusion about notation? If the notation <code>(X, y)</code> is used to signify the introduction rule for <code>∃</code> then it <em>does</em> make sense to apply <code>h</code> to a pair <code>(X, y)</code> because it is not really a pair in the sense of simple binary product.</p>
<p>In other words, suppose we write something like <code>∃-intro X y</code> as the proof term for the introduction rule of exists, i.e.,</p>
<pre><code>∃-intro : (X : Type) → {P : X → Type} → (y : P X) → ∃ X . P X
</code></pre>
<p>then the surjective pairing rule becomes</p>
<pre><code>case t of {∃-intro X y -&gt; h (∃-intro X y)}  =  h t
</code></pre>
<p>where <code>h : (∃ X . P X) → Y</code> and <code>t : ∃ X . P X</code>. As far as I can tell the application of <code>h</code> is well-typed on both sides.</p>

CC BY-SA 4.0
2024-06-03T13:24:06.013Z
As far as I understand, the notation `case t of {(X, x) -> h X x}` is supposed to unpack the existential type into its parts. Under `case`, we may use the type `X` and the value `x`. In my view, by `h (X , x)`  means a function `h` with a type parameter `X` and a value parameter `x : P X`. But your interpretation essentially says `case t of { Foo -> h Foo } = h Foo` where `Foo : `$\exists X.~P~X$ and I don't see what this notation brings us. This is not an eliminator for `Foo`, as it does not destructure `Foo`. I don't think Wadler meant that. But what did he mean? How to use this equation?
winitzki
CC BY-SA 4.0
2024-06-03T13:31:03.537Z
In your notation `∃-intro X y` is an introduction rule. In the scope where we write `∃-intro X y`, we are also allowed to see `X` and `y`. Then I would transform your syntax into `case t of {∃-intro X y -> h' X y}  =  h (∃-intro X y)`. And it just looks like a trivial rewriting of `h (∃-intro X y)` into `h' X y` where the difference between `h` and `h'` is purely syntactical. How can we make progress with the proof, using that? Are we going to assume that all values of type `∃ X . P X` are always of the form `∃-intro X y` for some `X` and `y`?
winitzki
CC BY-SA 4.0
2024-06-03T15:57:17.010Z
I see your dilemma now, thanks for explaining.
Andrej Bauer
CC BY-SA 4.0
2024-06-03T11:56:43.747Z
2024-06-03T12:23:58.983Z
2024-06-03T12:23:58.983Z
Andrej Bauer
<p>Following <a href="https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt" rel="nofollow noreferrer">Wadler's paper &quot;Recursive types for free&quot;</a> and having spent some months on reconstructing the proof that <span class="math-container">$\exists A. ~ A \times (A\to F~ A)$</span> is the terminal <span class="math-container">$F$</span>-coalgebra, I am still not able to prove one step that appears to be important.</p>
<p>Wadler denotes <span class="math-container">$\exists A. ~ A \times (A\to F~ A)$</span> by <code>T</code> and defines the functions:</p>
<pre><code>unfold  :  forall X. (X -&gt; F X) -&gt; X -&gt; T
unfold  =  \(X : *) -&gt; \(k : X -&gt; F X) -&gt; \(x : T) -&gt; (X, (k,x))

out     :  T -&gt; F T
out     =  \(t : T) -&gt; case t of { (X,(k,x)) -&gt; F (unfold X k) (k x) }

in      :  F T -&gt; T
in      =  unfold (F T) (F out)
</code></pre>
<p>In Wadler's notation, the tuple <code>(X, x)</code> is a packed form of the existentially-typed value built from a specific type <code>X</code> and a value <code>x : P X</code> for some type constructor <code>P</code>.</p>
<p>The main question is to prove that <code>out</code> and <code>in</code> are inverses. Equivalently, to prove that any <span class="math-container">$F$</span>-coalgebra has a unique map to <code>T</code>.</p>
<p>Wadler does not actually show a detailed proof but mentions that the proof requires the parametricity assumption for <code>unfold</code>:</p>
<pre><code>          k                               unfold X k     
   X ----------&gt; F X                   X -----------&gt; T
   |              |                    |              |
   |              |                    |              |
 h |              | F h   implies    h |              | id
   |              |                    |              |
   |              |                    |              |
   X' ---------&gt; F X'                  X' ----------&gt; T
          k'                             unfold X' k'
</code></pre>
<p>The precondition is that <code>h</code> is an F-coalgebra morphism between F-coalgebras <code>X</code> and <code>X'</code>.</p>
<p>This can be written as the relational property that, for any types <span class="math-container">$X$</span>, <span class="math-container">$X'$</span>, for any functions <span class="math-container">$h : X\to X'$</span>, <span class="math-container">$k : X\to F~X$</span>, <span class="math-container">$k' : X'\to F~X'$</span>, such that <span class="math-container">$F(h) \circ k = k'\circ h$</span> we will then have <span class="math-container">$\mathrm{unfold}~X~k = \mathrm{unfold}~X'~k' \circ h$</span>. Indeed, this is a consequence of the &quot;free theorem&quot; (i.e., the relational naturality law) for the type signature of <code>unfold</code>.</p>
<p>I have applied this assumption, and I tried applying various other &quot;free theorems&quot;, but I still cannot derive <span class="math-container">$\mathrm{in} \circ \mathrm{out} = \mathrm{id}$</span>. I can only derive a weaker property: <span class="math-container">$$\mathrm{in} \circ \mathrm{out} = \mathrm{unfold} ~T~\mathrm{out}$$</span></p>
<p>So, it remains to prove that <span class="math-container">$\mathrm{unfold} ~T~\mathrm{out} = \mathrm{id}$</span> but I don't see how this can be proved from parametricity assumptions.</p>
<p>In other words, what I am missing is to prove that, for any value <code>t : T</code>,
<span class="math-container">$$ \mathrm{unfold} ~T~\mathrm{out}~t =t$$</span></p>
<p>I also tried to encode the existential type in System F. For instance, we then get:</p>
<pre><code> T = forall R. (forall X. (X -&gt; F X) -&gt; X -&gt; R) -&gt; R
</code></pre>
<p>I applied relational parametricity to derive the free theorem for <code>T</code>, but that did not seem to help. I can show that the function <span class="math-container">$\mathrm{unfold} ~T~\mathrm{out}$</span> of type <span class="math-container">$T\to T$</span> is idempotent, but  I cannot show that it is an identity function.</p>
<p>However, I can make progress with a weaker assumption: that any value of type <code>T</code> is a result of <code>unfold</code> applied to <em>some</em> arguments (not necessarily to <code>T</code> and <code>out</code>). In other words, it appears to be necessary to assume that <code>unfold</code> is surjective. But it is not clear how to prove that. (A related question is <a href="https://cstheory.stackexchange.com/questions/54364">Is the encoding of existential types in System F adequate?</a> .)</p>
<p>If we assume that any value of type <code>T</code> is obtained as <code>unfold R c r</code> with some type <code>R</code> and some <code>c : R -&gt; F R</code>, <code>r : R</code> then we can apply the &quot;free theorem&quot; of <code>unfold</code> with types <code>X = R</code> and <code>X' = T</code>, with functions <code>h = unfold R c</code>, <code>k = c</code>, <code>k' = out</code>, and obtain (having already shown that <code>unfold R c</code> is an F-coalgebra morphism):</p>
<pre><code> unfold R c r = unfold T out (unfold R c r)
</code></pre>
<p>If we denote <code>t = unfold R c r</code> then we obtain the desired equation <code>t = unfold T out t</code>.</p>
<p>But this equation holds only for <code>t : T</code> that are obtained by applying <code>unfold</code> to some arguments (<code>t = unfold R c r</code>). The equation <code>t = unfold T out t</code> does not follow for arbitrary <code>t : T</code> withough the assumption that any value of type <code>T</code> is obtained as <code>unfold R c r</code> with some <code>R</code>, <code>c</code>, <code>r</code>.</p>
<p>So, the question is, how to prove <code>t = unfold T out t</code> for arbitrary <code>t : T</code>, or how to prove that an arbitrary <code>t : T</code> can be expressed as <code>unfold R c r</code>. (Can we prove that in System F with the encoding of <code>T</code> as shown above, and using parametricity?)</p>
<p>With that, I can complete the proof that <code>in</code> and <code>out</code> are inverses, and that <code>T</code> is a terminal <span class="math-container">$F$</span>-coalgebra.</p>
<p>Am I missing something? Wadler also cryptically says that another necessary assumption is &quot;the surjective pairing rule&quot; that he writes as:</p>
<pre><code>case t of {(X,y) -&gt; h (X,y)}  =  h t
</code></pre>
<p>This is perhaps related to my missing assumption that <code>unfold</code> is surjective. However, I cannot make sense of Wadler's notation as written in this equation. The function <code>h</code> seems to be used in a contradictory way. In the left-hand side, the type of <code>h</code>'s argument is  the type of a pair <code>(X, y)</code> - a (dependent) pair consisting of a type and a value. In the right-hand side, the type of <code>h</code>'s argument is the existential type that does not expose its encapsulated type or value. It is not the type of a pair.</p>
<p>The function <code>h</code> does not seem to be possible to typecheck if encoded in System F. The existential type is encoded as a function, not as a pair.</p>
<p>What is the missing step or a missing assumption here?</p>

<functional-programming><typed-lambda-calculus><recursion><parametricity><inductive-type>
How to prove that $\exists A. ~ A \times (A\to F~ A)$ encodes the greatest fixpoint of $F$?
winitzki
# How to prove that $\exists A. ~ A \times (A\to F~ A)$ encodes the greatest fixpoint of $F$?

(Asked by: username_0 on 2024-06-03)

Following [Wadler's paper "Recursive types for free"](https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt) and having spent some months on reconstructing the proof that $\exists A. ~ A \times (A\to F~ A)$ is the terminal $F$-coalgebra, I am still not able to prove one step that appears to be important.

Wadler denotes $\exists A. ~ A \times (A\to F~ A)$ by `T` and defines the functions:

```
unfold  :  forall X. (X -> F X) -> X -> T
unfold  =  \(X : *) -> \(k : X -> F X) -> \(x : T) -> (X, (k,x))

out     :  T -> F T
out     =  \(t : T) -> case t of { (X,(k,x)) -> F (unfold X k) (k x) }

in      :  F T -> T
in      =  unfold (F T) (F out)

```

In Wadler's notation, the tuple `(X, x)` is a packed form of the existentially-typed value built from a specific type `X` and a value `x : P X` for some type constructor `P`.

The main question is to prove that `out` and `in` are inverses. Equivalently, to prove that any $F$-coalgebra has a unique map to `T`.

Wadler does not actually show a detailed proof but mentions that the proof requires the parametricity assumption for `unfold`:

```
          k                               unfold X k     
   X ----------> F X                   X -----------> T
   |              |                    |              |
   |              |                    |              |
 h |              | F h   implies    h |              | id
   |              |                    |              |
   |              |                    |              |
   X' ---------> F X'                  X' ----------> T
          k'                             unfold X' k'

```

The precondition is that `h` is an F-coalgebra morphism between F-coalgebras `X` and `X'`.

This can be written as the relational property that, for any types $X$, $X'$, for any functions $h : X\to X'$, $k : X\to F~X$, $k' : X'\to F~X'$, such that $F(h) \circ k = k'\circ h$ we will then have $\mathrm{unfold}~X~k = \mathrm{unfold}~X'~k' \circ h$. Indeed, this is a consequence of the "free theorem" (i.e., the relational naturality law) for the type signature of `unfold`.

I have applied this assumption, and I tried applying various other "free theorems", but I still cannot derive $\mathrm{in} \circ \mathrm{out} = \mathrm{id}$. I can only derive a weaker property: $$\mathrm{in} \circ \mathrm{out} = \mathrm{unfold} ~T~\mathrm{out}$$

So, it remains to prove that $\mathrm{unfold} ~T~\mathrm{out} = \mathrm{id}$ but I don't see how this can be proved from parametricity assumptions.

In other words, what I am missing is to prove that, for any value `t : T`,
$$ \mathrm{unfold} ~T~\mathrm{out}~t =t$$

I also tried to encode the existential type in System F. For instance, we then get:

```
 T = forall R. (forall X. (X -> F X) -> X -> R) -> R

```

I applied relational parametricity to derive the free theorem for `T`, but that did not seem to help. I can show that the function $\mathrm{unfold} ~T~\mathrm{out}$ of type $T\to T$ is idempotent, but I cannot show that it is an identity function.

However, I can make progress with a weaker assumption: that any value of type `T` is a result of `unfold` applied to *some* arguments (not necessarily to `T` and `out`). In other words, it appears to be necessary to assume that `unfold` is surjective. But it is not clear how to prove that. (A related question is [Is the encoding of existential types in System F adequate?](https://cstheory.stackexchange.com/questions/54364) .)

If we assume that any value of type `T` is obtained as `unfold R c r` with some type `R` and some `c : R -> F R`, `r : R` then we can apply the "free theorem" of `unfold` with types `X = R` and `X' = T`, with functions `h = unfold R c`, `k = c`, `k' = out`, and obtain (having already shown that `unfold R c` is an F-coalgebra morphism):

```
 unfold R c r = unfold T out (unfold R c r)

```

If we denote `t = unfold R c r` then we obtain the desired equation `t = unfold T out t`.

But this equation holds only for `t : T` that are obtained by applying `unfold` to some arguments (`t = unfold R c r`). The equation `t = unfold T out t` does not follow for arbitrary `t : T` withough the assumption that any value of type `T` is obtained as `unfold R c r` with some `R`, `c`, `r`.

So, the question is, how to prove `t = unfold T out t` for arbitrary `t : T`, or how to prove that an arbitrary `t : T` can be expressed as `unfold R c r`. (Can we prove that in System F with the encoding of `T` as shown above, and using parametricity?)

With that, I can complete the proof that `in` and `out` are inverses, and that `T` is a terminal $F$-coalgebra.

Am I missing something? Wadler also cryptically says that another necessary assumption is "the surjective pairing rule" that he writes as:

```
case t of {(X,y) -> h (X,y)}  =  h t

```

This is perhaps related to my missing assumption that `unfold` is surjective. However, I cannot make sense of Wadler's notation as written in this equation. The function `h` seems to be used in a contradictory way. In the left-hand side, the type of `h`'s argument is the type of a pair `(X, y)` - a (dependent) pair consisting of a type and a value. In the right-hand side, the type of `h`'s argument is the existential type that does not expose its encapsulated type or value. It is not the type of a pair.

The function `h` does not seem to be possible to typecheck if encoded in System F. The existential type is encoded as a function, not as a pair.

What is the missing step or a missing assumption here?

**Tags:** functional-programming, typed-lambda-calculus, recursion, parametricity, inductive-type


---

## 2 answers

### Answer by username_1 on 2024-06-03. Score: 3 | Accepted answer

The surjective pairing rule is really just as written there by Wadler. username_2's interpretation is correct. What the equation `h t = case t of { (X, y) -> h (X, y) }` buys you is that on the left, `h` is applied to a variable, whereas on the right, `h` is applied to a constructor. That lets you lift any property you can prove about `h` on terms that are constructed using the constructor to a property on any input `t`, which is precisely what you want out of a property called "surjectivity of constructor".

```
t = case t of { (X, y) -> (X, y) }                             -- by surjective pairing (h = id)
  = case t of { (X, (k, x)) -> (X, (k, x)) }                   -- by surjective pairing for products
  = case t of { (X, (k, x)) -> unfold X k x }                  -- by definition of unfold
  = case t of { (X, (k, x)) -> unfold T out (unfold X k x) }   -- by unfold X k x = unfold T out (unfold X k x)
  = case t of { (X, (k, x)) -> unfold T out (X, (k, x)) }      -- by definition of unfold
  = unfold T out t                                             -- by surjective pairing (h = unfold T out)

```

> **Comments:**
> **username_0**: Thank you, I will have to go through this in more detail. For now I have two questions: 1) What is the type of `h`, and how can it be that the same `h` is applied on the left to a variable `t` of type `∃X. P X`, but on the right the same `h` is applied to a pair `(X, y)`? 2) To "lift any property on constructed terms to a property on any input" seems the same to me as to introduce `∃-intro` as username_2 did and then say that any `t : ∃X. P X` must be of the form `t = ∃-intro X y` for some `X : *` and `y : P X`. Or, the same as to say that `unfold` is surjective. How can we prove that in System F?  
> **username_1**: 1) `h : E P -> R` for some `R`. 2) You can't. You can imagine a model where every value is tagged with 0 or 1, and the semantics of terms are tagged with 0. Thus constructors are not surjective since they can't construct 1-tagged values, and yet the tag is unobservable, which allows equations like surjective pairing as an approximation of surjectivity.  
> **username_0**: 1) If `h : E P -> R` then `h` cannot be applied to the pair `(X, y)`, and `h` can only be applied to opaque values of type `E P`. What am I missing here? 2) Wadler says that the "surjective pairing rule" follows in parametric models. Can it be proved then?  
> **username_2**: @username_0: What is the type of `(X, y)`? If its type is the same as the domain of `h`, then `h (X, y)` is valid by the typing rule for application. The typing rules do not have any side conditions or extra premisess requiring one to check "opaqueness".  
> **username_0**: @username_2 Apparently, Wadler's notation `(X, y)` is too confusing to me and hinders my reasoning about those terms. Your notation (`∃-intro X y`) is clearer, as it shows that we are actually using a constructor to build a value of type `E P`. But to make things actually quite clear, I'd like to encode Wadler's notation in System F. Then $E~P=\forall R.~(\forall X.~P~X\to R)\to R$, Wadler's constructor `(X, y)` becomes $\Lambda R.~\lambda(k:\forall A.~P~A\to R).~k~X~y$, and Wadler's eliminator `(case t of {(X,y) -> w}) : W` becomes $t~W~(\Lambda X.~\lambda(y:P~X).~w)$. Is that right?  
> **username_2**: You're changing the subject. May we first resolve the question as to whether `h (X, y)` is valid? Do you see that it is (modulo confusing notation)?  
> **username_0**: @username_2  I'd love to resolve that question. But for me, the resolution using the notation `h (X, y)` proved to be very difficult despite prolonged effort. That's why I'm hoping to get more clarity by encoding everything in System F. Let me think about this. Right now, I see one source of confusion: The notation `case t of {(X, y) -> w}` uses `(X, y)` in a different way than the notation `(X, y)`. Perhaps, Wadler should have written `case t of { X -> y -> w }` instead?  
> **username_2**: And changing the notation to `∃-intro X y` doesn't help? To my mind you're blocked by a rather trivial notational quirk.  
> **username_0**: @username_2 1) Yes, I feel that I am unable to use Wadler's "surjective rule" in a proof because I don't understand the notation of that rule. That rule should have allowed me to replace something by something else in a proof, but I do not see what I am now allowed to replace by what. 2) Consider your notation, `case t of {∃-intro X y -> h (∃-intro X y)}`. Is it not true that `X` and `y` are bound variables inside the curly braces? Would it not be clearer to write them as such, for example: `case t of {`$\Lambda X.~\lambda (y: P~X).$`h (∃-intro X y)}`?  
> **username_0**: Actually, translating to System F helped a lot. In System F, after the translation I showed in a previous comment, I can prove the "surjectivity rule" by using the properties established in https://cstheory.stackexchange.com/questions/54124 Translating back into Wadler's notation, I can see that `case t of {Λ. y. h (∃-intro X y) } = h t`. Thank you for help!  
> **username_2**: Ok! Regarding notation, you may want to familiarize yourself with the syntax of `match` and `case` statements in OCaml, Haskell, Coq, Agda and Lean.  

---

### Answer by username_2 on 2024-06-03. Score: 1

Is this not just confusion about notation? If the notation `(X, y)` is used to signify the introduction rule for `∃` then it *does* make sense to apply `h` to a pair `(X, y)` because it is not really a pair in the sense of simple binary product.

In other words, suppose we write something like `∃-intro X y` as the proof term for the introduction rule of exists, i.e.,

```
∃-intro : (X : Type) → {P : X → Type} → (y : P X) → ∃ X . P X

```

then the surjective pairing rule becomes

```
case t of {∃-intro X y -> h (∃-intro X y)}  =  h t

```

where `h : (∃ X . P X) → Y` and `t : ∃ X . P X`. As far as I can tell the application of `h` is well-typed on both sides.

> **Comments:**
> **username_0**: As far as I understand, the notation `case t of {(X, x) -> h X x}` is supposed to unpack the existential type into its parts. Under `case`, we may use the type `X` and the value `x`. In my view, by `h (X , x)`  means a function `h` with a type parameter `X` and a value parameter `x : P X`. But your interpretation essentially says `case t of { Foo -> h Foo } = h Foo` where `Foo : `$\exists X.~P~X$ and I don't see what this notation brings us. This is not an eliminator for `Foo`, as it does not destructure `Foo`. I don't think Wadler meant that. But what did he mean? How to use this equation?  
> **username_0**: In your notation `∃-intro X y` is an introduction rule. In the scope where we write `∃-intro X y`, we are also allowed to see `X` and `y`. Then I would transform your syntax into `case t of {∃-intro X y -> h' X y}  =  h (∃-intro X y)`. And it just looks like a trivial rewriting of `h (∃-intro X y)` into `h' X y` where the difference between `h` and `h'` is purely syntactical. How can we make progress with the proof, using that? Are we going to assume that all values of type `∃ X . P X` are always of the form `∃-intro X y` for some `X` and `y`?  
> **username_2**: I see your dilemma now, thanks for explaining.  

---

