Define ℝP∞ (#1431)

Author: fredrik-bakke

references.bib

@@ -140,6 +140,18 @@ @phdthesis{Booij20PhD
   school        = {University of Birmingham},
 }
 
+@incollection{BR17,
+  title         = {The real projective spaces in homotopy type theory},
+  author        = {Buchholtz, Ulrik and Rijke, Egbert},
+  year          = 2017,
+  booktitle     = {2017 32nd {A}nnual {ACM}/{IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS})},
+  publisher     = {IEEE, [Piscataway], NJ},
+  pages         = 8,
+  isbn          = {978-1-5090-3018-7},
+  mrclass       = {55U40 (03B15 03G30 18G55)},
+  mrnumber      = 3776972,
+}
+
 @book{BSCS05,
   title         = {Absztrakt algebrai feladatok},
   author        = {Bálintné Szendrei, Mária and Czédli, Gábor and Szendrei, Ágnes},

src/synthetic-homotopy-theory.lagda.md

@@ -80,6 +80,7 @@ open import synthetic-homotopy-theory.identity-systems-descent-data-pushouts pub
 open import synthetic-homotopy-theory.induction-principle-pushouts public
 open import synthetic-homotopy-theory.infinite-complex-projective-space public
 open import synthetic-homotopy-theory.infinite-cyclic-types public
+open import synthetic-homotopy-theory.infinite-real-projective-space public
 open import synthetic-homotopy-theory.interval-type public
 open import synthetic-homotopy-theory.iterated-loop-spaces public
 open import synthetic-homotopy-theory.iterated-suspensions-of-pointed-types public

src/synthetic-homotopy-theory/infinite-complex-projective-space.lagda.md

@@ -1,4 +1,4 @@
-# The infinite complex projective space
+# The infinite dimensional complex projective space
 
 ```agda
 module synthetic-homotopy-theory.infinite-complex-projective-space where
@@ -34,3 +34,7 @@ pr2 point-ℂP∞ = unit-trunc-Set id-equiv
 
 This remains to be defined.
 [#742](https://github.com/UniMath/agda-unimath/issues/742)
+
+## See also
+
+- [The infinite dimensional real projective space](synthetic-homotopy-theory.infinite-real-projective-space.md)

src/synthetic-homotopy-theory/infinite-real-projective-space.lagda.md

@@ -0,0 +1,56 @@
+# The infinite dimensional real projective space
+
+```agda
+module synthetic-homotopy-theory.infinite-real-projective-space where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import group-theory.symmetric-concrete-groups
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+The {{#concept "infinite dimensional real projective space" Agda=ℝP∞}} `ℝP∞` is
+the classifying space of the
+[symmetric group](group-theory.symmetric-concrete-groups.md) on a
+[two-element type](univalent-combinatorics.2-element-types.md).
+
+## Definitions
+
+### As the delooping of a two-element type
+
+```agda
+ℝP∞ : UU (lsuc lzero)
+ℝP∞ = classifying-type-symmetric-Concrete-Group (Fin-Set 2)
+
+point-ℝP∞ : ℝP∞
+point-ℝP∞ = shape-symmetric-Concrete-Group (Fin-Set 2)
+```
+
+### As the sequential colimit of the finite dimensional real projective spaces
+
+The infinite dimensional real projective space `ℝP∞` may be realized as a
+[sequential colimit](synthetic-homotopy-theory.sequential-colimits.md) of finite
+dimensional real projective spaces, see Section IV {{#cite BR17}}.
+
+```text
+  ℝP⁻¹ ──→ ℝP⁰ ──→ ℝP¹ ──→ ℝP² ──→ ⋯ ──→ ℝPⁿ ──→ ℝPⁿ⁺¹ ──→ ⋯ ──→ ℝP∞
+```
+
+> This remains to be formalized.
+
+## References
+
+{{#bibliography}}
+
+## See also
+
+- [The infinite dimensional complex projective space](synthetic-homotopy-theory.infinite-complex-projective-space.md)