From ed1029641a7df07f5b635dd26a889263fc081ab5 Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Sat, 26 Sep 2015 19:35:58 -0400 Subject: [PATCH] fix(hott/*): update book.md and clean up homotopy.connectedness --- hott/book.md | 22 ++++++++++----------- hott/homotopy/connectedness.hlean | 33 ++----------------------------- hott/types/fiber.hlean | 18 ++++++++++++++++- 3 files changed, 30 insertions(+), 43 deletions(-) diff --git a/hott/book.md b/hott/book.md index 909d6b03a2..895a04fb86 100644 --- a/hott/book.md +++ b/hott/book.md @@ -18,10 +18,10 @@ The rows indicate the chapters, the columns the sections. | Ch 1 | . | . | . | . | + | + | + | + | + | . | + | + | | | | | Ch 2 | + | + | + | + | . | + | + | + | + | + | + | + | + | + | + | | Ch 3 | + | + | + | + | ½ | + | + | - | + | . | + | | | | | -| Ch 4 | - | + | - | + | . | + | - | - | + | | | | | | | +| Ch 4 | - | + | - | + | . | + | ½ | - | + | | | | | | | | Ch 5 | - | . | ½ | - | - | . | . | ½ | | | | | | | | | Ch 6 | . | + | + | + | + | ½ | ½ | ¼ | ¼ | ¼ | ¾ | - | . | | | -| Ch 7 | + | + | + | - | - | - | - | | | | | | | | | +| Ch 7 | + | + | + | - | ½ | - | - | | | | | | | | | | Ch 8 | ¾ | - | - | - | - | - | - | - | - | - | | | | | | | Ch 9 | ¾ | + | + | ¼ | ¾ | ½ | - | - | - | | | | | | | | Ch 10 | - | - | - | - | - | | | | | | | | | | | @@ -90,7 +90,7 @@ Chapter 4: Equivalences - 4.4 (Contractible fibers): [types.equiv](types/equiv.hlean) - 4.5 (On the definition of equivalences): no formalizable content - 4.6 (Surjections and embeddings): [function](function.hlean) -- 4.7 (Closure properties of equivalences): not formalized +- 4.7 (Closure properties of equivalences): Theorem 4.7.6 in [types.fiber](types/fiber.hlean) (the rest not formalized) - 4.8 (The object classifier): not formalized - 4.9 (Univalence implies function extensionality): [init.funext](init/funext.hlean) @@ -110,12 +110,12 @@ Chapter 6: Higher inductive types --------- - 6.1 (Introduction): no formalizable content -- 6.2 (Induction principles and dependent paths): dependent paths in [init.pathover](init/pathover.hlean), circle in [hit.circle](hit/circle.hlean) -- 6.3 (The interval): [hit.interval](hit/interval.hlean) -- 6.4 (Circles and spheres): [hit.circle](hit/circle.hlean) -- 6.5 (Suspensions): [hit.suspension](hit/suspension.hlean) (we define the circle to be the suspension of bool, but Lemma 6.5.1 is similar to proving the ordinary induction principle for the circle in [hit.circle](hit/circle.hlean)) and a bit in [hit.sphere](hit/sphere.hlean) and [types.pointed](types/pointed.hlean) -- 6.6 (Cell complexes): we define the torus using the quotient, see [hit.two_quotient](hit/two_quotient.hlean) and [hit.torus](hit/torus.hlean) (no dependent eliminator defined yet) -- 6.7 (Hubs and spokes): [hit.two_quotient](hit/two_quotient.hlean) and [hit.torus](hit/torus.hlean) (no dependent eliminator defined yet) +- 6.2 (Induction principles and dependent paths): dependent paths in [init.pathover](init/pathover.hlean), circle in [homotopy.circle](homotopy/circle.hlean) +- 6.3 (The interval): [homotopy.interval](homotopy/interval.hlean) +- 6.4 (Circles and spheres): [homotopy.sphere](homotopy/sphere.hlean) and [homotopy.circle](homotopy/circle.hlean) +- 6.5 (Suspensions): [homotopy.suspension](homotopy/suspension.hlean) (we define the circle to be the suspension of bool, but Lemma 6.5.1 is similar to proving the ordinary induction principle for the circle in [homotopy.circle](homotopy/circle.hlean)) and a bit in [homotopy.sphere](homotopy/sphere.hlean) and [types.pointed](types/pointed.hlean) +- 6.6 (Cell complexes): we define the torus using the quotient, see [hit.two_quotient](hit/two_quotient.hlean) and [homotopy.torus](homotopy/torus.hlean) (no dependent eliminator defined yet) +- 6.7 (Hubs and spokes): [hit.two_quotient](hit/two_quotient.hlean) and [homotopy.torus](homotopy/torus.hlean) (no dependent eliminator defined yet) - 6.8 (Pushouts): [hit.pushout](hit/pushout.hlean) (not everything yet) - 6.9 (Truncations): [hit.trunc](hit/trunc.hlean) (not everything yet) - 6.10 (Quotients): [hit.set_quotient](hit/set_quotient.hlean), [types.int](types/int/int.md) (folder) (not everything yet) @@ -130,7 +130,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): not formalized +- 7.5 (Connectedness): [homotopy.connectedness](homotopy/connectedness.hlean) (just the beginning so far) - 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 @@ -139,7 +139,7 @@ Chapter 8: Homotopy theory Unless otherwise noted, the files are in the folder [homotopy](homotopy/homotopy.md) -- 8.1 (π_1(S^1)): [hit.circle](hit/circle.hlean) (only one of the proofs) +- 8.1 (π_1(S^1)): [homotopy.circle](homotopy/circle.hlean) (only one of the proofs) - 8.2 (Connectedness of suspensions): not formalized - 8.3 (πk≤n of an n-connected space and π_{k