term in context

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** = **propositions as types** +**programs as proofs** +**relation type theory/category theory**

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

$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 \colon A \;\vdash \; B(a) \colon Type
\,.$

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