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].
7
questions
11
votes
1
answer
307
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 ...
- 4,087
10
votes
1
answer
485
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 ...
- 258
7
votes
0
answers
167
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 (...
- 4,087
6
votes
1
answer
207
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?
- 127
2
votes
2
answers
145
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 ...
- 125
2
votes
1
answer
106
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 ...
- 345
1
vote
3
answers
147
views
Is there a way to incorporate K's axiom while keeping the system consistent with univalence?
It has been known that if a type $A$ has decidable equality, i.e., $\forall a b: A, a = b \vee a \neq b$, then we can happily say that any two proofs for $a = b$ must be identical. Sometimes, we will ...
- 420