<p>The Curry-Howard correspondence is typically used in <em>constructive type theory</em>, i.e. where you don't have double negation elimination. This means that the identity you list doesn't actually hold in type theory without assuming additional axioms.</p>
<p>So you could assume double negation elimination and have <span class="math-container">$\Sigma (x:S).T$</span> be <span class="math-container">$\lnot \Pi(x:S) . \lnot T$</span>. But this is pretty useless from a computational point of view since you'll get &quot;stuck&quot; trying to evaluate with the double negation.</p>
<p>However, with Impredicative polymorphism, there is a way to encode Sigma using Pi, namely its Church encoding.</p>
<p>The encoding is given here: <a href="https://math.stackexchange.com/questions/661511/is-it-possible-to-express-sigma-type-in-martin-l%c3%b6f-type-theory-with-other-constr/673003#673003">https://math.stackexchange.com/questions/661511/is-it-possible-to-express-sigma-type-in-martin-l%c3%b6f-type-theory-with-other-constr/673003#673003</a></p>
<p>You don't strictly need Impredicative polymorphism, but without it Sigma lives at a higher level than Pi which is odd.</p>

CC BY-SA 4.0
2024-06-01T13:54:31.477Z
I see so it instead of using $\bot$ it is using forall types in a certain universe: $$\sum(x:A)B(x) \cong \prod(C:\mathbb{U})\left(\left(\prod(x:A)(B(x)\rightarrow C)\right)\rightarrow C\right)$$ I'm not sure I get why that is true but is is certainly intersting.
zooby
CC BY-SA 4.0
2024-06-01T16:24:13.843Z
Does it rely on the fact that $\forall_y:f(x)\rightarrow y$ must be false since a proposition can't imply all statements. Then we must prove somewhere that at least one statement in $\mathbb{U}$ is false?
zooby
CC BY-SA 4.0
2024-06-01T16:58:46.967Z
It's unclear what you mean by any of this.
Naïm Favier
CC BY-SA 4.0
2024-06-01T23:05:07.617Z
@zooby what is the type of $f$ and $y$ you're talking about?
Joey Eremondi
CC BY-SA 4.0
2024-06-01T07:09:17.243Z
2024-06-01T07:09:17.243Z
Joey Eremondi
<p>Using the <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="nofollow noreferrer">Curry-Howard Correspondence</a> and the fact we can write:
<span class="math-container">$$\forall x: f(x) \equiv \not \exists x: \lnot f(x)$$</span></p>
<p>Can we write the <span class="math-container">$\sum$</span> type in terms of the <span class="math-container">$\prod$</span> type?</p>
<p><span class="math-container">$$\sum(x:A)B(x) \overset ?\cong \left(\prod(x:A)(B(x)\rightarrow \bot )\right)\rightarrow\bot $$</span></p>
<p>In particular does this mean we can encode a pair <span class="math-container">$(a,b):A\times B$</span> as:</p>
<p><span class="math-container">$$(a,b):A\times B \overset ?\cong (a\Rightarrow(b \Rightarrow\bot))\Rightarrow \bot: (A\rightarrow (B\rightarrow \bot))\rightarrow \bot $$</span></p>
<p>(Where we are using the <span class="math-container">$\Rightarrow$</span> symbol instead of lambda syntax for functions).</p>
<p><strong>Speculation</strong></p>
<p>Further considering the sheffer stroke <span class="math-container">$a\uparrow b \equiv (a\implies (b\implies F))$</span> which all logic can be built from. This suggests there should be some dependent operator <span class="math-container">$a\uparrow b:\overline{\bigwedge}(x:A)B(x)$</span> from which all others can be built. (Note that it wouldn't help with readability!!). Functions and pairs should all be made out of this single operator:</p>
<p><span class="math-container">$$(a,b) \cong (a \uparrow b) \uparrow (a \uparrow b) : (A \overline{\land} B)\overline{\land}  (A \overline{\land} B)$$</span>
<span class="math-container">$$a\rightarrow b \cong a \uparrow (a\uparrow b) : A\overline{\land}  (A \overline{\land} B)$$</span></p>
<p>But the rule for function composition would be very strange since it has a very strange type.</p>
<p><strong>Question</strong></p>
<p>Is all I have said true or am I pushing the Curry-Howard Correspondence too far?</p>

<dependent-type>
Can the Sigma type be defined in terms of the pi type in dependent type theory?
zooby
# Can the Sigma type be defined in terms of the pi type in dependent type theory?

(Asked by: username_0 on 2024-05-31)

Using the [Curry-Howard Correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) and the fact we can write:
$$\forall x: f(x) \equiv \not \exists x: \lnot f(x)$$

Can we write the $\sum$ type in terms of the $\prod$ type?

$$\sum(x:A)B(x) \overset ?\cong \left(\prod(x:A)(B(x)\rightarrow \bot )\right)\rightarrow\bot $$

In particular does this mean we can encode a pair $(a,b):A\times B$ as:

$$(a,b):A\times B \overset ?\cong (a\Rightarrow(b \Rightarrow\bot))\Rightarrow \bot: (A\rightarrow (B\rightarrow \bot))\rightarrow \bot $$

(Where we are using the $\Rightarrow$ symbol instead of lambda syntax for functions).

**Speculation**

Further considering the sheffer stroke $a\uparrow b \equiv (a\implies (b\implies F))$ which all logic can be built from. This suggests there should be some dependent operator $a\uparrow b:\overline{\bigwedge}(x:A)B(x)$ from which all others can be built. (Note that it wouldn't help with readability!!). Functions and pairs should all be made out of this single operator:

$$(a,b) \cong (a \uparrow b) \uparrow (a \uparrow b) : (A \overline{\land} B)\overline{\land} (A \overline{\land} B)$$
$$a\rightarrow b \cong a \uparrow (a\uparrow b) : A\overline{\land} (A \overline{\land} B)$$

But the rule for function composition would be very strange since it has a very strange type.

**Question**

Is all I have said true or am I pushing the Curry-Howard Correspondence too far?

**Tags:** dependent-type


---

## 1 answers

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

The Curry-Howard correspondence is typically used in *constructive type theory*, i.e. where you don't have double negation elimination. This means that the identity you list doesn't actually hold in type theory without assuming additional axioms.

So you could assume double negation elimination and have $\Sigma (x:S).T$ be $\lnot \Pi(x:S) . \lnot T$. But this is pretty useless from a computational point of view since you'll get "stuck" trying to evaluate with the double negation.

However, with Impredicative polymorphism, there is a way to encode Sigma using Pi, namely its Church encoding.

The encoding is given here: <https://math.stackexchange.com/questions/661511/is-it-possible-to-express-sigma-type-in-martin-l%c3%b6f-type-theory-with-other-constr/673003#673003>

You don't strictly need Impredicative polymorphism, but without it Sigma lives at a higher level than Pi which is odd.

> **Comments:**
> **username_0**: I see so it instead of using $\bot$ it is using forall types in a certain universe: $$\sum(x:A)B(x) \cong \prod(C:\mathbb{U})\left(\left(\prod(x:A)(B(x)\rightarrow C)\right)\rightarrow C\right)$$ I'm not sure I get why that is true but is is certainly intersting.  
> **username_0**: Does it rely on the fact that $\forall_y:f(x)\rightarrow y$ must be false since a proposition can't imply all statements. Then we must prove somewhere that at least one statement in $\mathbb{U}$ is false?  
> **username_2**: It's unclear what you mean by any of this.  
> **username_1**: @username_0 what is the type of $f$ and $y$ you're talking about?  

---

