Unit: a type checker for dependent type theory

Overview & Synopsis

We present Unit, a type checker for dependent type theory with a module system in the tradition of Automath and a uniform treatment of definitions: two uses of a definition are compared by name and arguments before anything is unfolded, and otherwise the definition declared last is opened. There is no unification, no instance search, no tactics and no unfolding heuristic, so the work of checking can be observed and compared with the informal proof. With Unit we have checked a model of univalent type theory, synthetic algebraic geometry up to Châtelet's theorem, and synthetic Stone duality with its cohomology. These developments show that a small, uniform system supports substantial mathematics, and give concrete reasons to reconsider the complexity routinely accepted in proof assistants.