# Tag Info

Accepted

### What is predicativity?

Impredicativity is one of those soft concepts that appears in many related forms, but it is difficult to explain what precisely they share. Let me try anyhow. Impredicativity allows us to single out, ...
• 9,553

### Proof-theoretic comparison table?

Here are a few comparisons of dependent type theories with fragments of Peano arithmetic and set theories that I know of: Predicative systems (the MLTT family) Predicative systems are comparable with ...
• 1,479
Accepted

### Why not have Prop : Set in Coq?

As it often happens with Coq, the answer is historical reasons. In the original version dating back from 1984, Coq was based on the Calculus of Constructions, a barebone dependent type theory. In ...
• 2,316

### What are the advantages to impredicativity?

All impredicativity means is that propositions form a complete lattice! This is a basic principle of mathematics. So if you want to be able to use the architecture of mathematics developed in the last ...
• 2,023
Accepted

### What is the role of impredicativity in program extraction?

I have occasionally thought about this question. My inconclusive conclusion is that impredicativity hinders program extraction. Let me try to give an argument in the context of realizability. I am ...
• 9,553
Accepted

### Why are impredicative constructions used less in type theory than in material set theory?

Regarding natural numbers, and inductive types (ie. initial algebras of some form) in general, impredicative encodings are inconvenient, as they only specify weakly initial algebras, rather than ...
• 5,146

### What is predicativity?

System F allows for function types like $T=\Pi X. X \to X$, where $X$ ranges through all the types. In particular, $T$ is one of them! This means that the usual set-theoretic interpretation of \$\Pi (a:...
• 4,015

### What is predicativity?

As I understand it, impredicativity in type theory is unrelated (at least in a formal way) from impredicativity in set theory. The single rule in a type system which makes it impredicative is the ...
• 2,241
Accepted

### What are the advantages to impredicativity?

There are some tricks that only work when you have access to an impredicative universe. They tend to construct "the smallest object" of some kind, without an explicit construction, i.e. a ...
• 2,316
Accepted

### What is the trade-off to accepting impredicative propositions?

I think this is mainly not a question about usability, but rather a form of discomfort so as to the foundational status of theories incorporating impredicativity. Indeed, as you mentioned, ...
• 5,146
Accepted

### Can we completely erase propositions in the type checker?

The ability to have this kind of "erasure" for propositions is indeed one of the major arguments in favour of having a proper sort of strict propositions (see e.g. Section 9.3 of this ...
• 5,146

### What is the trade-off to accepting impredicative propositions?

There's a general principle to keep in mind: Weaker theories have more models Martin Escardo, Paul Taylor or Andrej Bauer will probably be able to supply some cool geometric examples of this, but ...
• 2,023

### Why are impredicative constructions used less in type theory than in material set theory?

Induction over impredicative encodings requires internalizing a small amount of parametricity. See https://cedille.github.io/ for an example of a language that does this. Otherwise working around the ...
Accepted

### Why can termination checker affect strict Prop in Agda?

After some research I have found a counterexample by Jesper Cockx: ...
• 6,256

### Why are impredicative constructions used less in type theory than in material set theory?

This is not directly an answer to the question, but since two other answers have claimed that impredicative encodings can't satisfy induction principles, I thought someone ought to set the record ...
• 3,180