arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~
arXiv 2609.01869math.CT

(2-dep,Σ)-范畴不是带族的广义范畴

(2-dep,$Σ$)-categories are not generalised categories with families

Luis Gambarte

AI总结:

本文证明(2-dep,Σ)-范畴与Coraglia等提出的带族的广义范畴非双等价,而是该概念的直接推广,明确了两类范畴在依赖类型范畴刻画中的等价关系差异。

AI中文摘要:

Coraglia和Emmenegger提出的带族的广义范畴是用于范畴化刻画依赖类型概念的最一般概念之一,已证明这类带族的广义范畴与 comprehension 范畴双等价。本文将证明,Petrakis提出的(dep,Σ)-范畴的扩展概念——(2-dep,Σ)-范畴,与带族的广义范畴并非双等价,而是与该概念的直接推广等价。

英文摘要:

The notion of a generalised category with families, introduced by Coraglia and Emmenegger is one of the most general notions introduced to capture categorically the notion of dependent typing. It is shown that these generalised categories with families are biequivalent to comprehension categories. We will show that the notion of a (2-dep,$Σ$)-category, an extension of the notion of a (dep,$Σ$)-category, introduced by Petrakis, is not biequivalent to generalised categories with families, but instead is equivalent to a direct generalisation of that notion.

↑