The infinite complex projective space

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-05-16.
Last modified on 2023-09-10.

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

ℂP∞ as the 2-truncation of the 2-sphere

This remains to be defined. #742

Recent changes