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