2023年11月17日晚上19：30-21：30，浙江大学哲学系的“哲学与类型论“系列讲座之单值与本体结构主义顺利举办。本次讲座由南加利福尼亚大学哲学系的助理教授陈路老师主讲，由浙江大学百人计划研究员Bruno Bentzen主持，总共有34名来自不同院系的老师和同学参加了本次讲座。

讲座一开始，陈路老师就点明此次讲座的主要内容：首先是对于本体结构主义相关内容的介绍，其次是对于同伦类型论(HoTT)和单值公理（UF）的介绍，最后是讨论同伦类型论何以能够解决本体结构主义的问题。

在第一部分，陈老师主要介绍了本体结构主义。陈老师首先解释本体结构主义是什么并且将这一观点与其他的传统观点进行对比。陈老师指出本体结构主义指的是结构而非个体作为基础，个体可以由结构内的关系完全地刻画。最后，陈老师提及了一个本体结构主义本身存在的问题。

在第二部分，陈老师介绍了有关同伦类型论的相关内容。首先，陈老师介绍了一个同构-相等命题：两个同构的系统是同一的。陈老师指出同伦类型论可以用于表达同构-相等命题的框架。同伦类型理论是对集合论和一阶谓词逻辑的一种替代，其核心就是把每一项当作是一个类型。随后，陈老师阐明如何从语义的角度去理解了同伦类型论并用同伦空间做类比介绍了相等类型。陈老师使用单值公理——单值公理在数学上清楚地表达了同构的结构是同一的，解释相等类型为什么能起到这样的作用。为避免误解，陈老师对于同伦类型论里的集合与集合论里的集合的含义做出了区分。

在本次讲座的第三部分，基于同伦类型论和单值公理，陈老师介绍了两种应对第一部分提出的问题的解决方案：代数普遍主义和代数结构主义。陈老师指出两个方案各有优缺点。代数普遍主义有着和不存在常量的一阶逻辑一样的表达力，但是代数普遍主义并不能满足单值公理的要求。代数结构主义的优点是我们不用去明确地去指称结构里的元素，它的语义可以不用去指称个体而达到目的。但在高阶情况之下，它会面对和代数普遍主义一样的问题。随后，陈老师对于可能的三个反驳进行了回应。

在提问环节来自四川大学哲学系的刘佶鑫老师、来自浙江大学哲学学院的Davide Fassio老师、来自浙江大学哲学学院的Bruno Bentzen老师以及各个同学，都提出了自己的见解和疑问。陈老师简要回应了几个关键问题。最后，Bentzen老师对整个讲座和问答环节做了精彩的总结。本次讲座在热烈的掌声中圆满结束。