相依型理论的一般定义

这篇论文的预印本“依赖类型理论的一般定义”终于出现在arxiv上了！三年多前，彼得·拉姆斯丹邀请我研究这一主题，我欣然接受，并把我的学生菲利普·哈塞尔沃特拉了进去。我们开始回答这个问题：

至少对我来说，研究这样一个吃力不讨好的话题的动机来自弗拉基米尔·沃沃茨基(VladimirVoevodsky)，他会向类型理论的观众提出这个问题。一些人带他去参加比赛，另一些人则认为他是个新手，只是需要学习更多的类型理论。我是后者中的一员，但最终我遇到了一个问题--我可以举出任何数量的类型理论的具体例子，但不能对一般概念进行全面和精确的数学定义。

通过声称类型理论是一个开放的概念来忽视这个问题太容易了，因此任何数学定义都不能完全涵盖这一概念。当然，它是开放式的，但这并不意味着我们甚至不应该尝试定义它。如果几何学家同样对开放的空间概念抱有宿命论，我们就永远不会有现代的几何学、拓扑学、栅栏--见鬼，20世纪的半个世纪的数学也不会出现！

当然，我们不是第一个也不是最后一个给类型理论下定义的人，事情应该是这样的。我们不主张优先或凌驾于类型理论的其他定义和观点之上。我们的方法或许可以被描述为具体的和证明论的：

我们的目标是达到一个通用性的水平，允许对广泛的类型理论进行有用的元理论。

以上每一点，大家都可以争辩，我们自己也说过很多次，不过，我觉得我们做了一些有价值的事，但最后的评判者将会是我们的读者，或没有读者。我们诚挚地邀请您看一看这份报纸。

我不应该忘记提到Peter，在Philipp和我的适度帮助下，几乎将整篇论文用Coq正式化了！参见GitHub上的资源库一般类型理论。

使用Markdown写下您的评论。使用$⋯$表示内联，使用$$⋯$$表示显示LaTeX公式，使用<；PRE>；⋯<；/PRE>；表示显示代码。您的电子邮件地址仅用于计算您的重力头像，不会存储在任何地方。评论通过拉取请求进行审核。