# Equality reflection without $\eta$

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?

• Does this answer your question? Extensional type theory and function extensionality May 16 '21 at 14:54
• @AndrejBauer no because we don't assume $\eta$
– bkrl
May 16 '21 at 15:11
• 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. May 16 '21 at 21:40
• 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. May 16 '21 at 21:41