HoTT案例研究：适用于数学家的HoTT：案例研究

HoTT案例研究 在职数学家的HoTT：案例研究 该项目旨在举例说明同型类型理论如何处理非正式数学中的一种常见实践，而又不违反其精神，即“争论同构”。 凯文·巴扎德（Kevin Buzzard）与约翰·康梅林（Johan Commelin）和帕特里克·马索特（Patrick Massot）一起了他时，描述了这种做法的一个引人注目的例子：当您通过反转几个元素来迭代圆环的局部化时，您通常想使用一个通过反转元素的乘积来进行局部化。 数学家立即断言，这两个局部环是唯一同构的，可以互换使用而不必再费心了-对于证明检验器，这成为一个更为严重的问题。 特别是，只要没有实际的相等而只有同构，就不可能应用重写策略。 同态类型理论（HoTT）对其均等性及其单价基础（UF）进行了仔细的分析，非常适合处理这种情况：同构将等同于局部环的均等，并且将应用标准重写策略。 为了使这一声明正式化，凯文·巴扎德（Kevi