# Questions tagged [dependent-type]

An overlapping feature of type theory and type systems.

12 questions
Filter by
Sorted by
Tagged with
8k views

### Why does Coq have Prop?

Coq has a type Prop of proof irrelevant propositions which are discarded during extraction. What are the reason for having this if we use Coq only for proofs. Prop is impredicative, so Prop : Prop, ...
• 1,762
7k views

### What is the most intuitive dependent type theory I could learn?

I am interested in getting a really solid grasp on dependent typing. I've read most of TaPL and read (if not fully absorbed) 'Dependent Types' in ATTaPL. I've also read and skimmed a bunch of articles ...
• 1,325
2k views

### Why it's impossible to declare an induction principle for Church numerals

Imagine, we defined natural numbers in dependently typed lambda calculus as Church numerals. They might be defined in the following way: ...
• 1,762
465 views

### How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?

For systems without dependent types, like Hindley-Milner type system, the types correspond to formulas of intuitionistic logic. There we know that its models are Heyting algebras, and in particular, ...
• 2,601
887 views

### Formalizing the theory of finite sets in type theory

Most proof assistants have a formalization of the concept of "finite set". These formalizations, however, differ wildly (although one hopes that they are all essentially equivalent!). What I don't ...
• 1,540
365 views

### Example of where violation of strict positivity condition in inductive types leads to inconsistency

Most dependent typed systems have a strict positivity conditions for inductive types. Does anybody know an example where violation of the condition leads to inconsistency in the system?
• 1,762
829 views

### Fixed points in dependent type theories

Most dependent type theories aim for some notion of correctness in two respects: The type system must be decidable. The type system must be consistent. e.g. $\forall \tau. \tau$ should not be ...
• 1,203
650 views

### "Correctness" of type theory

How to "proof" that type theory is correct? Or at least explain that it's meaningful in some sense. In what extent is this a mathematical question and in what is a philosophical one? When type ...
• 1,762
169 views

### Hereditary Substitution with Inductives and Eliminators?

I'm wondering, is there any existing work on hereditary substitution with inductive type families and dependent eliminators? In particular, normalizing the application of an eliminator to an ...
• 2,942
774 views

### Dependent Sums and Products

I'm trying to understand the connections between a few different concepts fundamental to dependent type theory. Dependent functions ($\Pi$-types) Including non-dependent functions ($A \rightarrow B$)...
• 145
210 views

### Type of induction principle for fixpoint types

To the Calculus of Constructions we could add a general fixpoint type constructor (accepting inconsistencies or assuming F is a ...
• 701
1 vote