← 研踪 PaperTrailarXiv:2610.34264 · v2
Unit: a type checker for dependent type theory
首次提交 2026-10-25 20:50
版本更新 2026-10-27 15:04
雷达观测 2026-10-29 00:35
摘要
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. 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 Chatelet's theorem, and synthetic Stone duality with its cohomology, and results on finite free resolustions. These developments show that a small, uniform system supports substantial mathematics, and give concrete reasons to reconsider the complexity routinely accepted in proof assistants.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v2 · 2026-10-27 15:04 · 最新观测版本
Unit: a type checker for dependent type theory
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. 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 Chatelet's theorem, and synthetic Stone duality with its cohomology, and results on finite free resolustions. These developments show that a small, uniform system supports substantial mathematics, and give concrete reasons to reconsider the complexity routinely accepted in proof assistants.
查看此版本解读 →查看此版本原文 ↗