Type theory MOC

Dependent type theory

A dependent type theory is a (cartesian) type theory where type formation is context-dependent, 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. 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 𝑏(𝑦) =𝑏(𝑥)[𝑦/𝑥] :𝐵(𝑦).

---

tidy | en | SemBr

Footnotes

1. 2025. Introduction to Homotopy Type Theory, §1.2, pp. 13–14. ↩