We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets \`a la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT (that every closed boolean is definitionally equal to a constant) by Artin gluing.


翻译:我们展示了一种为Bishop sets à la Coquand 专门设计的笛卡尔式立方体理论的版本XTT, 其中每种类型都享有身份证明的独特性的定义版本。 XTT 利用立方概念重建了许多观察类型理论的基本理念, 这是一种支持功能扩展性的强化型理论的版本。 我们证明了XTT( 每一个闭合的布尔在定义上都等同于恒定值) 的 canonicity 属性 。

0
下载
关闭预览

相关内容

专知会员服务
39+阅读 · 2020年9月6日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Python计算导论,560页pdf,Introduction to Computing Using Python
专知会员服务
72+阅读 · 2020年5月5日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
移动端机器学习资源合集
专知
8+阅读 · 2019年4月21日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
免费自然语言处理(NLP)课程及教材分享
深度学习与NLP
29+阅读 · 2019年1月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
最全数据科学学习资源:Python、线性代数、机器学习...
人工智能头条
11+阅读 · 2018年5月14日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
【推荐】自然语言处理(NLP)指南
机器学习研究会
35+阅读 · 2017年11月17日
【推荐】免费书(草稿):数据科学的数学基础
机器学习研究会
20+阅读 · 2017年10月1日
自然语言处理 (NLP)资源大全
机械鸡
35+阅读 · 2017年9月17日
Arxiv
0+阅读 · 2021年7月7日
Arxiv
0+阅读 · 2021年7月6日
Inference for Low-Rank Models
Arxiv
0+阅读 · 2021年7月6日
Arxiv
0+阅读 · 2021年7月5日
Arxiv
0+阅读 · 2021年7月3日
Arxiv
0+阅读 · 2021年7月2日
Ethics Sheets for AI Tasks
Arxiv
0+阅读 · 2021年7月2日
VIP会员
相关VIP内容
专知会员服务
39+阅读 · 2020年9月6日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Python计算导论,560页pdf,Introduction to Computing Using Python
专知会员服务
72+阅读 · 2020年5月5日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
相关资讯
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
移动端机器学习资源合集
专知
8+阅读 · 2019年4月21日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
免费自然语言处理(NLP)课程及教材分享
深度学习与NLP
29+阅读 · 2019年1月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
最全数据科学学习资源:Python、线性代数、机器学习...
人工智能头条
11+阅读 · 2018年5月14日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
【推荐】自然语言处理(NLP)指南
机器学习研究会
35+阅读 · 2017年11月17日
【推荐】免费书(草稿):数据科学的数学基础
机器学习研究会
20+阅读 · 2017年10月1日
自然语言处理 (NLP)资源大全
机械鸡
35+阅读 · 2017年9月17日
相关论文
Arxiv
0+阅读 · 2021年7月7日
Arxiv
0+阅读 · 2021年7月6日
Inference for Low-Rank Models
Arxiv
0+阅读 · 2021年7月6日
Arxiv
0+阅读 · 2021年7月5日
Arxiv
0+阅读 · 2021年7月3日
Arxiv
0+阅读 · 2021年7月2日
Ethics Sheets for AI Tasks
Arxiv
0+阅读 · 2021年7月2日
Top
微信扫码咨询专知VIP会员