32 votes
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 ...
user avatar
  • 26.6k
21 votes
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 ...
user avatar
18 votes
Accepted

Proof relevance vs. proof irrelevance

There are several possible notions of proof relevance. Let us consider three similar situations: An element of a sum $\Sigma (x : A) . P(x)$ is a pair $(a, p)$ where $a : A$ and $p$ is a proof of $P(...
user avatar
  • 26.6k
16 votes

In the Hott book, are the most of the type formers redundant? And if so, why?

You are asking several questions which are similar but distinct. Why doesn't the HoTT book use Church encodings for data types? Church encodings do not work in Martin-Löf type theory, for two ...
user avatar
15 votes

Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?

To me, your question seems analogous to saying "I've heard that non-Euclidean geometry requires me to give up Euclid's fifth axiom, which is very useful in many mathematical contexts." You don't have ...
user avatar
  • 251
15 votes
Accepted

In the Hott book, are the most of the type formers redundant? And if so, why?

Let me explain why the suggested encoding of the empty type does not work. We need to be explicit about universe levels and not sweep them under the rug. When people say "the empty type", they might ...
user avatar
  • 26.6k
14 votes
Accepted

Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?

You seem to be confusing several things here. First of all, like Alexis said in her answer, I don't see why you would need to accept/reject the principles of a given logical theory in order to study ...
user avatar
13 votes
Accepted

Why is regularity a problem in cubical type theory?

The difficulty is in making such a reduction compatible with all the other reductions involving transport/coe. From one perspective it is a “confluence” problem. It is unfortunate that in the ...
user avatar
13 votes

Proof relevance vs. proof irrelevance

I recommend that everyone first read Andrej Bauer's answer, as he covers all the basics extremely well. I agree with everything he says in his answer. I humbly offer more comments, even though I know ...
user avatar
11 votes
Accepted

Relating univalence for a theory of cateogries to the skeleton concept

I refer you to Chapter 9 of the HoTT book. In particular, a category is defined in such a way that isomorphic objects are equal, see Definition 9.1.6. As Example 9.1.15 points out, there really isn't ...
user avatar
  • 26.6k
11 votes

Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?

Type theory is a mathematical theory in which we can do very many different things (set theory is like that as well). We can use type theory for computability, or homotopy theory, or use it to express ...
user avatar
  • 26.6k
10 votes

Can we derive Cubical Type Theory from Self-Types?

This is not an answer but a very long comment. I find the idea quite interesting. To keep things focused, I think it would be very good to have a clear idea of what it means for the encoding of ...
user avatar
  • 26.6k
8 votes

Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?

I agree with Alexis and Damiano, and there is another dimension to $\lambda$-calculus that is not often emphasised, because of the dominance of the Curry-Howard correspondence in thinking about the $\...
user avatar
7 votes
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 ...
user avatar
  • 26.6k
7 votes

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 ...
user avatar
  • 1,882
7 votes
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. ...
user avatar
  • 26.6k
6 votes
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 ...
user avatar
  • 176
6 votes
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 ...
user avatar
5 votes
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$...
user avatar
5 votes

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 ...
user avatar
  • 636
4 votes
Accepted

Surjection from a type to a universe

No, there can't be such a surjection. Here's how to derive a contradiction, if there is a surjective map $f : A \to U_n$, where $A:U_m$. Since $m\leq n$, we can pull $f$ back along the embedding $U_m \...
user avatar
  • 156
4 votes
Accepted

How do we use directed univalence in directed type theory?

If by UKan you mean the ambient universe of all types in the theory (which is a bit of a misnomer, since there is no real Kan-ness to them), then no, it is not Segal. You should think of UCov as &...
user avatar
4 votes

What are the negative consequences of extending CIC with axioms?

A practical example of an axiom behaving badly you ask, what about this? 0 = 1 The Coquand paper referred to might be [ 1 ], where he shows that dependent ITT (...
user avatar
4 votes
Accepted

Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?

But it does follow. The types $$A = \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ n\ m)$$ and $$B = \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$$ are ...
user avatar
  • 26.6k
3 votes
Accepted

What is the coproduct: A + A?

The coproduct is the disjoint union. Set-theoretically, you can think of forming the coproduct of the sets $A$ and $B$ as: $$ A + B \;\;\triangleq\;\; \{ (0, a) \;|\; a \in A \} \cup \{ (1, b) \;|\;...
user avatar
3 votes

In homotopy type theory, is there a IsManifold predicate?

I'm afraid I don't have a clear answer to your question. As I imagine you know, the basic definition of being a manifold cannot even be formulated in HoTT, since it crucially relies on the topology of ...
user avatar
  • 13.2k
3 votes
Accepted

Effect of HoTT/Univalence Axiom on equality between terms of inductive types?

The Univalence axiom has various consequences for the identity types, for example: It implies function extensionality, which governs equality of functions. It implies that the circle has a non-...
user avatar
  • 26.6k
3 votes

Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?

Addressing the question in the title: $\mathsf{\lambda n\,m.\,refl}$ is not a proof of commutativity by definition because addition is not a constant function by definition. Of course, the ...
user avatar
2 votes

How does axiom K contradict univalence?

For a quick reference, here's (equation 8) a proof sketched in Agda. But I guess you're asking for the idea, and I think the reference is kinda technical. When you say 'univalence', you not only mean ...
user avatar
  • 923

Only top scored, non community-wiki answers of a minimum length are eligible