# Questions tagged [dependent-types]

An overlapping feature of type theory and type systems.

117 questions
Filter by
Sorted by
Tagged with
143 views

### Difference between computation in proposition proof and definitional computation?

As stated in equality at nLab, "computational equality" is about computational steps which take for example, $s(s(0))+ s(0)$ to $s(s(s(0)))$ and it acts exactly and can be considered same as ...
52 views

### How to find a term that proves a given proposition?

I'm reading this book, and there's something basic that I don't exactly get. The authors say that every common noun is declared to be a type. For example, $Human:Type$. Then, they give an example of ...
394 views

### Relationship between inductive families and type-returning functions

Dependently typed languages such as Agda support inductive families, also called indexed datatypes, which allow type parameters to vary between constructors. This can be used to define a set of ...
91 views

### Resources for connections between dependent type theory and LCCC

Can someone recommend introductory articles/papers on the connections between dependent type theory and locally cartesian closed category? Many Thanks!
26 views

### Introduction to Calculus of Inductive Constructions

Which books/notes teach Calculus of Inductive Constructions (CIC) without using a specific programming languages like Coq or Lean? I would like a reference that also doesn’t assume (naive) set theory, ...
1 vote
44 views

### Finding an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$

Let $\ast$ stand for "type" and $\square$ stand for "kind" so that $\ast:\square$. Suppose I want to find an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$. The derivation rules are ...
1 vote
40 views

### What types can be written in Kind but not Lean?

The Kind programming language has a sufficiently powerful type system to support proving theorems like in Lean, Coq, Idris, or Agda. I've seen it said that Kind has an even more powerful type system ...
1 vote
93 views

### Can the Calculus of Constructions (without inductives) be used to axiomatize mathematics?

I'm aware that proof assistants like Coq and Agda are based on CIC rather than CoC because there is e.g. no inductive natural number type in CoC. Therefore, for example the proof that addition is ...
155 views

### What are some examples of proofs that are also themselves "useful" programs?

With dependent types, types can be statements that are true or false and constructing a value with that type constitutes a proof of that statement. This proof/value construction is itself a program ...
109 views

### What is an explanation of the replace operator in the Pie language?

This is the first concept in The Little Typer to give me quite a bit of trouble, and it appears I am not alone (1 2), so perhaps it would be beneficial to ask here. Hopefully this can be connected ...
77 views

### What are strong examples of programming languages whose type systems don't embed into their native type theory?

Given a typical popular programming language, its native type theory is a dependent type theory which describes invariants, preconditions, predicates, and other generalizations of typical type-system ...
76 views

### Relationship between cartesian product and dependent product type

Introduction: Hi, I'm quite new to types so apologies in advance for the basic question and for any abuse of terminology. I believe I have a critical misunderstanding of dependent product types (and ...
1 vote
146 views

### Proving transitivity in an intuitionistic type theory without the K rule

In Agda, if I disable axiom $\mathbb{K}$ I'm not able to prove $$\forall\{A : \textbf{Set}\}\{a\ b : A\}\{p\ q : a \equiv b\} \to p \equiv q,$$ which I guess is normal since the system does not ...
633 views

### Decidability of dependent typing on primitive recursive languages

With a dependent type system in a normal functional language type checking may never halt. This is partially because dependent typing removes the isolation between types, and code. My question is this:...
1 vote
24 views

### How to specify a type for a SQL-like query?

What follows is a pretty complicated object (in an object-oriented, imperative, typed language), which I would like to create a type for with some sort of type annotations. I am open to how it is done,...
488 views

### What are the rules for positive recursive types in dependent type theory?

I've recently started independently learning type theory, using a combination of papers found online and ncatlab.org (but have not worked with category theory), and am about to start reading TAPL. I'...
2k views

2k views

### Why does Coq include let-expressions in its core language

Coq includes let-expressions in its core language. We can translate let-expressions to applications like this: let x : t = v in b ~> (\(x:t). b) v I understand ...
107 views

### Calculus of constructions, type-in-type and recursion

Does adding type-in-type to the calculus of constructions lead to (general) recursion? Such that one can write the Y combinator.
819 views

### What does canonicity property mean in Type Theory?

The "Computational Component" section of the Type Theory - Wikipedia (as well as a few papers about cubical type theory and 2d type theory) talk about canonicity property. Would you please explain ...
171 views

### Why values can not be replaced with their extensionally equal values in an intensional system?

Thomas Streicher states in Investigations into Intensional Type Theory(§Introduction p.5) that: Although in Intensional constructive set theory (Intensional Type Theory) one can do most of the ...
231 views

### Definition of extensional and propositional equality in Martin-Lof extensional type theory

Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.[4-5]) that: A similar situation occurs in extensional Martin-Lof type theory where propositional and definitional ...