10 votes
Accepted

Type Checking Undecidable in Extensional Type Theory

Extensional type theory is characterized by the reflection rule, which says that if the identity type ${\rm Id}(a,b)$ is inhabited, then $a\equiv b$ ($a$ and $b$ are judgmentally equal). It is called ...
Mike Shulman's user avatar
  • 3,000
7 votes
Accepted

Normalization by evaluation for extensional type theories

For many partial languages, although conversion is undecidable, we can decide conversion up to non-termination. For example, in pure LC, conversion is decidable for the $\beta$-normalizing terms. In ...
András Kovács's user avatar
6 votes
Accepted

What is the state of Nuprl and Extensional Type Theory?

... someone pointed me to this question a few days ago ... The Nuprl group has ceased to exist about two years ago when Richard Eaton (the lead programmer) died unexpectedly and Bob Constable retired. ...
Christoph Kreitz's user avatar
5 votes
Accepted

Is there a way to incorporate K's axiom while keeping the system consistent with univalence?

The question seems to boil down to the implicit assumption that pattern-matching needs uniqueness of identity proofs to work "well" (I will refrain from calling it "axiom K", ...
Meven Lennon-Bertrand's user avatar
3 votes
Accepted

What if identity type in extensional type theory were possibly non-deterministic?

I know of several works that have examined the idea of using some non-trivial decision procedure to implement conversion in a dependent type theory: Coq Modulo Theory, by Pierre-Yves Strub. This ...
cody's user avatar
  • 336
3 votes

Is there a way to incorporate K's axiom while keeping the system consistent with univalence?

The Equations package for Coq/Rocq provides pattern matching without K, as described by Cockx, Devriese, and Piessens and comparable to Agda --without-K, for all ...
James Wood's user avatar
3 votes

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?

The universal property of final coalgebras can be formalized as unique-ana : ∀ (f : A → B × A) (g : A → Stream B) → unfold ∘ g ≡ map₂ g ∘ f → g ≡ ana f where <...
Li-yao Xia's user avatar
  • 1,562
2 votes

Is there a way to incorporate K's axiom while keeping the system consistent with univalence?

It looks like Meven's answer is what you want, but just to answer the core question as stated: I'm seeking methods akin to Streicher's K Axiom, which asserts the uniqueness of identity proofs, but ...
Joey Eremondi's user avatar
2 votes

What if identity type in extensional type theory were possibly non-deterministic?

Your idea to use heuristics and tactics to solve problems in type theory is good, and is massively used, not just for equality checking but also for all sorts of other things. But you are trying to ...
Andrej Bauer's user avatar
  • 8,621

Only top scored, non community-wiki answers of a minimum length are eligible