The categorical semantics of a dependent type theory is normally described as a CwA/CwF/CompCat/etc. and in these models, we can talk about propositional equality by interpreting an 'identity type'. So, what about judgmental equality?
My little analysis: I've heard people saying 'two terms are equal if they are interpreted as the same morphism (or uniquely isomorphic terms)'. This is not what I'm looking for. Take a contextual category as an example: if the base category $\cal C$ has all pullbacks and a terminal object, we can define in it the notion of equalizers, which interprets the extensional identity type. With that type, the definitional equality becomes propositional equality (is that true? I'm not sure -- please correct me if I'm wrong!). But there is certainly a difference in the type theory (where we do not always identify definitional equality and propositional ones).
So, what are definitional equalities in the categorical semantics?