No.

The fact that equalities corresponding to beta reduction, etc. are validated is not "an accident of implementation choices".

It is a consequences of the fact that standard type constructors (function space, products, ...) are interpreted by their native meaning in the meta-level.

For example, if the metatheory is again type theory, and interpretation is done by recursion over the universes of object types, reifying all type constructors by themselves (like in an inductive-recursive universe), then all conversions in the object language will again be valid in the metatheory, and coherence issues won't arise.

I suspect that (sufficiently split) categorical models could also be presented this way, but it might be less natural because equality of types would then have to refer to (actual) equality of objects.

Cheers,

Andrew