From 0eb070e183c1f505314684ccdc9118e2a4d927c5 Mon Sep 17 00:00:00 2001
From: Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Fri, 6 Nov 2015 11:39:07 -0500
Subject: [PATCH] fix(hott/book.md): align with previous commit

---
 hott/book.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/hott/book.md b/hott/book.md
index e9adaeb51..6c8397d9c 100644
--- a/hott/book.md
+++ b/hott/book.md
@@ -21,8 +21,8 @@ The rows indicate the chapters, the columns the sections.
 | Ch 4  | - | + | + | + | . | + | ½ | + | + |    |    |    |    |    |    |
 | Ch 5  | - | . | ½ | - | - | . | . | ½ |   |    |    |    |    |    |    |
 | Ch 6  | . | + | + | + | + | ½ | ½ | + | ¾ | ¼  | ¾  | +  | .  |    |    |
-| Ch 7  | + | + | + | - | ½ | - | - |   |   |    |    |    |    |    |    |
-| Ch 8  | ¾ | - | - | - | - | - | - | - | - | -  |    |    |    |    |    |
+| Ch 7  | + | + | + | - | ¾ | - | - |   |   |    |    |    |    |    |    |
+| Ch 8  | ¾ | ¾ | - | - | - | - | - | - | - | -  |    |    |    |    |    |
 | Ch 9  | ¾ | + | + | ½ | ¾ | ½ | - | - | - |    |    |    |    |    |    |
 | Ch 10 | - | - | - | - | - |   |   |   |   |    |    |    |    |    |    |
 | Ch 11 | - | - | - | - | - | - |   |   |   |    |    |    |    |    |    |
@@ -132,7 +132,7 @@ Chapter 7: Homotopy n-types
 - 7.2 (Uniqueness of identity proofs and Hedberg’s theorem): [init.hedberg](init/hedberg.hlean) and [types.trunc](types/trunc.hlean)
 - 7.3 (Truncations): [init.hit](init/hit.hlean), [hit.trunc](hit/trunc.hlean) and [types.trunc](types/trunc.hlean)
 - 7.4 (Colimits of n-types): not formalized
-- 7.5 (Connectedness): [homotopy.connectedness](homotopy/connectedness.hlean) (just the beginning so far)
+- 7.5 (Connectedness): [homotopy.connectedness](homotopy/connectedness.hlean) (the main "induction principle" Lemma 7.5.7)
 - 7.6 (Orthogonal factorization): not formalized
 - 7.7 (Modalities): not formalized, and may be unformalizable in general because it's unclear how to define modalities
 
@@ -142,7 +142,7 @@ Chapter 8: Homotopy theory
 Unless otherwise noted, the files are in the folder [homotopy](homotopy/homotopy.md)
 
 - 8.1 (π_1(S^1)): [homotopy.circle](homotopy/circle.hlean) (only one of the proofs)
-- 8.2 (Connectedness of suspensions): not formalized
+- 8.2 (Connectedness of suspensions): [homotopy.connectedness](homotopy/connectedness.hlean) (different proof)
 - 8.3 (πk≤n of an n-connected space and π_{k<n}(S^n)): not formalized
 - 8.4 (Fiber sequences and the long exact sequence): not formalized
 - 8.5 (The Hopf fibration): not formalized