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?

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.