Skip to main content

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].

Filter by
Sorted by
Tagged with
1 vote
3 answers

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 ...
5 votes
1 answer

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

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 ...
2 votes
1 answer

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 ...
10 votes
1 answer

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 ...
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 (...
11 votes
1 answer

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 ...