@UrsSchreiber: no update from the library in Paris, but since they were intending to make the thesis publicly available, I feel there is no harm in uploading it to the nLab for the time being.

are multiple ways to represent a single term. Working over a slice is one way to capture the dependency structure, but it is not necessary to do so. Dependency can be captured instead by working in the original category, and identifying dependencies by projecting out of pullbacks. (I feel this comment is probably not very clear, and I really need more space to make it clear.) Perhaps this is a conversation that could be had elsewhere, without MO's limitations, though. (2/2)

To be honest, I think that it is difficult to have this sort of technical discussion in the comments section of MO, and the character limit is going to make it easy to cause undue confusion. Since Andrej Bauer's answer has clarified OP's question, it also doesn't seem so worthwhile to modify mine further; it may be simpler to delete my answer. My general impression, though, is that we are interpreting the semantics of a term in a dependent type theory differently: since categories with finite limits have a lot of redundancy in a certain sense (as some morphisms determine others), there (1/2)

@BartoszMilewski: you can view $\iota$ here as the projection function $\pi_1$ from a pullback. The empty context can be interpreted as a singleton set.

My understanding is that, if $a : A \vdash B(a)\ \mathrm{type}$, then a term $\Gamma \vdash s : B$ can be represented either as a morphism $\Gamma \to B$ in $\mathscr C$ or as a morphism $\Gamma \to \Gamma \times_A B$ in $\mathscr C/\Gamma$, but the two are equivalent by the universal property of the pullback. I agree with the other points, though.