In homotopy type theory, is there a IsManifold predicate?
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).