Weak omega-Categories from Intensional Type Theory
Weak omega-Categories from Intensional Type Theory
复制标题
内涵类型理论中的弱欧米伽范畴
DOI：
10.2168/lmcs-6(3:24)2010
复制
发表时间：
2008
影响因子：
0.5
通讯作者：
P. Lumsdaine
中科院分区：
文献类型：
--
作者：
P. Lumsdaine
较高的类别最近成为建模强度类型理论的自然背景。这就提出了一个问题，即类型理论的语法自然形成了什么。我们表明，对于任何类型的Martin -Lof强化类型理论，该类型的术语及其较高的身份类型在伦斯特的意义上构成了弱的***类别。确切地说，我们构建了一个可签定的球状operad $ {p _ {\ mathit {ml}^{\ mathrm {id}}}}} $ type type type上可定义的构图定律。
Higher-dimensional categories have recently emerged as a natural context for modelling intensional type theories; this raises the question of what higher-categorical structures the syntax of type theory naturally forms. We show that for any type in Martin-Lof Intensional Type Theory, the system of terms of that type and its higher identity types forms a weak *** -category in the sense of Leinster. Precisely, we construct a contractible globular operad ${P_{\mathit{ML}^{\mathrm{Id}}}}$ of type-theoretically definable composition laws, and give an action of this operad on any type and its identity types.