Spheres
Content created by Jonathan Prieto-Cubides, Fredrik Bakke, Egbert Rijke, Raymond Baker and maybemabeline.
Created on 2023-01-28.
Last modified on 2023-09-16.
module synthetic-homotopy-theory.spheres where
Imports
open import elementary-number-theory.natural-numbers open import foundation.identity-types open import foundation.universe-levels open import synthetic-homotopy-theory.suspensions-of-types open import univalent-combinatorics.standard-finite-types
Idea
The spheres are defined as iterated suspensions of Fin 2
.
Definition
sphere : ℕ → UU lzero sphere zero-ℕ = Fin 2 sphere (succ-ℕ n) = suspension (sphere n) north-sphere : (n : ℕ) → sphere n north-sphere zero-ℕ = zero-Fin 1 north-sphere (succ-ℕ n) = north-suspension south-sphere : (n : ℕ) → sphere n south-sphere zero-ℕ = one-Fin 1 south-sphere (succ-ℕ n) = south-suspension meridian-sphere : (n : ℕ) → sphere n → north-sphere (succ-ℕ n) = south-sphere (succ-ℕ n) meridian-sphere n = meridian-suspension
Recent changes
- 2023-09-16. maybemabeline and Egbert Rijke. Equivalence between the first sphere and the circle (#776).
- 2023-08-28. Raymond Baker and Fredrik Bakke. Suspension reorganization (#700).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490).