hott / book Goto Github PK

Am I the only one getting hundres of warning from pdfTex during compilation, like this:

[285pdfTeX warning (ext4): destination with the same identifier (name{lem.10.2.7}) has been already used, duplicate ignored

Does anyone mind if the trivial homotopy groups of spheres are called 0 instead of 1?

At tea yesterday it was suggested to name LEM_n the version of LEM restricted to n-types, and AC_n the version of AC that involves the n-truncation. Then LEM_infty and AC_infty would be the PAT versions (so AC_infty is provable and LEM_infty is inconsistent with univalence) and LEM_{-1} and AC_{-1} would be the mere-propositional versions (which hold in the sSet model and thus may consistently be assumed).

One technical problem I see with this is that LEM_infty and AC_infty might also be interpreted to refer to the infty-truncation (hypercompletion) rather than no truncation at all. However, that seems unlikely to be a serious problem, since the untruncated meanings of LEM_infty and AC_infty aren't intended for wide use.

A more serious problem is that there are also another parameters in AC. The version of AC in section 2.8.5 assumes that X is a set, each A(x) is a set, and each P(x,a) is a mere proposition; thus this statement lives entirely in the world of sets. If we remove the requirement that X be a set, the statement becomes inconsistent, since we could take A to be the universal cover of the circle. However, I believe the statement is true in the simplicial model when X is a set and each P(x,a) is a mere proposition, with no truncation hypotheses on A (and also still with propositional truncation in the statement), and at least a priori this seems to be a stronger statement. So there is at least another whole axis of truncation indices that we could vary along. There might even be a third one: I don't know what happens if we remove the truncation hypothesis on P.

In revising the set theory chapter I discovered Definition 2.7.1 of a "set" and Definition 5.3.9 of "h-set". What is the official terminology? Should I say "set" or "h-set"?

In homotopy.tex we read "The reason this problem is interesting is that the (higher) inductive
definition of a type X presents X as a free $\infty$-groupoid, and this
presentation \emph{determines} but does not \emph{explicitly describe}
the higher identity types of X.", but no "problem" has been recently mentioned.

The appeal to univalence at the start of the proof of 3.1.1 is not quite clear. The assumptions are that f:A->B and that qinv(f) is inhabited. The latter amounts to two homotopies, rather than proofs of equality, so I don't quite see where univalence applies. I guess you can tacitly convert the homotopies into equalities (paths), then come back out via univalence to get something of the form idtoeqv(p) as stated, but this seems a bit awkward.

Am I just confused?

Are we going to have an index of terms? Even though it is easy to search through a PDF file, an index still points the reader to the most relevant place where a given term is discussed.

Here's a nice timesink for Mike: suppose label1 and label2 refer to Sections. Then \autoref{label1} produces "\S x.y.z" but \autoref{label1,label2} produces "Sections x.y.z and u.v.w".

What does the question mark in table 7.1 signify?

In the computation of pi_1 S^1 it seems the integers are defined as an inductive type, instead of as a quotient. If the definition of Z as a quotient in chapter 10 gets moved to an earlier point, as was agreed, then that should be the definition referred to.

I'm referring to this sentence in homotopy.tex: The proof is by induction, with cases for $0$,$1$,$-1$,$n+1$, and $n-1$.

The sentence

By comparing universal properties, we can identify this with the free group on the set $\pi_0(A)$.

in homotopy.tex is not quite right. For example, if A is S^0, we would get a free group with 2 generators, which is not Z, the fundamental group of S^1.

(The context is taking the pushout 1 <-- A --> 1 and computing its fundamental group.)

Reminder:

The proof of example {universe-is-not-truncated} in homotopy.tex is still to be written.

"It should be possible to show, assuming $\Sn^n:\UU$ for all $n:\nat$, that the universe \UU is not an $n$-type for any $n$, since $\Omega^{n+1}(\UU,\Sn^n)$ should be nontrivial."

In Ch 1, we need to define negation as implication to false, and disequality as the negation of equality.

The statement of Blakers-Massey needs some work. It should refer to the connectedness of the maps C -> X and C -> Y, instead of that of X and Y. The notation C(x,y) is undefined. "glue" should be recalled from 5.8. P should be defined, as Mike noted.

Sections 2.5.2 and 2.5.4 are called $\Sigma$-types and $\Pi$-types, respectively. In a PDF viewer (Skim and Preview on OSX) these appear as "-types" and "-types" in the table of contents sidebar. If anyone knows how to fix this, without ruining the table of contents in the book, please do. For example, you might attempt

\subsection[Pi-types]{$\Pi$-types}

but then in the main table of contents (the paper one) you will see "Pi-types", which is ugly.

the section 1.2 on Universes gets things off to a rather technical and arcane start -- sets as trees, paradoxes, impredicativity, typical ambiguity, it's all rather much for the mathematical reader encountering type theory for the first time.

How about moving this technical discussion to the end of the chapter (and saying that it is optional), and starting with function types instead? We just need to introduce the symbol UU as a way of talking about dependent types. That can be deferred to section 1.4 on dependent types.

UU shouldn't occur in 1.3 anyway.

There are three occurences of the phrase "provably equal". What is that supposed to mean? They were all written by Mike and appear as follows:

1. basics-equivalences.tex: For instance, for a single function $f:A\to B$ there may be multiple inhabitants of~\eqref{eq:qinvtype} which are not provably equal.
2. basics.tex: It's not hard to show that these three elements would be (provably) \emph{equal} (see \autoref{ex:basics:concat}), but there can still be reasons to prefer a particular definition over a provably equal one.
3. introduction.tex: Type-theoretically, this means there are many paths that are \emph{provably} equal to reflexivity, but not definitionally so.

Computer scientists sometime use "provably" when they really mean "we proved it", and that is quite awful. Let us not do that (if that is what we are doing). In any case, as we are not playing games with models, I do not see how we can meaningfully say "provable" (as opposed to "true"). At best we can point out that we actually have a proof of something, bu that is "proved", not "provable".

setmath.tex and uatofe.tex use raw "\lamba x . e" for function abstraction. We have an official \lam macro which should probably be used instead. However, that macro produces very ugly output and I dislike it. It follows the notation for sums and products, which is not necessary at all. Why should a term forming operation follow the same syntax as type forming operations? Just because it abstracts a variable? This is insufficient. May I produce alternative \lam that is not so visually heavy? (And one in which the type of the variable can be omitted.)

"From a foundational point of view, therefore, we may speak of Whitehead’s principle as a “classicality axiom”, akin to LEM and AC....Thus, by showing us a world of mathematics where ∞-groupoids are basic objects, univalent foundations reveals new axioms that have heretofore been implicitly assumed without realizing it, solely due to the nature of our chosen foundational system."

I like the ideas in the paragraph containing the sentences above, and have two remarks:

(1) Is there anything more "fundamental" that would serve as an axiom implying Whitehead's principle?

(2) The phrase "axioms that have heretofore been implicitly assumed without realizing it" will sound a bit fishy to mathematicians who think of Whitehead's Principle as a theorem of classical mathematics, with its own complete proof, not implicitly "assuming" anything. It will also sound a bit fishy to mathematicians who dread the prospect of adding a new axiom to the system in every chapter to cover yet another classical theorem whose proof doesn't quite fit into the new framework. A slight shift of emphasis in the phrasing would perhaps go over better.

In Lemma 10.2.9, item (iii) I use induction in a strange way. The statement involves showing that something holds forall real u and all Cauchy approximations x, and I want to use the inductive hypothesis on a particular x_\delta. Even though it feels like it should be ok, I do not see how to establish the validity of the argument. See the proof, where it says "(WHY CAN I DO THAT?)". Help would be appreciated.

As Andrej said, it would be nice to have a table of common equations, with references to places in the book. This could replace the slightly odd section 2.3.

In homotopy.tex we read a remark about the naive van Kampen's "code":

"code(u, v) is required to be a set, even though it involves the untruncated type A in its definition. This is why the version of van Kampen we are currently describing is “naive”. We will explain at the end of this subsection why this is an undesirable feature, and remedy it in the next subsection."

But in the next section, where the improved "code" is defined, we read

"code(ib, ib′ ) is now a set-quotient of the type of sequences..."

So the second "code" is also forced to be a set. Why doesn't it suffer from the same defect?

For an ordinary inductive definition, the constructors must be strictly positive. For a higher inductive definition, the source and target of path constructors must also be natural. This should be mentioned explicitly somewhere.

There should also be a discussion somewhere of inductive-inductive and/or inductive-recursive definitions, whichever is being used for the Cauchy reals.

Reminder: The question mark in

Most (all ?) constructions introduced in this book are predicative.

in preliminaries.tex seems to indicate a question for the authors to resolve.

Does section 4.3 have a point any more? It seems to basically duplicate parts of chapter 1.

Someone should search all the tex files and convert uses of \lambda to uses of the macro \lam.

should be attributed to Martin Hofmann and Carboni

I'm reviewing, as promised, Chapter 3, but in the process found a typo and a minor unclarity (imho) of the proofs of Lemmas 2.8.11 and 2.8.12, which I have now changed slightly to correct the missing equals sign and make the proof a bit clearer.

The proof of Lemma 3.1.2 seems a little murky to me. I'm going to write out my own version and compare before making any suggestions for any changes.

The following statement in section 2.6 confuses me: "In fact, basically every induction principle in type theory is part of a universal property of this sort", where an example of the said universal property is
\Pi (w : A x B), C(w) is equivalent to \Pi (a : A) \Pi (b : B), C(a,b)
for products, where the function from right to left (typo in the book says left-to-right) is the dependent eliminator.

The statement seems to suggest a direct generalization to natural numbers:
\Pi (n : Nat), C(w) is equivalent to C(0) x (\Pi (n : Nat), C(n) -> C(s(n)))
where the function from right to left is the dependent elimination principle.

However, dependent elimination on natural numbers is not an equivalence: there can be multiple distinct recurrences generating the same function, e.g., the recurrences (0, \lambda n,y, s(n)) and (0, lambda n,y, s(y)) both generate the identity function but they can be easily shown not to be equal. So I am not sure what the statement about universal properties is intended to mean ..?

Thanks,

Kristina

Definition 7.1.1 says it defines the homotopy group, but what's written is just a set.

We need a proof of Eckmann-Hilton somewhere!

The statement of van Kampen will be unsatisfying to mathematicians, because it involves the "code" fibration, whose definition is complicated. Example 7.5.8 attempts to rectify this in the special case where A=1 by relating it to the free product of groups. But what about rephrasing vanKampen so the statement is that Pi_1 transforms a pushout of spaces into a pushout of groupoids, and then specialize that to the case where A is connected by discussing free product with amalgamation? A lemma to prove would then be that the codes fibration is really giving the pushout of groupoids, represented by words.

We should define strict positivity and say that this is a requirement for an inductive type.
Still open: do we need inductive families?

I made some slight modifications to the wording of the proof of 3.1.2 to, I hope, clarify it (and to correct a little typo). I dropped the word "always" because it seemed unclear in that position, and rephrased a bit.

We read this:

When $A$, $B$, and $C$ are not all sets, however, the version of the van Kampen theorem proven in the previous section is not as useful, since it does not identify the path-space of $P$ with a set presented in terms of \emph{set-level data}.

But I'm confused, because up to now A, B, and C have been types, not sets.

The traditional logical notation \land and \lor clashes with the traditional homotopy-theoretic notation for smash products and wedges. Is this irredeemable? What if we just wrote out the words "and" and "or"?

Do we define somewhere what k < n means when k and n are natural numbers?
This is needed to state results like pi_k(S^n) is trivial for k < n.

The axiom of impredicativity of hProp needs to be discussed somewhere, probably in 2.8. I think chapter 9 implicitly assumes this, but is it used anywhere else?

Dan L should check whether my fix to the definition of "code" in f8530d9 is okay (if it's his definition), and whether it prompts any modification to the proofs.

In 1.1 Type theory versus set theory -> third last paragraph -> last sentence

'The collection of all such assumptions is called the context; from a topological point of view it may be thought of as a “parameter space”.'

Most of the definitions online are different to what it should mean here (I guess this is why it is put in quotes).
Wiki definition of "parameter space"
http://en.wikipedia.org/wiki/Parameter_space

So I would recommend that adding some short explanation in the book or adding something in Wikipedia. It could be helpful.

Chapter 4.4 discusses W-types. It says something like "f(b) it the b-th argument, or (for the example of Lists over A), "there are 1 + A many labels in the tree" (labels = constructors). This sounds strange, as A and B are types, but we don't know how to formulate it.

The Pi-W-pretopos part of the chapter on sets will take some work before it fits in with the rest of the book. The text is sometimes repetitive, the diagrams are in TiKZ rather than in xypic, there are footnotes to obscure PDFs in the wiki, definitions define two concepts but only one is in \emph, it says "in the present paper", etc. How finished is this, precisely?

Section 9.1.3 should not be called "Voevodsky's Impredicative quotients" but just "Impredicative quotients", and then explain in the text it is something Vladimir came up with.

If you'd like me to help with any of this, let me know. For example, I can turn TiKZ to xypic.

In particular, this includes the "equivalence induction" formulation of univalence, and the "homotopy induction" formulation of funext. Probably this would fit in chapter 4.

Namely, the identities

ap(f,p@q) = ap(f,p)@ap(q)
ap(f,!p) = !ap(f,p)

Is this stated somewhere? I would expect to find it in the chapter "Functions are functors" but I can't seem to locate it. It is used very often so it should probably be a separate lemma.

Kristina

The comment

"LEM implies that \emph{any} type $X$ has \emph{decidable mere equality}, meaning
[\prd{x,y:X} \big(\brck{x=y} + \brck{x\neq y}\big).]"

in hlevels.tex might benefit if it were pointed out or proved somewhere that negation commutes with squashing. Or indeed, that negative statements are already squashed.

Reminder:

\note{FIXME: recreate table in TeX}
\includegraphics[width=5.5in]{spheres.png}

(see homotopy.tex0

In d42d6e1 I changed three instances of \Omega_1 to \Omega, since it seems that's what was meant. The author might want to confirm that by closing this issue.

Is it just me, or is the n-truncation off by one? To get the n-truncation of A, we should use the hub & spoke with the sphere S^{n+1}, but the book uses S^n. This might have been noticed if the author of proof of 6.3.1 provided a base case for the induction, rather than just the induction step.

Theorem 4.1.1 is called "uniqueness principle" in the description before. It says that two functions with domain Nat are equal if they satisfy the same recurrences (propositionally). Does it make sense to call this "propositional eta"? (2 questions: Do people actually call it "eta", and does it make sense to mention that in the book?)