Contents

# Contents

## Idea

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 \,.$

Last revised on May 7, 2022 at 08:56:45. See the history of this page for a list of all contributions to it.