Tangent spheres (#853)

This PR defines what it means for a point in a type to have a tangent
sphere. It also defines the notion of premanifold, which are types
equipped with the structure that every point comes equipped with a
tangent sphere.

src/synthetic-homotopy-theory.lagda.md

@@ -53,10 +53,12 @@ open import synthetic-homotopy-theory.join-powers-of-types public
 open import synthetic-homotopy-theory.joins-of-types public
 open import synthetic-homotopy-theory.loop-spaces public
 open import synthetic-homotopy-theory.maps-of-prespectra public
+open import synthetic-homotopy-theory.mere-spheres public
 open import synthetic-homotopy-theory.morphisms-descent-data-circle public
 open import synthetic-homotopy-theory.multiplication-circle public
 open import synthetic-homotopy-theory.plus-principle public
 open import synthetic-homotopy-theory.powers-of-loops public
+open import synthetic-homotopy-theory.premanifolds public
 open import synthetic-homotopy-theory.prespectra public
 open import synthetic-homotopy-theory.pullback-property-pushouts public
 open import synthetic-homotopy-theory.pushouts public
@@ -70,6 +72,7 @@ open import synthetic-homotopy-theory.suspension-prespectra public
 open import synthetic-homotopy-theory.suspension-structures public
 open import synthetic-homotopy-theory.suspensions-of-pointed-types public
 open import synthetic-homotopy-theory.suspensions-of-types public
+open import synthetic-homotopy-theory.tangent-spheres public
 open import synthetic-homotopy-theory.triple-loop-spaces public
 open import synthetic-homotopy-theory.universal-cover-circle public
 open import synthetic-homotopy-theory.universal-property-circle public

src/synthetic-homotopy-theory/mere-spheres.lagda.md

@@ -0,0 +1,62 @@
+# Mere spheres
+
+```agda
+module synthetic-homotopy-theory.mere-spheres where
+```
+
+<details></summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.mere-equivalences
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.spheres
+```
+
+</details>
+
+## Idea
+
+A **mere `n`-sphere** is a type `X` that is
+[merely equivalent](foundation.mere-equivalences.md) to the
+[`n`-sphere](synthetic-homotopy-theory.spheres.md).
+
+## Definitions
+
+### The predicate of being a mere `n`-sphere
+
+```agda
+module _
+  {l : Level} (n : ℕ) (X : UU l)
+  where
+
+  is-mere-sphere-Prop : Prop l
+  is-mere-sphere-Prop = mere-equiv-Prop (sphere n) X
+
+  is-mere-sphere : UU l
+  is-mere-sphere = type-Prop is-mere-sphere-Prop
+
+  is-prop-is-mere-sphere : is-prop is-mere-sphere
+  is-prop-is-mere-sphere = is-prop-type-Prop is-mere-sphere-Prop
+```
+
+### Mere spheres
+
+```agda
+mere-sphere : (l : Level) (n : ℕ) → UU (lsuc l)
+mere-sphere l n = Σ (UU l) (is-mere-sphere n)
+
+module _
+  {l : Level} (n : ℕ) (X : mere-sphere l n)
+  where
+
+  type-mere-sphere : UU l
+  type-mere-sphere = pr1 X
+
+  mere-equiv-mere-sphere : mere-equiv (sphere n) type-mere-sphere
+  mere-equiv-mere-sphere = pr2 X
+```

src/synthetic-homotopy-theory/premanifolds.lagda.md

@@ -0,0 +1,104 @@
+# Premanifolds
+
+```agda
+module synthetic-homotopy-theory.premanifolds where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.mere-equivalences
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.mere-spheres
+open import synthetic-homotopy-theory.pushouts
+open import synthetic-homotopy-theory.spheres
+open import synthetic-homotopy-theory.tangent-spheres
+```
+
+</details>
+
+## Idea
+
+An **`n`-dimensional premanifold** is a type `M` such that every element `x : M`
+comes equipped with a
+[tangent `n`-sphere](synthetic-homotopy-theory.tangent-spheres.md).
+
+## Definitions
+
+### Premanifolds
+
+```agda
+Premanifold : (l : Level) (n : ℕ) → UU (lsuc l)
+Premanifold l n = Σ (UU l) (λ M → (x : M) → has-tangent-sphere n x)
+
+module _
+  {l : Level} (n : ℕ) (M : Premanifold l n)
+  where
+
+  type-Premanifold : UU l
+  type-Premanifold = pr1 M
+
+  tangent-sphere-Premanifold : (x : type-Premanifold) → mere-sphere lzero n
+  tangent-sphere-Premanifold x =
+    tangent-sphere-has-tangent-sphere n (pr2 M x)
+
+  type-tangent-sphere-Premanifold : (x : type-Premanifold) → UU lzero
+  type-tangent-sphere-Premanifold x =
+    type-tangent-sphere-has-tangent-sphere n (pr2 M x)
+
+  mere-equiv-tangent-sphere-Premanifold :
+    (x : type-Premanifold) →
+    mere-equiv (sphere n) (type-tangent-sphere-Premanifold x)
+  mere-equiv-tangent-sphere-Premanifold x =
+    mere-equiv-tangent-sphere-has-tangent-sphere n (pr2 M x)
+
+  complement-Premanifold : (x : type-Premanifold) → UU l
+  complement-Premanifold x =
+    complement-has-tangent-sphere n (pr2 M x)
+
+  inclusion-tangent-sphere-Premanifold :
+    (x : type-Premanifold) →
+    type-tangent-sphere-Premanifold x → complement-Premanifold x
+  inclusion-tangent-sphere-Premanifold x =
+    inclusion-tangent-sphere-has-tangent-sphere n (pr2 M x)
+
+  inclusion-complement-Premanifold :
+    (x : type-Premanifold) → complement-Premanifold x → type-Premanifold
+  inclusion-complement-Premanifold x =
+    inclusion-complement-has-tangent-sphere n (pr2 M x)
+
+  coherence-square-Premanifold :
+    (x : type-Premanifold) →
+    coherence-square-maps
+      ( inclusion-tangent-sphere-Premanifold x)
+      ( terminal-map)
+      ( inclusion-complement-Premanifold x)
+      ( point x)
+  coherence-square-Premanifold x =
+    coherence-square-has-tangent-sphere n (pr2 M x)
+
+  cocone-Premanifold :
+    (x : type-Premanifold) →
+    cocone
+      ( terminal-map)
+      ( inclusion-tangent-sphere-Premanifold x)
+      ( type-Premanifold)
+  cocone-Premanifold x =
+    cocone-has-tangent-sphere n (pr2 M x)
+
+  is-pushout-Premanifold :
+    (x : type-Premanifold) →
+    is-pushout
+      ( terminal-map)
+      ( inclusion-tangent-sphere-Premanifold x)
+      ( cocone-Premanifold x)
+  is-pushout-Premanifold x =
+    is-pushout-has-tangent-sphere n (pr2 M x)
+```

src/synthetic-homotopy-theory/tangent-spheres.lagda.md

@@ -0,0 +1,126 @@
+# Tangent spheres
+
+```agda
+module synthetic-homotopy-theory.tangent-spheres where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.mere-equivalences
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.mere-spheres
+open import synthetic-homotopy-theory.pushouts
+open import synthetic-homotopy-theory.spheres
+```
+
+</details>
+
+## Idea
+
+Consider a type `X` and a point `x : X`. We say that `x` **has a tangent
+`n`-sphere** if we can construct the following data:
+
+- A [mere sphere](synthetic-homotopy-theory.mere-spheres.md) `T`, which we also
+  refer to as the **tangent sphere** of `x`.
+- A type `C`, which we call the **complement** of `x`.
+- A map `j : T → C` including the tangent sphere into the complement.
+- A map `i : C → X` including the complement into the type `X`.
+- A [homotopy](foundation-core.homotopies.md) witnessing that the square
+  ```text
+        j
+    T -----> C
+    |        |
+    |        | i
+    V        V
+    1 -----> X
+        x
+  ```
+  [commutes](foundation.commuting-squares-of-maps.md), and is a
+  [pushout](synthetic-homotopy-theory.pushouts.md).
+
+In other words, a tangent `n`-sphere at a point `x` consistst of a mere sphere
+and a complement such that the space `X` can be reconstructed by attaching the
+point to the complement via the inclusion of the tangent sphere into the
+complement.
+
+## Definitions
+
+### The predicate of having a tangent sphere
+
+```agda
+module _
+  {l : Level} (n : ℕ) {X : UU l} (x : X)
+  where
+
+  has-tangent-sphere : UU (lsuc l)
+  has-tangent-sphere =
+    Σ ( mere-sphere lzero n)
+      ( λ T →
+        Σ ( UU l)
+          ( λ C →
+            Σ ( type-mere-sphere n T → C)
+              ( λ j →
+                Σ ( C → X)
+                  ( λ i →
+                    Σ ( coherence-square-maps j terminal-map i (point x))
+                      ( λ H →
+                        is-pushout terminal-map j (point x , i , H))))))
+
+module _
+  {l : Level} (n : ℕ) {X : UU l} {x : X} (T : has-tangent-sphere n x)
+  where
+
+  tangent-sphere-has-tangent-sphere : mere-sphere lzero n
+  tangent-sphere-has-tangent-sphere = pr1 T
+
+  type-tangent-sphere-has-tangent-sphere : UU lzero
+  type-tangent-sphere-has-tangent-sphere =
+    type-mere-sphere n tangent-sphere-has-tangent-sphere
+
+  mere-equiv-tangent-sphere-has-tangent-sphere :
+    mere-equiv (sphere n) type-tangent-sphere-has-tangent-sphere
+  mere-equiv-tangent-sphere-has-tangent-sphere =
+    mere-equiv-mere-sphere n tangent-sphere-has-tangent-sphere
+
+  complement-has-tangent-sphere : UU l
+  complement-has-tangent-sphere = pr1 (pr2 T)
+
+  inclusion-tangent-sphere-has-tangent-sphere :
+    type-tangent-sphere-has-tangent-sphere → complement-has-tangent-sphere
+  inclusion-tangent-sphere-has-tangent-sphere = pr1 (pr2 (pr2 T))
+
+  inclusion-complement-has-tangent-sphere :
+    complement-has-tangent-sphere → X
+  inclusion-complement-has-tangent-sphere = pr1 (pr2 (pr2 (pr2 T)))
+
+  coherence-square-has-tangent-sphere :
+    coherence-square-maps
+      ( inclusion-tangent-sphere-has-tangent-sphere)
+      ( terminal-map)
+      ( inclusion-complement-has-tangent-sphere)
+      ( point x)
+  coherence-square-has-tangent-sphere =
+    pr1 (pr2 (pr2 (pr2 (pr2 T))))
+
+  cocone-has-tangent-sphere :
+    cocone terminal-map inclusion-tangent-sphere-has-tangent-sphere X
+  pr1 cocone-has-tangent-sphere = point x
+  pr1 (pr2 cocone-has-tangent-sphere) = inclusion-complement-has-tangent-sphere
+  pr2 (pr2 cocone-has-tangent-sphere) = coherence-square-has-tangent-sphere
+
+  is-pushout-has-tangent-sphere :
+    is-pushout
+      ( terminal-map)
+      ( inclusion-tangent-sphere-has-tangent-sphere)
+      ( cocone-has-tangent-sphere)
+  is-pushout-has-tangent-sphere =
+    pr2 (pr2 (pr2 (pr2 (pr2 T))))
+```