<p>Extensionality is basically the reversibility of the introduction rule. Negative types have reversible introduction rules, while positive types have reversible elimination rules. So you are looking in the wrong direction.</p>
<p>The nlab entry for sum types mentions polarity at the very end.</p>

CC BY-SA 4.0
2021-11-02T16:11:45.077Z
Can you expand on that? It sounds more like an eta-rule than extensionality to me, but I'm guessing there's a connection I'm not seeing. Is there a connection to equality reflection?
Joey Eremondi
CC BY-SA 4.0
2021-11-02T18:26:13.727Z
In the presence of $\beta$-rules and congruence rules, extensionality and $\eta$-rules are interderivable. For example if $x : A \vdash f x \equiv g x$ then $f \equiv (\lambda x . f x) \equiv (\lambda x . g x) \equiv g$, where we used the $\eta$-rule in the first and third step, and a congruence rule in the second step.
Andrej Bauer
CC BY-SA 4.0
2021-11-02T20:33:34.240Z
Is there a name for 'reversibility of elimination rules'?
ice1000
CC BY-SA 4.0
2021-11-03T00:01:23.833Z
@ice1000 Intuitionistic type theory is inherently biased towards positive types. I doubt there is a name for that.
Trebor
CC BY-SA 4.0
2021-11-03T16:44:00.567Z
@AndrejBauer Ahh, okay that makes sense. Is this related to how lots of type theories have eta-expansion, but not eta-contraction? Because eta-contraction implies extensionality?
Joey Eremondi
CC BY-SA 4.0
2021-11-03T17:03:04.280Z
@jmite No, η contraction is avoided because it conflicts with β reduction from a confluence standpoint. What is usually missing for extensional equality is a way to go from a point-wise identity _proof_ to the judgmental $x : A ⊢ f x \equiv g x$ so that congruence and η rules can apply. Equality reflection in extensional type theory allows this, but intensional type theory does not.
Dan Doel
CC BY-SA 4.0
2021-11-03T18:57:36.830Z
There is a family of equality checking algorithms that can deal with *judgemental* extensionality rules. See [An extensible equality checking algorithm for dependent type theories](https://arxiv.org/abs/2103.07397), and references therein for precursors on which the aglorithm is based. (Apologies for shameless self-promotion.)
Andrej Bauer
CC BY-SA 4.0
2021-11-02T15:23:33.363Z
2021-11-02T15:23:33.363Z
Trebor
<p>It is well-known in the literature that (internal) extensionality of a function type means <span class="math-container">$(\prod_a f~a=g~a)\implies f=g$</span> (where <span class="math-container">$=$</span> is the intensional equality type) and extensionality of a product type means <span class="math-container">$\sum_{p:a.1=b.1}\text{transport}~p~(a.2)=b.2 \implies a=b$</span>, but how is extensionality of positive types defined?</p>
<p>I can guess that for <span class="math-container">$a, b: X+Y$</span> two inhabitants of a sum-type, we might want to say that &quot;either (<span class="math-container">$a=inl(a'), b=inl(b')$</span> and <span class="math-container">$a'=b'$</span>) or (<span class="math-container">$a=inr(a'),b=inr(b')$</span> and <span class="math-container">$a'=b'$</span>) do <span class="math-container">$a=b$</span>&quot;, but it looks impossible, right? Because we do not have an operation for deciding whether <span class="math-container">$a=inl(a')$</span> or not, given that <span class="math-container">$a$</span> is open.</p>

<type-theory><extensionality>
What is the general definition of 'extensionality' in type theory and how is extensionality defined for positive types?
ice1000
# What is the general definition of 'extensionality' in type theory and how is extensionality defined for positive types?

(Asked by: username_0 on 2021-11-02)

It is well-known in the literature that (internal) extensionality of a function type means $(\prod\_a f~a=g~a)\implies f=g$ (where $=$ is the intensional equality type) and extensionality of a product type means $\sum\_{p:a.1=b.1}\text{transport}~p~(a.2)=b.2 \implies a=b$, but how is extensionality of positive types defined?

I can guess that for $a, b: X+Y$ two inhabitants of a sum-type, we might want to say that "either ($a=inl(a'), b=inl(b')$ and $a'=b'$) or ($a=inr(a'),b=inr(b')$ and $a'=b'$) do $a=b$", but it looks impossible, right? Because we do not have an operation for deciding whether $a=inl(a')$ or not, given that $a$ is open.

**Tags:** type-theory, extensionality

---

## 1 answers

### Answer by username_1 on 2021-11-02. Score: 6 | Accepted answer

Extensionality is basically the reversibility of the introduction rule. Negative types have reversible introduction rules, while positive types have reversible elimination rules. So you are looking in the wrong direction.

The nlab entry for sum types mentions polarity at the very end.

> **Comments:**
> **username_2**: Can you expand on that? It sounds more like an eta-rule than extensionality to me, but I'm guessing there's a connection I'm not seeing. Is there a connection to equality reflection?  
> **username_3**: In the presence of $\beta$-rules and congruence rules, extensionality and $\eta$-rules are interderivable. For example if $x : A \vdash f x \equiv g x$ then $f \equiv (\lambda x . f x) \equiv (\lambda x . g x) \equiv g$, where we used the $\eta$-rule in the first and third step, and a congruence rule in the second step.  
> **username_0**: Is there a name for 'reversibility of elimination rules'?  
> **username_1**: @ice1000 Intuitionistic type theory is inherently biased towards positive types. I doubt there is a name for that.  
> **username_2**: @AndrejBauer Ahh, okay that makes sense. Is this related to how lots of type theories have eta-expansion, but not eta-contraction? Because eta-contraction implies extensionality?  
> **username_4**: @jmite No, η contraction is avoided because it conflicts with β reduction from a confluence standpoint. What is usually missing for extensional equality is a way to go from a point-wise identity _proof_ to the judgmental $x : A ⊢ f x \equiv g x$ so that congruence and η rules can apply. Equality reflection in extensional type theory allows this, but intensional type theory does not.  
> **username_3**: There is a family of equality checking algorithms that can deal with *judgemental* extensionality rules. See [An extensible equality checking algorithm for dependent type theories](https://arxiv.org/abs/2103.07397), and references therein for precursors on which the aglorithm is based. (Apologies for shameless self-promotion.)  

---

