Internal language theorems are fundamental in categorical logic, since they express an equivalence between syntax and semantics. One of such theorems was proven by Clairambault and Dybjer, who corrected the result originally by Seely. More specifically, they constructed a biequivalence between the bicategory of locally Cartesian closed categories and the bicategory of democratic categories with families with extensional identity types, $\sum$-types, and $\prod$-types. This theorem expresses that the internal language of locally Cartesian closed is extensional Martin-L\"of type theory with dependent sums and products. In this paper, we study the theorem by Clairambault and Dybjer for univalent categories, and we extend it to various classes of toposes, among which are $\prod$-pretoposes and elementary toposes. The results in this paper have been formalized using the proof assistant Coq and the UniMath library.


翻译:暂无翻译

0
下载
关闭预览

相关内容

论文(Paper)是专知网站核心资料文档,包括全球顶级期刊、顶级会议论文,及全球顶尖高校博士硕士学位论文。重点关注中国计算机学会推荐的国际学术会议和期刊,CCF-A、B、C三类。通过人机协作方式,汇编、挖掘后呈现于专知网站。
专知会员服务
127+阅读 · 2021年6月18日
【机器学习术语宝典】机器学习中英文术语表
专知会员服务
59+阅读 · 2020年7月12日
【ACL2020】多模态信息抽取,365页ppt
专知会员服务
143+阅读 · 2020年7月6日
FlowQA: Grasping Flow in History for Conversational Machine Comprehension
专知会员服务
28+阅读 · 2019年10月18日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
学习自然语言处理路线图
专知会员服务
137+阅读 · 2019年9月24日
知识图谱最新研究综述
深度学习自然语言处理
45+阅读 · 2020年6月14日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
STRCF for Visual Object Tracking
统计学习与视觉计算组
14+阅读 · 2018年5月29日
Focal Loss for Dense Object Detection
统计学习与视觉计算组
11+阅读 · 2018年3月15日
国家自然科学基金
11+阅读 · 2017年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
4+阅读 · 2014年12月31日
Arxiv
0+阅读 · 11月11日
Recent advances in deep learning theory
Arxiv
50+阅读 · 2020年12月20日
VIP会员
相关VIP内容
专知会员服务
127+阅读 · 2021年6月18日
【机器学习术语宝典】机器学习中英文术语表
专知会员服务
59+阅读 · 2020年7月12日
【ACL2020】多模态信息抽取,365页ppt
专知会员服务
143+阅读 · 2020年7月6日
FlowQA: Grasping Flow in History for Conversational Machine Comprehension
专知会员服务
28+阅读 · 2019年10月18日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
学习自然语言处理路线图
专知会员服务
137+阅读 · 2019年9月24日
相关资讯
知识图谱最新研究综述
深度学习自然语言处理
45+阅读 · 2020年6月14日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
STRCF for Visual Object Tracking
统计学习与视觉计算组
14+阅读 · 2018年5月29日
Focal Loss for Dense Object Detection
统计学习与视觉计算组
11+阅读 · 2018年3月15日
相关基金
国家自然科学基金
11+阅读 · 2017年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
4+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员