Let $X : Type$ in a type theory $T$ interpreting synthetic differential geometry - I don't believe it should matter too much if we have smooth stuff on hand except maybe at the end of this line, but we can have it for niceness' sake. An $n$-dimensional premanifold is defined in the Agda-UniMath library as a (homotopy) type that can locally be constructed by gluing a (homotopy) $n$-sphere to a suitable complement of each $x : X$.
- Is it a property when $X$ is (equivalent to) a manifold? Real or complex, though real is more important for:
- In the classical theory of manifolds it is not the case that every manifold has a smooth structure so we would not expect to be able to find a tangent sphere of each point, but a lot of constructive math to my mind is about everything being "potentially continuous" or even "potentially smooth", so this motivates the question: when $T$ is a cohesive type theory (with shape modality $\int$) and $X$ is a manifold (assuming 1), is it so, or at least consistent, that $\int X$ is a premanifold?
