The Set-Theoretic Type

Dependent type theory and set theory have different foundations but overlapping ambitions. Type theory builds mathematics from typing rules — every object has a type, and the rules for forming types encode mathematical structure. Set theory builds mathematics from membership — every object is a set, and the axioms for membership encode what exists. The two traditions have mostly developed in parallel, with occasional translations between them.

Yang, Guilloud, and Kunčak (arXiv:2603.12827) demonstrate a mechanized embedding of dependent function types with universe hierarchies into schematic first-order logic based on Tarski-Grothendieck set theory axioms. Using the Lisa proof assistant, they implement bidirectional type-checking as a tactic that computes proofs of typing judgments, verified from set-theoretic axioms and deduction rules.

The types-as-sets paradigm makes this possible: a dependent function type Π(x:A).B(x) is interpreted as a set of functions whose domain is A and whose codomain varies with the input. The universe hierarchy (Type₀ : Type₁ : Type₂ : …) maps to a hierarchy of Grothendieck universes — sets large enough to be closed under the standard set-forming operations. The embedding is not a loose analogy but a formal translation with mechanically verified correctness.

The result addresses a practical question: can automated reasoning tools built for set theory handle dependent types? The answer is yes, with the caveat that the encoding introduces overhead — what type theory handles natively through its rules, set theory must handle through axioms and lemmas. But the overhead is manageable, and the embedding enables set-theoretic proof assistants to work with dependently typed mathematics without abandoning their foundations.