# In homotopy type theory, is there a IsManifold predicate?

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?

• In homotopy type theory the types should be thought of as homotopy types. Thus you would need a homotopy-theoretic characterization of those homotopy types that arise as the homotopy types of manifolds. Is there one? – Andrej Bauer Jun 11 '15 at 13:21
• @Andrej, that's probably part of the question. I know that Lurie has a definition of cobordisms as $(\infty, n)$-categories, if that helps. – Turion Jun 11 '15 at 15:46
• Types in homotopy type theory are like $(\infty, 1)$-objects. – Andrej Bauer Jun 11 '15 at 15:55
• I didn't say we couldn't define simplicial sets, I said that we don't know how to define the homotopy type presented by a simplicial set. The reason is that it would require adding paths of all dimensions coming from the simplices of all dimensions, and we don't know how to do that in general with HITs that can have only finitely many constructors. – Mike Shulman Jun 12 '15 at 21:33
• Yes, a geometric realization is what we don't have yet. I don't think degeneracy is the issue here, though; you should be able to ignore the degeneracies and still get the right homotopy type of a geometric realization. The problem is infinity. – Mike Shulman Jun 12 '15 at 22:50

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).

• I see. Some important buzz words seem to be "cohesive $(\infty, 1)$-topos" and "smooth $\infty$-groupoid". Maybe the latter is somehow what I'm after... – Turion Jun 15 '15 at 21:43

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.

• Sure, that's why I asked whether one could define it in such a way, that $\text{IsManifold}(A)$ is the type of all manifolds which are homotopy equivalent to $A$. If I want to define manifolds up to isomorphism, I need to encode them in something else than types. How do I define manifolds in term of simplicial sets? – Turion Jun 11 '15 at 8:15