# Contents

## Idea

In type theory, a term in context is a term such as

$a:A\phantom{\rule{thickmathspace}{0ex}}⊢\phantom{\rule{thickmathspace}{0ex}}b\left(a\right):B\left(a\right)$a \colon A \; \vdash \; b(a) \colon B(a)

which may involve free variables from some context (here, $a:A$). In dependent type theory, the type of a term in context may also depend on the same context, an $A$-dependent type, such as

$a:A\phantom{\rule{thickmathspace}{0ex}}⊢\phantom{\rule{thickmathspace}{0ex}}B\left(a\right):\mathrm{Type}\phantom{\rule{thinmathspace}{0ex}}.$a \colon A \;\vdash \; B(a) \colon Type \,.

Revised on September 28, 2012 16:51:05 by Urs Schreiber (82.169.65.155)