Most categorical models for dependent types have traditionally been heavily set based: contexts form a category, and for each we have a set of types in said context -- and for each type a set of terms of said type. This is the case for categories with families, categories with attributes, and natural models; in particular, all of them can be traced back to certain discrete Grothendieck fibrations. We extend this intuition to the case of general, non necessarily discrete, fibrations, so that over a given context one has not only a set but a category of types. We argue that the added structure can be attributed to a notion of subtyping that shares many features with that of coercive subtyping, in the sense that it is the product of thinking about subtyping as an abbreviation mechanism: we say that a given type $A'$ is a subtype of $A$ if there is a unique coercion from $A'$ to $A$. Whenever we need a term of type $A$, then, it suffices to have a term of type $A'$, which we can `plug-in' into $A$. For this version of subtyping we provide rules, coherences, and explicit models, and we compare and contrast it to coercive subtyping as introduced by Z. Luo and others. We conclude by suggesting how the tools we present can be employed in finding appropriate rules relating subtyping and certain type constructors.


翻译:暂无翻译

0
下载
关闭预览

相关内容

专知会员服务
49+阅读 · 2021年8月13日
【ACL2020】多模态信息抽取,365页ppt
专知会员服务
141+阅读 · 2020年7月6日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
145+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
171+阅读 · 2019年10月11日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
学习自然语言处理路线图
专知会员服务
134+阅读 · 2019年9月24日
RL解决'BipedalWalkerHardcore-v2' (SOTA)
CreateAMind
31+阅读 · 2019年7月17日
一文了解成分句法分析
人工智能头条
15+阅读 · 2019年4月24日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
Focal Loss for Dense Object Detection
统计学习与视觉计算组
11+阅读 · 2018年3月15日
CNN 反向传播算法推导
统计学习与视觉计算组
28+阅读 · 2017年12月29日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
Layer Normalization原理及其TensorFlow实现
深度学习每日摘要
32+阅读 · 2017年6月17日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 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+阅读 · 2月8日
VIP会员
相关资讯
RL解决'BipedalWalkerHardcore-v2' (SOTA)
CreateAMind
31+阅读 · 2019年7月17日
一文了解成分句法分析
人工智能头条
15+阅读 · 2019年4月24日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
Focal Loss for Dense Object Detection
统计学习与视觉计算组
11+阅读 · 2018年3月15日
CNN 反向传播算法推导
统计学习与视觉计算组
28+阅读 · 2017年12月29日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
Layer Normalization原理及其TensorFlow实现
深度学习每日摘要
32+阅读 · 2017年6月17日
相关基金
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 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会员