In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.


翻译:在构造型集合论中,序数是指具有传递性的集合。 在同伦类型论(HoTT)中,序数是具有传递性、良基、扩张性的二元关系的类型。 如果我们使用(HoTT对构造型集合论的)阿兹尔解释,我们将证明两个定义是等价的。 随后,我们推广了类型论序数的概念,以捕捉所有阿兹尔解释中的集合,而不仅仅是序数。 这导致了一个自然的有序结构类,其中包含了类型论序数,并实现了集合论的高阶归纳解释。 我们所有的结果都在Agda中进行了形式化。

0
下载
关闭预览

相关内容

专知会员服务
42+阅读 · 2020年12月18日
专知会员服务
50+阅读 · 2020年12月14日
【干货书】机器学习速查手册,135页pdf
专知会员服务
125+阅读 · 2020年11月20日
因果图,Causal Graphs,52页ppt
专知会员服务
246+阅读 · 2020年4月19日
【UMD开放书】机器学习课程书册,19章227页pdf,带你学习ML
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
Transferring Knowledge across Learning Processes
CreateAMind
28+阅读 · 2019年5月18日
别说还不懂依存句法分析
人工智能头条
23+阅读 · 2019年4月8日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
这一次,彻底解决滚动穿透
IMWeb前端社区
35+阅读 · 2019年1月4日
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日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
Arxiv
0+阅读 · 2023年6月13日
Arxiv
0+阅读 · 2023年6月13日
Arxiv
0+阅读 · 2023年6月12日
VIP会员
相关VIP内容
相关资讯
Transferring Knowledge across Learning Processes
CreateAMind
28+阅读 · 2019年5月18日
别说还不懂依存句法分析
人工智能头条
23+阅读 · 2019年4月8日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
这一次,彻底解决滚动穿透
IMWeb前端社区
35+阅读 · 2019年1月4日
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日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
Top
微信扫码咨询专知VIP会员