Type theory MOC

Dependent type theory

A dependent type theory is a (cartesian) type theory where type formation is context-dependent, #m/def/type and thus may be parameterized by terms. This is in contrast to a non-dependent type theory where only terms are context-dependent, and types may in practice be defined by a Context-free grammar.

Type family

A type in a nonempty context is called type family or fibration. #m/def/type Specifically, if then a type family over in context is given by a judgement

A section picks out a term of for each , and thus corresponds to a judgement¹

When using named contexts in informal type theory, we will often write

where and are not meant to denote actual functions, but rather the occurance of a substitution, so that and .

#state/tidy | #lang/en | #SemBr