# Tag Info

31

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 perfectly aware of its incompletness. (In fact, this is quite obvious, especially when half of the authors are logicians of some sort). But does incompleteness "...

21

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 formalizing HoTT in Idris at the moment. Barrier 1: Idris has heterogeneous equality and heterogeneous equality rewriting. From the HoTT perspective this means we have ...

16

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(a)$. An element of $\Sigma (x : A) . \|P(x)\|$, where $\|{-}\|$ is propositional truncation, is a pair $(a, q)$ where $a : A$ and $q$ is an equivalence class ...

16

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 reasons. First, MLTT is predicative. There is a universe hierarchy, and each type lives at a particular universe level, and a type at level $n$ can only quantify ...

15

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 to give up the axiom in the sense of "personally agree, at a basic philosophical level, that it doesn't hold", you just have to think of it in terms like: "As a ...

15

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 mean one of two things: A single type $E$ which is empty with respect to all types. Such a type has the elimination rule: for every $n$ and type family $A : E \... 14 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 it and learn about it. The fact that your theory is intuitionistic doesn't mean that your meta-theory has to be! You may freely use proof by contradiction or ... 13 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 community, so much was said about "decidability of degeneracies" that we began to give the impression that this was the hard part of the algorithm (since as ... 13 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 less on this topic than he does - but I was mentioned by name, as was my project. When I gave a talk about agda-categories, I explained one thing about it that ... 11 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 a reasonable notion of "skeletality" in HoTT. This is so because equality is so weak that it already means "isomorphic". Furthermore, Theorem 9.4.16 says ... 11 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 features of a programming language, etc. One of the things that we can use type theory for is as a kind of logic (this is known as Curry-Howard correspondence).... 9 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 cubical type theory to be correct, namely that it is sound and conservative. Soundness just means you can encode everything (for instance, that you did not forget to ... 8 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$\lambda$-calculus. Typed$\lambda$-calculus can be used to represent formulae of classical logic. The most well-known system used for this purpose is the ... 7 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. Assume it did. We shall work in a specific model of MLTT with propositional truncation, namely assemblies over number realizability. It is not too important what ... 7 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 used interchangably". Mathematicians casually use this intuition to pretend that two isomorphic things are actually equal when they are not. Univalence ... 7 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 definitional equality with a reduction principle for them) and some do not -- those break canonicity. This is "bad" for different reasons: In theory, canonicity lets you ... 6 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 squash type; there's no way to write an eliminator into any type except another squash type. Relatedly, having squash types, as presented in the book you linked, ... 5 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$to be the statement of the axiom of choice (relative to some universe), then for$M=O_P$the type you showed is inhabited, since you get to use the axiom of ... 5 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 fact that we do not care about the computational behaviour of the postulates. In Observational Type Theory, it is possible to postulate a proof of any consistent ... 4 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 (Martin-Löf's intuitionistic type theory) extended with pattern matching allows you to prove UIP (axiom of uniqueness of identity proofs). Later Streicher and Hoffmann [ 2 ] present a model of ... 4 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 both contractible. Indeed, they are both inhabited and because$\mathrm{Nat}$is a set, its identity type is a proposition, hence so are$A$and$B$, as they are ... 4 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 \to U_n$. This gives a surjective map$f' : A' \to U_m$, and it is not hard to see that the type$A'$is equivalent to a type in$U_m$. Thus we have a ... 3 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 commutativity proof can be shown to be propositionally equal (by a "dependent" equality, or path-over-path) to the$\mathsf{refl}$-returning one, by Andrej's ... 3 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) \;|\; b \in B \}$$ Now it should be obvious that$A + A \not= A$. 3 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 the space in question, which does not exist for every type! The primitive notion in HoTT is that of the path space$I_X$of a type$X\$. But, as far as I know, ...

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