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