The aim of this paper is to refine and extend Voevodsky's draft "A universe polymorphic type system" that outlines a type theory where judgments can depend on equalities between universe levels expressions (constraints). We first recall a version of type theory with an externally indexed sequence of universes. We then add judgments for internal universe levels, built up from level variables by a successor operation and a binary supremum operation, and also judgments for equality of universe levels. Furthermore, we extend this type theory with rules for level-indexed product types. Finally, we add constraints to the theory, so that a hypothetical judgment can depend on equalities between universe levels. We also give rules for constraint-indexed product types, and compare the resulting type theory to Voevodsky's.


翻译:本文的目的是完善和扩展Voevodsky的“ 宇宙多元形态系统” 草案, 该草案概述了一种类型的理论, 判断可以取决于宇宙水平表达式( 约束性) 之间的等同性。 我们首先回顾一个版本的类型理论, 带有外部指数化的宇宙序列 。 然后我们加上对内部宇宙水平的判断, 由水平变量建立, 由后续操作和二进制顶峰操作建立, 以及宇宙水平平等性判断。 此外, 我们扩展了这种类型理论, 并增加了水平指数化产品类型的规则 。 最后, 我们增加了对理论的限制, 这样假设性判断可以取决于宇宙水平的等同性 。 我们还给出了限制指数化产品类型的规则, 并将由此产生的类型理论与Voevodsky 相比较 。

0
下载
关闭预览

相关内容

人类接受高层次教育、进行原创性研究的场所。 现在的大学一般包括一个能授予硕士和博士学位的研究生院和数个专业学院,以及能授予学士学位的一个本科生院。大学还包括高等专科学校
不可错过!《机器学习100讲》课程,UBC Mark Schmidt讲授
专知会员服务
74+阅读 · 2022年6月28日
【硬核书】矩阵代数基础,248页pdf
专知会员服务
86+阅读 · 2021年12月9日
专知会员服务
26+阅读 · 2021年4月2日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
79+阅读 · 2020年7月26日
专知会员服务
61+阅读 · 2020年3月19日
机器学习入门的经验与建议
专知会员服务
94+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
41+阅读 · 2019年10月9日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium8
中国图象图形学学会CSIG
0+阅读 · 2021年11月16日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
28+阅读 · 2019年5月18日
ICLR2019最佳论文出炉
专知
12+阅读 · 2019年5月6日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Arxiv
0+阅读 · 2023年2月7日
Arxiv
0+阅读 · 2023年2月7日
VIP会员
相关VIP内容
不可错过!《机器学习100讲》课程,UBC Mark Schmidt讲授
专知会员服务
74+阅读 · 2022年6月28日
【硬核书】矩阵代数基础,248页pdf
专知会员服务
86+阅读 · 2021年12月9日
专知会员服务
26+阅读 · 2021年4月2日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
79+阅读 · 2020年7月26日
专知会员服务
61+阅读 · 2020年3月19日
机器学习入门的经验与建议
专知会员服务
94+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
41+阅读 · 2019年10月9日
相关资讯
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium8
中国图象图形学学会CSIG
0+阅读 · 2021年11月16日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
28+阅读 · 2019年5月18日
ICLR2019最佳论文出炉
专知
12+阅读 · 2019年5月6日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
相关基金
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Top
微信扫码咨询专知VIP会员