I have trouble understanding precisely how dependent type theories are intepreted in categories (in the most simple case, for example in a locally cartesian closed category). I know that a type in context is morally a bundle over the interpretation of the context, that a term in context is a section, etc.. But the actual interpretation seems only to work if the model (a lccc for example) is replaced by a split equivalent version of itself before hand. Let me cite from Martin Hofmann's 1994 paper On the interpretation of Type Theory in Locally Cartesian Closed Categories.
Interpreting dependent type theory in locally cartesian closed categories (lcccs) and more generally in (non split) fibrational models (...) is an intricate problem. The reason is that in order to interpret terms associated with substitution like pairing for $\Sigma$-types or applications for $\Pi$-types one needs a semantical equivalent to syntactic substitution. To clarify the issue (...)
And Martin Hofmann then proceeds to clarify the issue. The paper also contains a solution to the coherence problem, but it makes the interpretation process much harder to understand. I am not able to use the CwA in Hofmann's paper to quickly translate between type theoretic and categorical statements in the way I can for statements written in simply-typed first-order logic.
The paper is from 1994, and people (actual categorical logicians) which I met this week told me that today many effective shortcuts and techniques exist to deal with coherence problems, and that they are often unpublished. They haven't been able to tell me if the specific problem (from the paper I quoted above) is still a problem, and what its most effective solution is, but they encouraged me to ask here. I am afraid of going through a lot of technical details for no good reason.
What is the most effective and modern way to deal with coherence problems in the interpretation of dependent type theory? Where can I read about it?
Is the paper by Martin Hofmann outdated, or do I just have to try harder?