agda-unimath icon indicating copy to clipboard operation
agda-unimath copied to clipboard

Published 20 hours ago • verified publisher icon UniMath

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

Open fredrik-bakke opened this issue 1 year ago • 0 comments

The following is waiting to be defined in synthetic-homotopy-theory.infinite-complex-projective-space:

  • [ ] ℂP∞ as the 2-truncation of the 2-sphere

fredrik-bakke avatar Sep 10 '23 17:09 fredrik-bakke