nLab
substitution natural deduction - table

	type theory	category theory
	syntax	semantics
	natural deduction	universal construction
	substitution…………………….	pullback
	$\frac{x_2:X_2⊢A(x_2):\mathrm{Type}{x}_1:X_1⊢f(x_1):X_2}{x_1:X_1⊢A(f(x_1)):\mathrm{Type}}$	$$ $\begin{array}{ccc}{f}^{*}A& \to & A\\ \downarrow & & \downarrow \\ X_1& \stackrel{f}{\to }& X_2\end{array}$