Substitution is Pullback I've read here,
here
and here about how to interpret pullbacks as the substitution of a term into a predicate or dependent type, such as $y:C⊢B(f(y)):Type$ being the pullback of the function $y:C⊢f(y):A$ and predicate $x:A⊢B(x): Type$.
What I do not understand is that all interpretations require two different "kinds" of arrows: one is a vanilla function, the other a predicate/dependent type. When I look at the starting diagram $A \rightarrow_f C \leftarrow_g B$ for a pullback, I just see two arrows $f$ and $g$.
I initially thought that functions and predicates/dependent types are actually interchangeable. For example, $y:Nat⊢Vector(y):Type$ is equivalent to $y:Vector⊢length(y):Nat$.
My issue then is that a pullback can be expressed in two ways; to re-use the above example, the pullback is both $y:C⊢B(f(y)):Type$ and $y:B⊢C(g(y)):Type$ (where $g$ is defined in the equivalence $x:A⊢B(x): Type \equiv x:B⊢g(x):A$). How to reconcile these two and prove equality?
Thanks  
 A: I think you are a bit confused about the whole interpretation of judgments as objects and arrows. Let me try to make it clearer.
Suppose $\vdash C : \mathit{Type}$ and $\vdash A : \mathit{Type}$ are valid judgments. Their interpretations are respectively the objects $C$ and $A$.
Then we can form the judgment $y : C \vdash A : \mathit{Type}$. Since the context contains the variable $y : C$, its interpretation is an arrow with codomain $C$. The domain is the object that corresponds to the judgment $\vdash \Sigma_{y : C}\, A : \mathit{Type}$, i.e. the product $C \times A$. Therefore the interpretation is the projection $\pi_1\colon C \times A \to C$. Of course, we also have the projection $\pi_2 \colon C \times A \to A$.
Then, we suppose $y : C \vdash f(y) : A$ is a valid judgment. Its interpretation is an arrow $f \colon C \to C \times A$ that is a section of $\pi_1 \colon C \times A \to C$, i.e. $\pi_1 \, f = 1_C$.
Finally, suppose $x : A \vdash B(x) : \mathit{Type}$ is a valid judgment. Since the context contains the variable $x : A$, its interpretation is an arrow with codomain $A$. The domain is the object that corresponds to the judgment $\vdash \Sigma_{x : A}\, B(x) : \mathit{Type}$, that we shall denote by $\Sigma_A\, B$. Then the interpretation is the projection $\pi_1 \colon \Sigma_A\, B \to A$.
Now, we are interested in the arrows $\pi_2 \, f \colon C \to A$ and $\pi_1 \colon \Sigma_A\, B \to A$. If we form the pullback of these two arrows we get an object $\Sigma_C\, f^* B$ together with two morphisms $\pi_1\colon \Sigma_C\, f^* B \to C$ and $h\colon \Sigma_C\, f^* B \to \Sigma_A\, B$ satisfying the universal property.
$\pi_1\colon \Sigma_C\, f^* B \to C$ corresponds to the judgment $y : C \vdash B(f(y)) : \mathit{Type}$. It is the pullback of $\pi_1 \colon \Sigma_A\, B \to A$ along $\pi_2\, f$ and indeed it corresponds to the substitution into $x: A \vdash B(x) : \mathit{Type}$.
$h\colon \Sigma_C\, f^* B \to \Sigma_A\, B$ corresponds to the judgment $z : \Sigma_{y: C}\, B(f(y)) \vdash \langle f(\pi_1(z)), \pi_2(z)) \rangle : \Sigma_{x: A}\, B(x)$. It is the pullback of $\pi_2\, f$ along $\pi_1$ and indeed it corresponds to the weakening of the judgment $y : C \vdash f(y) : A$ with respect to the judgment $x : A \vdash B(x) : \mathit{Type}$, since it contains the void information that if $z : \Sigma_{y: C}\, B(f(y))$ then $\pi_2 (z) : B(f(\pi_1(z)))$.
