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 ...
Hiroki Chen's user avatar
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?
Pavel Shuhray's user avatar
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 ...
Tiago Campos's user avatar
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 ...
Russoul's user avatar
  • 345
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 ...
Trebor's user avatar
  • 3,967
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,967
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 ...
keep_learning's user avatar