<p>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 <strong>formulated</strong> in HoTT, since it crucially relies on the <em>topology</em> of the space in question, which does not exist for every type!</p>

<p>The primitive notion in HoTT is that of the <em>path space</em> $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.</p>

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

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

<p>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.</p>

<p>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 <a href="http://ncatlab.org/nlab/show/formal+smooth+manifold" rel="nofollow">here</a> and <a href="http://ncatlab.org/nlab/show/cohesive+homotopy+type+theory" rel="nofollow">here</a> (n-Cat Lab).</p>

CC BY-SA 3.0
2015-06-15T21:43:21.253Z
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
CC BY-SA 3.0
2015-06-15T21:35:04.440Z
2015-06-15T21:35:04.440Z
cody
<p>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). </p>

<p>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.</p>

<p>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. </p>

<p>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.</p>

CC BY-SA 3.0
2015-06-11T08:15:26.380Z
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
CC BY-SA 3.0
2015-06-11T01:46:57.467Z
2015-06-11T01:46:57.467Z
Baby Dragon
<p>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.</p>

<p>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 <a href="https://en.wikipedia.org/wiki/Topological_quantum_field_theory" rel="noreferrer">topological quantum field theories</a> only carry homotopy information.</p>

<p>Other questions in manifold theory are exactly whether homotopy equivalence implies isomorphism under certain circumstances, for example the question of <a href="https://en.wikipedia.org/wiki/Homotopy_sphere" rel="noreferrer">homotopy spheres</a>.</p>

<p>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$.</p>

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

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

<p>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?</p>

CC BY-SA 3.0
2015-06-11T13:21:05.040Z
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
CC BY-SA 3.0
2015-06-11T15:46:41.720Z
@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
CC BY-SA 3.0
2015-06-11T15:55:05.643Z
Types in homotopy type theory are like $(\infty, 1)$-objects.
Andrej Bauer
CC BY-SA 3.0
2015-06-11T16:00:03.093Z
@Andrej, so in the $(\infty, 1)$-category of non-extended $n$-cobordisms, the objects  are $(n-1)$-dimensional manifolds, which sounds quite right. I don't think that Lurie defines this category inductively, though.
Turion
CC BY-SA 3.0
2015-06-11T19:13:42.577Z
Your "easier version" makes me suspect that you're missing a bit of the intuition of homotopy type theory.  Simplicial sets play essentially no role inside the theory.  The types of HoTT are "homotopy types" that don't "remember" any information about a simplicial set or topological space that might have been used to present them.  At present in ordinary HoTT we don't even know how to define the homotopy type presented by an internally-defined topological space or simplicial set.  Cohesive homotopy type theory may be a better approach.
Mike Shulman
CC BY-SA 3.0
2015-06-11T21:27:27.380Z
@Mike, oh, I'm surprised. I'm just in the middle of reading the HoTT book and I haven't done any work yet, so naturally I'm lacking intuition. But I would have thought that it's easy to define the category of sets. I've seen implementations of categories and functors. So what's so hard to implement simplicial sets?
Turion
CC BY-SA 3.0
2015-06-12T08:30:53.510Z
@MikeShulman, does that justify asking a new question maybe?
Turion
CC BY-SA 3.0
2015-06-12T21:33:04.513Z
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
CC BY-SA 3.0
2015-06-12T21:37:25.493Z
@Mike, ah, so we're lacking a geometric realisation from simplicial sets to the universe? I guess part of the problem is that it's undecidable what the nondegenerate simplices are
Turion
CC BY-SA 3.0
2015-06-12T22:50:24.487Z
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
CC BY-SA 3.0
2015-06-16T04:24:49.250Z
If you don't find the answer you are looking for here after a few more days, you may want to repost this on [MathOverflow.se].
Kaveh
<homotopy-type-theory>
In homotopy type theory, is there a IsManifold predicate?
Turion
# In homotopy type theory, is there a IsManifold predicate?

(Asked by: username_0 on 2015-06-10)

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](https://en.wikipedia.org/wiki/Topological_quantum_field_theory) 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](https://en.wikipedia.org/wiki/Homotopy_sphere).

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?

**Tags:** homotopy-type-theory
> **Comments:**
> **username_1**: 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?  
> **username_0**: @Andrej, that's probably part of the question. I know that Lurie has a definition of cobordisms as $(\infty, n)$-categories, if that helps.  
> **username_1**: Types in homotopy type theory are like $(\infty, 1)$-objects.  
> **username_0**: @Andrej, so in the $(\infty, 1)$-category of non-extended $n$-cobordisms, the objects  are $(n-1)$-dimensional manifolds, which sounds quite right. I don't think that Lurie defines this category inductively, though.  
> **username_2**: Your "easier version" makes me suspect that you're missing a bit of the intuition of homotopy type theory.  Simplicial sets play essentially no role inside the theory.  The types of HoTT are "homotopy types" that don't "remember" any information about a simplicial set or topological space that might have been used to present them.  At present in ordinary HoTT we don't even know how to define the homotopy type presented by an internally-defined topological space or simplicial set.  Cohesive homotopy type theory may be a better approach.  
> **username_0**: @Mike, oh, I'm surprised. I'm just in the middle of reading the HoTT book and I haven't done any work yet, so naturally I'm lacking intuition. But I would have thought that it's easy to define the category of sets. I've seen implementations of categories and functors. So what's so hard to implement simplicial sets?  
> **username_0**: @MikeShulman, does that justify asking a new question maybe?  
> **username_2**: 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.  
> **username_0**: @Mike, ah, so we're lacking a geometric realisation from simplicial sets to the universe? I guess part of the problem is that it's undecidable what the nondegenerate simplices are  
> **username_2**: 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.  
> **username_3**: If you don't find the answer you are looking for here after a few more days, you may want to repost this on [MathOverflow.se].  

---

## 2 answers

### Answer by username_4 on 2015-06-15. Score: 3

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](http://ncatlab.org/nlab/show/formal+smooth+manifold) and [here](http://ncatlab.org/nlab/show/cohesive+homotopy+type+theory) (n-Cat Lab).

> **Comments:**
> **username_0**: 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...  

---

### Answer by username_5 on 2015-06-11. Score: 0

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.

> **Comments:**
> **username_0**: 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?  

---

