# Tag Info

### Has anyone ever accidentally "proven" a false theorem with type-in-type?

I did this myself! (At least, if you interpret "incorrect" as "probably not true" rather than "demonstrably false".) In the early days of homotopy type theory, we were ...
• 3,200
Accepted

### Has anyone ever accidentally "proven" a false theorem with type-in-type?

Yes. In fact, there is a very interesting example which is tied to the history of dependent type theory: Per Martin-Löf, in his 1971 manuscript*, studied a system with type-in-type which famously ...
• 1,489
Accepted

### What are the bases for different Proof Assistants?

There are a lot of bases, theories and techniques in proof assistants. Let me show you how deep the rabbit hole is (in suggested order of implementation): (Fibrational) Dependent Type Theories CoC (...
• 1,297

### What are the bases for different Proof Assistants?

Here are some other points in the space: NuPrl has dependent types but is pretty different from, e.g., Coq; as I understand it, it's based on a model of untyped computation and proofs of well-...
• 1,547
Accepted

### What are the motivations for different variants of categorical models of dependent type?

I would divide these models into three general groups. Structures that are more "categorical", arising naturally from categories "in nature" without the need for strictification ...
• 3,200
Accepted

### Easy ways to introduce inductive types

In principle, every indexed inductive type can be defined from $\bot$, $\top$, $\mathsf{Bool}$, $\Pi$, $\Sigma$, $\mathsf{W}$, $\mathsf{Id}$ and universes, with exactly the expected eliminators and ...
• 2,077

### Bringing OOP features into proof assistants?

Object oriented programming cannot easily be integrated into proof assistants, because object types are naturally mixed-variance. For example, a Java interface like: ...
• 2,053
Accepted

### Bringing OOP features into proof assistants?

Semantics The main OOP investigation and modeling in second order type theory was done by Luca Cardelli and Martin Abadi, e.g. in Theory of Objects and later was continued by Anton Setzer in Object-...
• 1,297
Accepted

### Can you build W-types out of natural numbers predicatively?

The answer is no. According to Anton Setzer's PhD thesis: Proof theoretical strength of Martin-Löf Type Theory with W-type and one universe: Aczel has shown in [Acz77] that Martin-Löf’s type theory ...
• 2,300

### What are the bases for different Proof Assistants?

ACL2 is based on the logic of Common Lisp. This means several things: The universe (over which one quantifies and defines predicates) consists of the s-expressions. Logically, it is equivalent to ...
• 2,300
Accepted

### What's the relationship between refinement types and dependent types?

Is there something that is only possible with refinement types, but not possible (or extremely hard to imitate) in dependent types? Yes. Refinement types make the notion of logical or ghost term ...
• 2,053

### What are the upsides and downsides of typed vs untyped conversion?

From the perspective of implementation of conversion checking, it really depends on the specific setting. For vanilla intuitionistic type theories without more exotic features (like cubical TT, ...
• 2,077
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 ...
• 3,200

### What's the relationship between refinement types and dependent types?

I am not sure that there is a unique definition of refinement types, but there is a common theme. In general, a system featuring refinement types is some kind of ML extended with a subset type ...
• 2,333

### What about dependent types is useful for theorem provers?

A general-purpose proof assistant must be built on a foundation that is strong enough to represent most or all of mathematics, since proofs take place in mathematics. Dependent type theory, like ...
• 3,200
Accepted

### In the "Simply Easy!" paper, why is it safe to evaluate types in the empty environment?

All is well. The implementation distinguishes between bound variables, represented as Bound i where i :: Int and free variables, ...
• 9,802
Accepted

### Does "unique mere existence" imply "existence"?

If $\varphi$ is proposition-valued and has at most one witness, then $\sum_{x:X}\varphi(x)$ is a proposition. We can see this because, given two inhabitants of $\sum_{x:X}\varphi(x)$, they have the ...
• 1,053
Accepted

### Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

[Supplemental: I rewrote the answer so that any shred of vagueness is gone, as it was evoking religuous zeal, and I would prefer to stick to math. Everything is explained in terms of a widely accepted ...
• 9,802

### What about dependent types is useful for theorem provers?

Dependent types allow quantifiers over values, which is very important in describing propositions. This is impossible in, for example, simple type theory (on the other hand, it is not necessary to ...
• 6,306
Accepted

### What are the principal differences between Agda's core type theory and Coq's?

I will answer the headline question and ignore UTT (I believe thinking of Agda as UTT causes more confusion than it solves). There are very many differences between the theories Agda and Coq implement,...
• 1,053

### Are Logics Based on Dependent Types Stronger Than Ones Without?

Pretty much always, it means "this gadget is more annoying to formalise in HOL", not "this gadget is not possible to formalise in HOL." A simple example of this is formalising ...
• 2,053
Accepted

### How can you represent a dependent type visually?

I addressed some of these questions in my lecture “Spartan Type Theory” (PDF slides) at the UniMath 2017 school in Birmingham. In particular, slide 18 looks like this: Please look at the slides for ...
• 9,802

### Universe inconsistency as an effect

I don't have an answer, but I would like to provide some buzzwords and references that will make it easier to find relevant literature. Some background information Computational effects and dependent ...
• 9,802

### In a dependently typed language, are all types statements?

To make the basics clear: languages don't mean anything before you assign them meanings manually, and you can interpret the same language different ways. So if you want to interpret a dependent type ...
• 4,025

### Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

Is this perhaps a problem with 'common understanding' regarding what it means to be Turing complete? Indeed it is: a pop-science understanding of dependent types has led to this myth being deeply ...
• 1,266

### Formalization of abstract definitions

Maybe if you look at things the other way around, you’ll see why this is not a particularly deep feature from the type-theoretic point of view. Instead of viewing an abstracted definition as a ...
• 5,530
Accepted

### How to implement first-order relational structures in Coq?

Supplemental: It looks like I misunderstood the point of the question and the OP might have simply been looking for the sig type, usually written as ...
• 9,802

### What are the upsides and downsides of typed vs untyped conversion?

Typed conversion makes establishing metatheoretical properties of the syntax overwhelmingly easier, especially if you want to prove things like decidability of typechecking. Basically, when showing ...
• 2,053
Accepted

### Interpretation of dependent types: Coherence

I have commented with Curien's 1990 work on substitution up to isomorphisms, but you said it's too old. Here's a quite new reference, by Lumsdaine and Warren: https://arxiv.org/abs/1411.1736 It was ...
• 6,306