nLab
judgements for types and terms - table

type theorycategory theory
syntaxsemantics
judgmentdiagram
typeobject in category
A:Type\vdash\; A \colon TypeA𝒞A \in \mathcal{C}
termelement
a:A\vdash\; a \colon A*aA* \stackrel{a}{\to} A
dependent typeobject in slice category
x:XA(x):Typex \colon X \;\vdash\; A(x) \colon TypeA X𝒞 /X\array{A \\ \downarrow \\ X} \in \mathcal{C}_{/X}
term in contextgeneralized elements/element in slice category
x:Xa(x):A(x)x \colon X \;\vdash \; a(x)\colon A(x)X a A id X X\array{X &&\stackrel{a}{\to}&& A \\ & {}_{\mathllap{id_X}}\searrow && \swarrow_{\mathrlap{}} \\ && X}
x:Xa(x):Ax \colon X \;\vdash \; a(x)\colon AX (id X,a) X×A id X p 1 X\array{X &&\stackrel{(id_X,a)}{\to}&& X \times A \\ & {}_{\mathllap{id_X}}\searrow && \swarrow_{\mathrlap{p_1}} \\ && X}
Created on September 28, 2012 23:19:22 by Urs Schreiber (82.113.106.47)