# Tag Info

Accepted

### Homotopy type theory and Gödel's incompleteness theorems

HoTT "suffers" from Gödel incompleteness, of course, since it has a computably enumerable language and rules of inference, and we can formalize arithmetic in it. The authors of the HoTT book were ...
• 26.6k
Accepted

### Formalizing Homotopy Type theory in Idris

Here is a small, incomplete, and inconsistent formalization of HoTT in Idris. It shows that you can derive a contradiction in Idris just by postulating univalence. There are two barriers to ...
Accepted

• 10.3k
Accepted

### How Univalence can be used for proofs about algorithm correctness

The univalence axiom is not a magic wand that solves all problems. Univalence has an immense explanatory power because it makes mathematically precise the intuition that "isomorphic structures can be ...
• 26.6k

### What are the negative consequences of extending CIC with axioms?

One first reason to reject axioms is that they might be inconsistent. Even for the axioms that are proved consistent, some of them have a computational interpretation (we know how to extend ...
• 1,882
Accepted

### Choose term of coproduct type

We are going to show that in MLTT with propositional truncation the type $$\textstyle \prod_{A:U_0}\prod_{B:U_0} (\|A\| \to A) \times (\|B\| \to B) \to (\|A + B\| \to A + B)$$ has no inhabitants. ...
• 26.6k
Accepted

### How does axiom K contradict univalence?

You will certainly find it natural that most types, like structures, admit different isomorphisms. Just take the type $\textbf{2}$, with inhabitants $0_\textbf{2}$ and $1_\textbf{2}$. It admits 2 ...
• 176
Accepted

### Squash type vs Propositional truncation type

Squash types correspond to judgmental truncation, not propositional truncation. In a type theory without a type for judgmental equality, there's non much of a way to make use of an inhabitant of a ...
• 251
Accepted

### Obtaining the Axiom of Choice through a modality in HTT

There is a trivial sense in which the answer is yes. For any proposition $P$, there's a modality $O_P$ called the open modality determined by $P$, defined by $O_P(X) \equiv (P\to X)$. If you take $P$...
• 665

### What are the negative consequences of extending CIC with axioms?

To understand why extending a theorem prover with some axioms can cause problems, it is also interesting to see when it is benign to do so. Two cases come to mind and they both have to do with the ...
• 636
Accepted

• 1,329