In homotopy type theory, is there a IsManifold predicate?

Question

Any type $A: \mathcal{U}$ can be thought of as a homotopy type, or a sufficiently nice topological space up to homotopy equivalence. Now, manifolds are topological spaces with some extra structure.

Some questions in manifold theory are still interesting up to homotopy, for example 2-manifolds are isomorphic whenever they are homotopy equivalent, and it is suspected that 4d extended topological quantum field theories only carry homotopy information.

Other questions in manifold theory are exactly whether homotopy equivalence implies isomorphism under certain circumstances, for example the question of homotopy spheres.

So I'm wondering whether it's possible to define a predicate like $\text{IsManifold}: \mathcal{U} \to \mathcal{U}$, such that $\text{IsManifold}(A)$ is inhabited by possibilities of defining a manifold that is homotopy equivalent to $A$.

As an application, we can define any homotopy invariant of manifolds (like the genus of surfaces) on types satisfying this predicate.

Since in all generality, this is probably too much to ask for a start, so here is an easier version:

Surely it is feasible to define a type of simplicial sets $\text{sSet}$. Can we define a proposition $\text{IsManifold}': \text{sSet} \to \text{Bool}$ that decides whether the realisation of a given simplicial set is a manifold?

Answer 1

I'm afraid I don't have a clear answer to your question. As I imagine you know, the basic definition of being a manifold cannot even be formulated in HoTT, since it crucially relies on the topology of the space in question, which does not exist for every type!

The primitive notion in HoTT is that of the path space $I_X$ of a type $X$. But, as far as I know, this does not in general define a topology over $X$, which is required in the usual definition of manifolds.

Another point is the property vs structure problem that seems to underly your question. It is certainly possible to define a manifold structure over a type: a manifold is a tuple $(X, T, A)$ where $X$ is a type, $T$ is a topology over $X$, and $A$ is an atlas, etc.

Given such a structure (which may include proofs of the various properties that underlie the structure), you can of course ask whether it is homotopy equivalent to another $Y$, as a homotopy type. This means that being a manifold is first defined as being a structure, and only then can you ask the question whether another type has the property of being homotopy equivalent to some manifold.

This is just what you do in "ordinary" math though, and doesn't seem to nicely use the synthetic properties of HoTT. As far as I can tell, the machinery required to talk about manifolds in a synthetic way is still being worked out, and certainly hasn't been well explored yet in any of the current (semi-)implementations of HoTT. This is an exiting avenue of research though. It seems to be structural, and thus requires adding constructs to "ordinary" HoTT.

The most notable proponent of this approach is Urs Shreiber (though Mike Shulman certainly is a close second, and might be able to give a more informed answer), and some pointers can be found here and here (n-Cat Lab).

Answer 2

The usual way that manifold theory gets turned into homotopy theory is transformative in nature. What I mean by this is that it is often possible to phrase questions of manifold theory in homotopy theory. That is not to say that the new objects of homotopy theory are necessarily manifolds (sometimes they are, sometimes they are not).

Homotopy type theory on the other hand declares that "homotopic objects are equal". Now the problem with an isManifold predicate is that it is not a homotopy invariant notion. This means that you would have two equal (homotopic) objects, one which is a manifold, and the other which is not. So in that sense it is not a well define predicate. Again that is not to say that there is not an encoding of certain questions of manifold theory, but the underlying objects are no longer manifolds.

To see that being a manifold is not a homotopy invariant notion, take any manifold, and add a whisker that grows out of a point (in the case of a sphere, you get something that looks like a ballon with a string tied to it). At the point where the whisker is attached, the space loses the property of being locally Euclidian.

Note that you can define a notion of a manifold in simplicial sets. They would look something like PL manifolds. The Same problem will occur that there will be equal (homotopic) simplicial sets that are not manifolds.