nLab
judgements for types and terms - table

type theory	category theory
syntax	semantics
judgment	diagram
type	object in category
$⊢A:\mathrm{Type}$	$A\in 𝒞$
term	element
$⊢a:A$	$*\stackrel{a}{\to }A$
dependent type	object in slice category
$x:X⊢A(x):\mathrm{Type}$	$\begin{array}{c}A\\ \downarrow \\ X\end{array}\in {𝒞}_{/X}$
term in context	generalized elements/element in slice category
$x:X⊢a(x):A(x)$	$\begin{array}{ccccc}X& & \stackrel{a}{\to }& & A\\ & {}_{{\mathrm{id}}_X}\searrow & & {\swarrow }_{}\\ & & X\end{array}$
$x:X⊢a(x):A$	$\begin{array}{ccccc}X& & \stackrel{({\mathrm{id}}_X,a)}{\to }& & X\times A\\ & {}_{{\mathrm{id}}_X}\searrow & & {\swarrow }_{p_1}\\ & & X\end{array}$