Hi Matt,
I should point out that when I say "a type theory" I mean an ordinary dependently typed language, without any strict equalities or 2-levelness. Any such theory has only (dependent) types and terms and usual structural rules.
Any "coherence problem" is solved by simply adding an infinite tower of terms. For example, in MLTT, if f : A -> B -> C, you can define function swap(f) = \x y -> f y x : B -> A -> C. Then swap \circ swap = id definitionally. Of course, you cannot have such a definitional equality in Q(MLTT), but instead you have a propositional equality p : Id(swap \circ swap, id) and also an infinite tower of terms, which assure that p is coherent. Any rule that holds definitionally in MLTT will be true in Q(MLTT) propositionally.