Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-17.
Last modified on 2024-01-09.

module synthetic-homotopy-theory.premanifolds where
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


An n-dimensional premanifold is a type M such that every element x : M comes equipped with a tangent n-sphere.



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)

  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) 
      ( inclusion-tangent-sphere-Premanifold x)
      ( terminal-map (type-tangent-sphere-Premanifold x))
      ( inclusion-complement-Premanifold x)
      ( point x)
  coherence-square-Premanifold x =
    coherence-square-has-tangent-sphere n (pr2 M x)

  cocone-Premanifold :
    (x : type-Premanifold) 
      ( terminal-map (type-tangent-sphere-Premanifold x))
      ( inclusion-tangent-sphere-Premanifold x)
      ( type-Premanifold)
  cocone-Premanifold x =
    cocone-has-tangent-sphere n (pr2 M x)

  is-pushout-Premanifold :
    (x : type-Premanifold) 
      ( terminal-map (type-tangent-sphere-Premanifold x))
      ( inclusion-tangent-sphere-Premanifold x)
      ( cocone-Premanifold x)
  is-pushout-Premanifold x =
    is-pushout-has-tangent-sphere n (pr2 M x)

Recent changes