<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" 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? .)
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. Andrej'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 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?  
> **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**: @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?  
> **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**: @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?  
> **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**: @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)}`?  
> **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.  

---

