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].
6
questions
4
votes
0
answers
60
views
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?
2
votes
2
answers
134
views
What if identity type in extensional type theory were possibly non-deterministic?
In extensional type theory, identity types are lifted to the definitional equality mechanism, this lead to a bunch of problems, and I imagine that's why they are not very popular.
My question is if we ...
- 336
2
votes
1
answer
98
views
Is existence of Stream as final co-algebra for the suitable functor enough to write functions into equality of streams by co-induction in ExtMLTT?
Suppose we work inside MLTT with equality reflection (extensional MLTT).
Assume I postulate existence of Streams as final co-algebra for the suitable functor.
Is that enough to prove the bisimulation ...
- 1,517
9
votes
1
answer
330
views
Type Checking Undecidable in Extensional Type Theory
What is the difference between intensional vs extensional type theories and how come the type checking is undecidable for extensional type theory? Also, how does it affect the expressiveness of ...
- 3,688
7
votes
0
answers
146
views
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 (...
- 3,688
11
votes
1
answer
245
views
Normalization by evaluation for extensional type theories
Is there material on how to implement normalization for (any flavor of) ETT?
This describes techniques related to doing untyped normalization. But there are (operational and semantic) problems when ...
- 3,688