Set theory with types
Математика традиционно опирается на теорию множеств Цортера (ZF), где всё есть множество, но это вызывает парадоксы вроде (x \in x) (парадокс Рассела) и абсурдные кодировки: упорядоченная пара ((x,y)) как ({{x},{x,y}}), число (n) как ({0,\ldots,n-1}). Де Бруин в 1973 г. критикует эту "странную идею", отмечая: рациональное число и множество точек в евклидовой плоскости не имеют смысла в пересечении, если всё закодировано как множества. Математики избегают технических деталей ZF, а школьное введение множеств (союзы, пересечения) полезно, но не требует тотальной онтологии.
Де Бруин предлагает теорию множеств с типовыми ограничениями: множества формируются внутри заданного класса/типа, исключая (x \in x) и сохраняя интуитивность. Это мотивировало AUTOMATH — зависимую теорию типов. Достаточно иерархии (\mathbb{N}, \mathbb{N}^\mathbb{N}, \mathbb{N}^{\mathbb{N}^\mathbb{N}}, \ldots) без их объединения (inaccessible); для большего — тип SET с аксиомами ZF. HOL (Isabelle/HOL) реализует подобное; до 1980 "type theory" означала высшую логику Principia Mathematica, а не только Lean/Agda.