# nLab substitution natural deduction - table

type theorycategory theory
syntaxsemantics
natural deductionuniversal construction
substitution…………………….pullback
$\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 }$

Last revised on November 14, 2012 at 22:38:09. See the history of this page for a list of all contributions to it.