As you conjecture, MLTT with equality reflection can’t distinguish between isomorphic types.
Precisely, let MLTT[X] be the extension of MLTT by a single closed base type X.
Suppose \C is a model of MLTT — presented as a CwA with appropriate extra logical structure — and A, B are two isomorphic types in it, over the empty context. So A, B induce two interpretations of MLTT[X] in \C.
Then there’s a CwA \C^\iso, with the category of isomorphisms in \C, and with a type over an iso Г1 <~> Г2 being a pair of types A1, A2 over Г1, Г2 that correspond under reindexing along the isomorphism.
Now I claim this carries suitable structure to again model MLTT[X], and furthermore (importantly) such that the two projection maps \C^\iso —> \C both preserve all the logical structure. For most logical type-formers (Pi’s, Sigma’s, etc), the structure is by showing that these type-formers are provably functorial in isomorphisms. (This uses the equality reflection.) For the universe(s), this just uses the identity iso on the universe(s) of \C. The base type X, we model by the given isomorphism A <~> B.
So this induces an interpretation of MLTT[X] in \C^\iso, whose two projections to \C are the two original interpretations in \C.
In particular, if P is any type in MLTT[X] — i.e. a property of an arbitrary type definable in MLTT — then its interpretation in \C^\iso is an isomorphism P[A] <~> P[B]. I think this is a reasonable positive answer to your question?
I don’t remember anywhere this construction appears in the literature, but I’ve always assumed that it has been noted before. (Actually, I’d be very glad to hear a reference if anyone remembers seeing this somewhere, even if only in folklore not in print.) Without identity reflection, it no longer works — since one doesn’t know that the logical structure in \C respects isomorphisms between types — but essentially the same approach works once one replaces isomorphisms by equivalences. This is in the work of Chris Kapulkin’s and mine that I presented in Bonn in February, which we hope to have written up very soon…
Best,
–Peter.