Skip to main content
24 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(...
Andrej Bauer's user avatar
  • 29.2k
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 ...
Neel Krishnaswami's user avatar
16 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 ...
Alexis's user avatar
  • 261
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 ...
Andrej Bauer's user avatar
  • 29.2k
15 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 ...
Jonathan Sterling's user avatar
14 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 ...
Jacques Carette's user avatar
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 ...
Damiano Mazza's user avatar
12 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 ...
Andrej Bauer's user avatar
  • 29.2k
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 ...
Andrej Bauer's user avatar
  • 29.2k
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 $\...
Martin Berger's user avatar
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. ...
Andrej Bauer's user avatar
  • 29.2k
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 ...
L. Garde's user avatar
  • 176
5 votes
Accepted

Generalizations, or extensions of W-types in MLTT

The representation issue of W-types was resolved by Jasper Hugunin. So from type formers $0$, $1$, $2$, $W$, $\Pi$, $\Sigma$, identity and a universe hierarchy we do get all indexed inductive families ...
András Kovács's 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$...
Mike Shulman's user avatar
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 \...
Egbert's user avatar
  • 156
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 ...
Andrej Bauer's user avatar
  • 29.2k
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 &...
Mike Shulman's user avatar
3 votes

Generalizations, or extensions of W-types in MLTT

You could start with Spartan type theory (which honestly should be upgraded to use evaluation-by-normalization) and add simple inductive datatypes to them. This would involve several steps. First, add ...
Andrej Bauer's user avatar
  • 29.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-...
Andrej Bauer's user avatar
  • 29.2k
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) \;|\;...
Neel Krishnaswami's user avatar
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 ...
András Kovács's 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 ...
ice1000's user avatar
  • 957

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