报告题目： An introduction to homotopy type theory

报 告 人： J. Daniel Christensen（加拿大西安大略大学教授）

报告时间：2017年11月1日下午16:10

报告地点：数学实验室

摘要： Type theory is a formal system that was originally intended to describe set-like objects, and which is well-suited to formalizing proofs so that they can be verified by a computer.  Recently, it was realized that type theory is intrinsically homotopical, and can be used to reason about spaces and other homotopical categories. Voevodsky introduced an axiom that he calls Univalence, which says roughly that homotopy equivalence and equality agree.  This axiom holds for spaces, and makes the theory truly homotopical.  This talk will start with an introduction to type theory, will introduce Univalence and give examples of its consequences, and will briefly discuss some recent work on developing the theory of localization in homotopy type theory.

欢迎全校师生参加！
注：本次讲座将纳入数学系继续教育课程。

理学院

2017年10月31日