Reading about the categorical models of dependent type theory (DTT) I have faced many articles pointing out the coherence problem for the interpretation of DTT in locally cartesian closed categories (LCCC).
As Awodey and Rabe point out briefly (2011), "LCC categories interpret contexts $\Gamma$ as objects $[[\Gamma]]$, types in context $\Gamma$ as objects in the slice category over $[[Γ]]$, substitution as pullback, and dependent sum and product as left and right adjoint to pullback".
This is the interpretation that Seely gave in his 1984's article. The subtlety here is that it uses pullbacks to interpret substitution and, due to the pseudo-functoriality of pullbacks, the interpretation of a type declaration is not strict when you apply the substitution rule but is given only up to isomorphism.
There are other situations where we interpret things using pullbacks. For instance, in categorical logic, a relation symbol $R \rightarrowtail A_1,\dots,A_n$ is interpreted as a pullback, as well as the conjunction $\phi\land\psi$ of two formulas (like Definition D1.2.6 of the Elephant book). But in such case, substitution is interpreted as composition.
Even in DTT there are other constructions which are interpreted as pullbacks. Look at Definition D4.4.3(a) of the Elephant book regarding the interpretation of the Weakening Rule:
[…] say $\Gamma = (x_1: A_1),\dots,(x_n: A_n)$ and $\Delta = (x_1: A_1),\dots,(x_m: A_m)$ where $m > n$, then the composite of the morphisms which lie in the interpretation of $A$ but not in that of $\Gamma$ is a morphism $M\Delta \rightarrow M\Gamma$ in $C$, and we obtain the interpretation of a type or term declaration $\theta$ in the context $M\Gamma$ simply by pulling back its interpretation in the context $\Gamma$ along this morphism.[…]
Note that, in the case presented above, the resulting object associated with the declaration $\theta$ after applying the Weakening Rule is not even necessarily isomorphic to its interpretation in the premise.
My question is: why is coherence so important in respect to substituion?
And why we don't bother about coherence in regards to other rules (I have never even seen this problem beeing stated for categorical logic, apart from DTT)? Am I missing something? Did I understand something wrong?
Best Answer
The usual way to prove that a given category is a model of some syntax is to show that it belongs to some category of structured categories and that the syntax defines the initial object of that category. But since substitution in syntax is strict, the obvious category in which it defines the initial object consists of categorical structures with strict substitution. Thus, in order to interpret syntax in a category without strictly associative pullbacks, one needs a coherence theorem to replace the latter by something that does have strict substitutions.
The reason this problem doesn't arise until you get to dependent type theory is that for first-order logic you can take the quotient by isomorphisms, interpreting predicates by isomorphism classes of monomorphisms rather than single ones. This produces a fibration of posets (not just preorders) with strictly associative substitution.
I am not sure what you mean by "substitution is interpreted by composition". If your category is an elementary topos, then you can also choose to interpret predicates by maps into the subobject classifier, in which case substitution is indeed interpreted by composition, which is strictly associative. But for more general categories this is not possible.
Note also that weakening is really just a special case of substitution, in the broad sense of substitution along a map of contexts.
Finally, as you may have noticed, the section on dependent type theory in Sketches of an Elephant is rather, well, sketchy. In particular, it ignores this issue of coherence.