The infinite complex projective space
module synthetic-homotopy-theory.infinite-complex-projective-space where
Imports
open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.set-truncations open import foundation.universe-levels open import synthetic-homotopy-theory.circle
Definitions
ℂP∞ as the 1-connected component of the universe at the circle
ℂP∞ : UU (lsuc lzero) ℂP∞ = Σ (UU lzero) (λ X → type-trunc-Set (𝕊¹ ≃ X)) point-ℂP∞ : ℂP∞ pr1 point-ℂP∞ = 𝕊¹ pr2 point-ℂP∞ = unit-trunc-Set id-equiv