<p>Are type theories with equality reflection (i.e. having a term of an identity type between two objects allows us to freely swap them) but not the <span class="math-container">$\eta$</span>-rule for <span class="math-container">$\Pi$</span>-types interesting?</p>
<p>Does function extensionality have to hold in such a type theory?</p>

CC BY-SA 4.0
2021-05-16T14:54:18.277Z
Does this answer your question? [Extensional type theory and function extensionality](https://cstheory.stackexchange.com/questions/46331/extensional-type-theory-and-function-extensionality)
Andrej Bauer
CC BY-SA 4.0
2021-05-16T15:11:19.890Z
@AndrejBauer no because we don't assume $\eta$
bkrl
CC BY-SA 4.0
2021-05-16T21:40:23.943Z
Is it interesting is subjective, but I expect that you do not obtain function extensionality in such a type theory. Intuitively, equality reflection collapses the difference between internal and external equality, but without funext externally, this collapse won't imply funext internally.
daniel gratzer
CC BY-SA 4.0
2021-05-16T21:41:09.227Z
I think it's not too much work to cook up a category which has finite limits and a weaker form of dependent product without unicity to actually prove this.
daniel gratzer
<type-theory>
Equality reflection without $\eta$
bkrl
# Equality reflection without $\eta$

(Asked by: username_0 on 2021-05-16)

Are type theories with equality reflection (i.e. having a term of an identity type between two objects allows us to freely swap them) but not the $\eta$-rule for $\Pi$-types interesting?

Does function extensionality have to hold in such a type theory?

**Tags:** type-theory

> **Comments:**
> **username_1**: Does this answer your question? [Extensional type theory and function extensionality](https://cstheory.stackexchange.com/questions/46331/extensional-type-theory-and-function-extensionality)  
> **username_0**: @AndrejBauer no because we don't assume $\eta$  
> **username_2**: Is it interesting is subjective, but I expect that you do not obtain function extensionality in such a type theory. Intuitively, equality reflection collapses the difference between internal and external equality, but without funext externally, this collapse won't imply funext internally.  
> **username_2**: I think it's not too much work to cook up a category which has finite limits and a weaker form of dependent product without unicity to actually prove this.  

---

## 0 answers

