# solutions to exercises: 8.1 8.3 8.4 8.5 #840

Merged
merged 3 commits into from Aug 12, 2015

## Conversation

### LuisScoccola commented Jul 22, 2015

 No description provided.
 solutions to exercises: 8.1 8.3 8.4 8.5 
 019f39a 
 $\eqv{ \Parens{(a,b)=(a,b), \refl{(a,b)}} }{\Parens{(a=a \times b=b), (\refl{a}, \refl{b})}}.$ By Univalence Axiom this is the same as proving the equality.

#### mikeshulman Jul 23, 2015

Contributor

I don't see where univalence comes in here? I think this equivalence should be true without any need for univalence. Maybe the point is that when we say "equivalence of pointed types" we mean by definition an equivalence of underlying types that respects the basepoints?

#### LuisScoccola Jul 30, 2015

Author

I thought we had to prove the equality, not only the equivalence. Fixed.

 Now is a good time to make a drawing to convince oneself that this is the right way to define the inclusions between consecutive spheres, and that this is the diagram intended in he exercise.

#### mikeshulman Jul 23, 2015

Contributor

Typo: "the exercise"

 constructed. The constructors are: \begin{align*} j_{\blank} &: \prd{n : \nat} \Sn^n \to \Sn^{\infty}\\ \glue_{\blank} &: \prd{n : \nat} \prd{x: \Sn^n} j_n(x) = j_{n+1}\circ i_n (x)

#### mikeshulman Jul 23, 2015

Contributor

I guess by j_{n+1}\circ i_n (x) you mean (j_{n+1}\circ i_n)(x), but that's one of those things that's not immediately obvious how to parse. I would tend to write j_{n+1}(i_n (x)) instead.

 We also have the usual computational rules. Now, we can interpret the proof that we are going to give as follows. Each sphere is the equator'' of the next one. We say equator'' because it passes trough $\north$ and $\south$ so technically you have to rotate the bigger sphere for

#### mikeshulman Jul 23, 2015

Contributor

Typo: "through"

 Now, we can interpret the proof that we are going to give as follows. Each sphere is the equator'' of the next one. We say equator'' because it passes trough $\north$ and $\south$ so technically you have to rotate the bigger sphere for the inclusion to be exactly in the equator.

#### mikeshulman Jul 23, 2015

Contributor

If you don't want to have to rotate, I guess you could say "meridian" instead of "equator". (-:

 \end{tikzpicture} \end{center} we get a path $x \defeq j_n(y) = j_{n+1} \circ i_n(y)$. But, as we will show, the image of $\Sn^n$ under $i_n$ is contractible,

#### mikeshulman Jul 23, 2015

Contributor

"the image of $\Sn^n$ under $i_n$ is contractible" is a little imprecise, which I suppose is okay since this is only an outline, but I think it might confuse the reader. What you mean is that the "inclusion" i_n is nullhomotopic, right?

 equals $j_{n+1}\circ i_n(\north_n)$. By concatenation with $\glue_n(\north_n)$, we reduce our goal to the inductive hypothesis. Lets now show that the inclusion of $\Sn^n$ in $\Sn^{n+1}$ can be

#### mikeshulman Jul 23, 2015

Contributor

Typo: "Let's"

 Lets now show that the inclusion of $\Sn^n$ in $\Sn^{n+1}$ can be continuously retracted to $\north_{n+1}$. That is, lets construct a homotopy:

#### mikeshulman Jul 23, 2015

Contributor

Again: "let's"

 Now we define the inclusions $i_n : \Sn^n \to \Sn^{n+1}$. For the base case we have to give a function $i_0 : \bool \to \susp \bool$. This is easy: send one point to $\north$ and the other to $\south$.

#### mikeshulman Jul 23, 2015

Contributor

I know the exercise says to start with S^0, but I notice that if we start with S^{-1} instead, which is empty, then the base case is even easier. (-:

#### LuisScoccola Jul 30, 2015

Author

That's true. In fact, by starting at 0 one has to repeat part of the argument. I prefer to start at 0 only because I like the family S^- to be defined over the natural numbers. But I can change it if it is not elegant to repeat part of an argument.

#### andrejbauer Jul 30, 2015

Member

You can also change the exercise in the book to have it start with 0 :-)

#### mikeshulman Jul 30, 2015

Contributor

I think it is fine as-is, I was just making an observation.

 Composing the two proofs we just gave we get a function: $J_{\blank} \defeq \glue_n(x)\ct \apfunc{j_{n+1}}{H_n(x)}\ct D_{n+1} : \prd{n:\nat}\prd{x:\Sn^{\infty}} j_n(x) = j_0(\north_0).$

#### mikeshulman Jul 23, 2015

Contributor

Typo: x:\Sn^n.

#### mikeshulman Jul 23, 2015

Contributor

Also, just a comment (not mandatory to change): the macro \prd is smart so that you don't need to write it twice: you can just say \prd{n:\nat}{x:\Sn^n}.

#### mikeshulman Jul 23, 2015

Contributor

This confused me at first; when you said "is just" and then displayed an equality, I thought you were saying that the previous displayed equation reduced to this equation. But instead you are saying that the LHS of the previous displayed equation reduces to the LHS of this equation, which we know to be equal to the RHS of this equation by cancellation. Maybe you could clarify the wording.

 $\apfunc{j_{n+1}}{H_n(x)} = \glue_{n+1}(i_n(x))\ct\apfunc{j_{n+2}}{H_{n+1}(i_n(x))} \ct\glue_{n+1}(\north_{n+1})$ But we remeber that we have the homotopy

#### mikeshulman Jul 23, 2015

Contributor

Typo: "remember"

 But we remeber that we have the homotopy $\glue_{n+1} : j_{n+1} = j_{n+2}\circ i_{n+1}$, so, by a simple application of \cref{lem:htpy-natural}, the functoriality of $\apfunc{}{}$, and some standard cancelations, we reduce the goal to:

#### mikeshulman Jul 23, 2015

Contributor

Typo: "cancellations"

 $\glue_{n+1} : j_{n+1} = j_{n+2}\circ i_{n+1}$, so, by a simple application of \cref{lem:htpy-natural}, the functoriality of $\apfunc{}{}$, and some standard cancelations, we reduce the goal to: $\apfunc{i_{n+1}}{H_n(x)} = H_{n+1}(i_n(x))$

#### mikeshulman Jul 23, 2015

Contributor

I would appreciate having this reduction spelled out in a little more detail.

 First we write down the type of the induction principle explicitly: \[ \ind{\Sn^\infty} : \prd{C:\Sn^\infty \to \UU} \prd{n:C(\north)}\prd{s:C(\south)}

#### mikeshulman Jul 23, 2015

Contributor

Again, you can leave out the intermediate \prds (and doing so causes the book-style parentheses to get inserted).

 We know that every two points $y_1,y_2 : Y$ are merely equal, because $Y$ is is connected. That is, we have a function $c : \prd{y_1,y_2:Y}\trunc {} {y_1 = y_2}$.

#### mikeshulman Jul 23, 2015

Contributor

This is by Exercise 7.6, I guess; is that fact stated anywhere else in the book?

#### LuisScoccola Jul 30, 2015

Author

I was refering to Remark 3.11.2. It is true that this is not the standard definition, so I added a comment in the solution.

 We note that it suffices to show that for any $y_1,y_2:Y$ we have $\trunc {} {\hfib{f}{y_1} = \hfib{f}{y_2}}$ because by Univalence $\hfib{f}{y_1} = \hfib{f}{y_2}$ is equivalent to $\hfib{f}{y_1}\simeq \hfib{f}{y_2}$ and thus, by Univalence, they are equal.

#### mikeshulman Jul 23, 2015

Contributor

Again, the application of univalence is unnecessary here.

#### LuisScoccola Jul 30, 2015

Author

You are absolutely right. On the other hand, I noticed that (without using univalence) we can prove the equality instead of the equivalence. It is in fact simpler.

Contributor

### mikeshulman commented Jul 23, 2015

 This is very nice! Modulo my comments, it looks good to me, but since the writeup is somewhat lengthy I would appreciate it if someone else had the time to look it over as well. One general comment: since \blank is shorthand for a lambda-abstraction, I guess f_{\blank} is shorthand for \lam{x} f_x, which by the uniqueness rule is equal to f. So while it's not wrong to write f_{\blank} \defeq, it's simpler to just write f \defeq, and probably less confusing (especially if the type of f is actually a function of multiple variables).
 Fixed (I hope) the corrections made by Mike. 
 dd54c75 
Author

### LuisScoccola commented Jul 30, 2015

 I know that putting \blank can sometimes be confusing. I used it in this case because every function in the proof is indexed over the natural numbers, and \blank shows where the index n will be placed. When the function takes multiple arguments, the natural n is always the first one, so I think it is clear, but I can certainly be wrong.
 is connected. That is, we have a function $c : \prd{y_1,y_2:Y}\trunc {} {y_1 = y_2}$. This is by definition, if we use the definition stated in \textit{Remark $3.11.2$}. Otherwise we can use \cref{ex:connectivity-inductively}.

#### mikeshulman Jul 30, 2015

Contributor

Ah! I think the intended definition was that of \cref{ex:connectivity-inductively}, which is the standard meaning of "connencted" (= 0-connected). The other is actually something that I think now should be changed; will open a new PR.

#### mikeshulman Aug 6, 2015

Contributor

Could you please update this reference, now that my PR has been merged? I think the correct thing to point to is "the remark after \cref{thm:connected-pointed}" or else just \cref{ex:connectivity-inductively}.

referenced this pull request Jul 30, 2015
 We know that every two points $y_1,y_2 : Y$ are merely equal, because $Y$ is is connected. That is, we have a function $c : \prd{y_1,y_2:Y}\trunc {} {y_1 = y_2}$. This is by definition, if we use the definition stated in \textit{Remark $3.11.2$}. Otherwise we can use

#### mikeshulman Aug 6, 2015

Contributor

I think the citation of 3.11.2 should be removed in this case, but just for future reference, you shouldn't explicitly write in the number of any theorem or remark. If it doesn't have a label yet in the source that you can use \cref on, just add such a label as part of the PR. (You'll need to re-run make main.labels after adding such a label before it will show up in exercise_solutions.)

 Reference to {thm:connected-pointed} updated 
 f080698 
Contributor

### mikeshulman commented Aug 12, 2015

 Thanks for your patience with all my suggestions. It doesn't look like anyone else is going to look at this, so I'll go ahead and merge it. Thanks for a nice write-up!
added a commit that referenced this pull request Aug 12, 2015
 Merge pull request #840 from LuisScoccola/exercise_solutions 
 e895971 
solutions to exercises: 8.1 8.3 8.4 8.5
merged commit e895971 into HoTT:master Aug 12, 2015
1 check passed
1 check passed
continuous-integration/travis-ci/pr The Travis CI build passed
Details
Contributor

### nicolaikraus commented Aug 13, 2015

 I think these solutions are very good. There is one small typo that should be fixed. Sorry, I know I'm too late, so I'll create a quick pull request for that fix (I hope that's the way to do this? - I don't have too much experience with all the possibilities git offers).
referenced this pull request Aug 13, 2015