nLab substitution natural deduction - table

	type theory	category theory
	syntax	semantics
	natural deduction	universal construction
	substitution…………………….	pullback of display maps
	$\frac{ x_2 \colon X_2\; \vdash\; A(x_2) \colon Type \;\;\;\; x_1 \colon X_1\; \vdash \; f(x_1)\colon X_2}{ x_1 \colon X_1 \;\vdash A(f(x_1)) \colon Type}$	$\,$ $\array{ f^* A &\to& A \\ \downarrow && \downarrow \\ X_1 &\stackrel{f}{\to}& X_2 }$