• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >A bifibrational reconstruction of Lawvere’s presheaf hyperdoctrine
【24h】

A bifibrational reconstruction of Lawvere’s presheaf hyperdoctrine

机译：Lawvere的束前高学说的双歧重建

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Combining insights from the study of type refinement systems and of monoidal closed chiralities, we show how to reconstruct Lawvere's hyperdoctrine of presheaves using a full and faithful embedding into a monoidal closed bifibration living now over the compact closed category of small categories and distributors. Besides revealing dualities which are not immediately apparent in the traditional presentation of the presheaf hyperdoctrine, this reconstruction leads us to an axiomatic treatment of directed equality predicates (modelled by hom presheaves), realizing a vision initially set out by Lawvere (1970). It also leads to a simple calculus of string diagrams (representing presheaves) that is highly reminiscent of C. S. Peirce's existential graphs for predicate logic, refining an earlier interpretation of existential graphs in terms of Boolean hyperdoctrines by Brady and Trimble. Finally, we illustrate how this work extends to a bifibrational setting a number of fundamental ideas of linear logic.
机译：结合对类型细化系统和单曲面封闭手性的研究的见解，我们展示了如何使用完整和忠实的嵌入到单曲面封闭双纤化中来重构Lawvere的滑轮的超学说，而该分解过程现在生活在小型类别和分销商的紧凑封闭类别中。除了揭示二重性在传统的前捆扎主义理论中没有立即显现出的二元性外，这种重建还使我们对有向平等谓词（由hom presheaves建模）进行公理化处理，实现了Lawvere（1970）最初提出的愿景。这也导致了字符串图的简单演算（表示预滑轮），这非常让人联想到C. S. Peirce的谓词逻辑存在图，从而完善了Brady和Trimble在布尔超doctrines方面对存在图的较早解释。最后，我们说明了这项工作如何扩展到设置了线性逻辑的许多基本概念的双歧化。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号