# nLab judgements for types and terms - table

type theorycategory theory
syntaxsemantics
judgmentdiagram
typeobject in category
$\vdash\; A \colon Type$$A \in \mathcal{C}$
termelement
$\vdash\; a \colon A$$* \stackrel{a}{\to} A$
dependent typeobject in slice category
$x \colon X \;\vdash\; A(x) \colon Type$$\array{A \\ \downarrow \\ X} \in \mathcal{C}_{/X}$
term in contextgeneralized elements/element in slice category
$x \colon X \;\vdash \; a(x)\colon A(x)$$\array{X &&\stackrel{a}{\to}&& A \\ & {}_{\mathllap{id_X}}\searrow && \swarrow_{\mathrlap{}} \\ && X}$
$x \colon X \;\vdash \; a(x)\colon A$$\array{X &&\stackrel{(id_X,a)}{\to}&& X \times A \\ & {}_{\mathllap{id_X}}\searrow && \swarrow_{\mathrlap{p_1}} \\ && X}$

Created on September 28, 2012 at 23:19:22. See the history of this page for a list of all contributions to it.