cubical
cubical copied to clipboard
agda
Some properties of connected spaces
I proved some properties of connected spaces while working on a project; I figured they might be a good fit for this library.
This pull requests contains:
- proofs that being connected is a proposition
- a proof that k-connected k-types are contractible
- a proof of Corollary 7.5.9 in the HoTT book: A type is n-connected iff every map to n-types is constant (896a7e46b5c720c4b8bf8917c329a27107241360)
- a slightly strengthened version of the "only if"-part of the above: A type A is n-connected if the map
λ b a → b : B → (A → B)has a section for any n-type B. (ab12f081184a82b8c923d890aaa06624b6be3d74) - a proof that all loop spaces of k+2-connected spaces are merely equivalent
- a recursive characterization of connectivity similar to Exercise 7.6 of the HoTT book: A type is (k+1)-connected iff it is (k+1)-inhabited and has k-connected paths (c50abab32341feb5f16acec7008ff66442322c21)
a result that I found useful is that a pointed type (X , a) is connected iff (x : X) -> || x = a ||
a result that I found useful is that a pointed type (X , a) is connected iff
(x : X) -> || x = a ||
Check out fdaa6cf7a74a2a23695283c352e524511e0cfdbb. Is this what you had in mind?
