Questions tagged [extensional-type-theory]

Use for proof assistants or type theories featuring an equality type that has a reflection rule creating judgemental equalities out of them. See also [reflection].

2 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
7 votes
0 answers

Tutorial implementations of extensional type theories

There are cool projects out there that covers the basic principles of implementing dependent type theories as very spartan proof assistants. These projects helped a lot when I learned about (...
Trebor's user avatar
  • 3,688
4 votes
0 answers

What is the state of Nuprl and Extensional Type Theory?

I want to use extensional type theory. I have installed Nuprl (on a virtual machine). It starts over an hour and I can't find examples or forums. Is there a better way?
Pavel Shuhray's user avatar