fix(hott/*): update book.md and clean up homotopy.connectedness
This commit is contained in:
Ulrik Buchholtz
Leonardo de Moura
parent
2c22501084
commit
ed1029641a
3 changed files with 30 additions and 43 deletions
22
hott/book.md
22
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<n}(S^n)): not formalized
|
||||
- 8.4 (Fiber sequences and the long exact sequence): not formalized
|
||||
|
|
|
|||
|
|
@ -3,39 +3,10 @@ Copyright (c) 2015 Ulrik Buchholtz. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Ulrik Buchholtz
|
||||
-/
|
||||
import types.trunc
|
||||
import types.trunc types.arrow_2 types.fiber
|
||||
|
||||
open eq is_trunc is_equiv nat equiv trunc function
|
||||
|
||||
-- TODO(Ulrik) move this to somewhere else (cannot be sigma b/c dep. on fiber)
|
||||
namespace sigma
|
||||
variables {A : Type} {P Q : A → Type}
|
||||
|
||||
definition total [reducible] (f : Πa, P a → Q a) : (Σa, P a) → (Σa, Q a) :=
|
||||
sigma.rec (λa p, ⟨a , f a p⟩)
|
||||
|
||||
-- Theorem 4.7.6
|
||||
--definition fiber_total_equiv (f : Πa, P a → Q a) {a : A} (q : Q a)
|
||||
-- : fiber (total f) ⟨a , q⟩ ≃ fiber (f a) q :=
|
||||
--sorry
|
||||
|
||||
end sigma
|
||||
|
||||
-- TODO(Ulrik) move this to somewhere else (cannot be unit b/c dep. on fiber)
|
||||
namespace unit
|
||||
|
||||
definition fiber_star_equiv (A : Type) : fiber (λx : A, star) star ≃ A :=
|
||||
begin
|
||||
fapply equiv.MK,
|
||||
{ intro f, cases f with a H, exact a },
|
||||
{ intro a, apply fiber.mk a, reflexivity },
|
||||
{ intro a, reflexivity },
|
||||
{ intro f, cases f with a H, change fiber.mk a (refl star) = fiber.mk a H,
|
||||
rewrite [is_hset.elim H (refl star)] }
|
||||
end
|
||||
|
||||
end unit
|
||||
|
||||
namespace homotopy
|
||||
|
||||
definition is_conn (n : trunc_index) (A : Type) : Type :=
|
||||
|
|
@ -48,7 +19,7 @@ namespace homotopy
|
|||
: is_conn_map n (λx : A, unit.star) → is_conn n A :=
|
||||
begin
|
||||
intro H, unfold is_conn_map at H,
|
||||
rewrite [-(ua (unit.fiber_star_equiv A))],
|
||||
rewrite [-(ua (fiber.fiber_star_equiv A))],
|
||||
exact (H unit.star)
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -45,7 +45,23 @@ namespace fiber
|
|||
|
||||
end fiber
|
||||
|
||||
open function is_equiv is_trunc
|
||||
open unit is_trunc
|
||||
|
||||
namespace fiber
|
||||
|
||||
definition fiber_star_equiv (A : Type) : fiber (λx : A, star) star ≃ A :=
|
||||
begin
|
||||
fapply equiv.MK,
|
||||
{ intro f, cases f with a H, exact a },
|
||||
{ intro a, apply fiber.mk a, reflexivity },
|
||||
{ intro a, reflexivity },
|
||||
{ intro f, cases f with a H, change fiber.mk a (refl star) = fiber.mk a H,
|
||||
rewrite [is_hset.elim H (refl star)] }
|
||||
end
|
||||
|
||||
end fiber
|
||||
|
||||
open function is_equiv
|
||||
|
||||
namespace fiber
|
||||
/- Theorem 4.7.6 -/
|
||||
|
|
|
|||
Loading…
Reference in a new issue