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
11 votes
1 answer
262 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 ...
Trebor's user avatar
  • 3,718
10 votes
1 answer
384 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 ...
keep_learning's user avatar
7 votes
0 answers
151 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 (...
Trebor's user avatar
  • 3,718
5 votes
1 answer
173 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?
Pavel Shuhray's user avatar
2 votes
2 answers
139 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 ...
Tiago Campos's user avatar
2 votes
1 answer
101 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 ...
Russoul's user avatar
  • 345
1 vote
3 answers
105 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 ...
Hiroki Chen's user avatar