Scholarlink

Homotopy type theory, together with the partition of types into levels and the univalence axiom developed by Vladimir Voevodsky, provides both a new logical foundation for mathematics, called Univalent Foundations, and a formal language usable with computers for checking the proofs mathematicians make.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Univalent Foundations

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Daniel R. Grayson

摘要

Homotopy type theory, together with the partition of types into levels and the univalence axiom developed by Vladimir Voevodsky, provides both a new logical foundation for mathematics, called Univalent Foundations, and a formal language usable with computers for checking the proofs mathematicians make.