Modalities in homotopy type theory
Modalities in homotopy type theory
复制标题
同伦型理论的模态
DOI：
10.23638/lmcs-16(1:2)2020
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Bas Spitters
中科院分区：
文献类型：
--
作者：
E. Rijke;Michael Shulman;Bas Spitters
单叶同伦类型理论（英语：Univalent homotopy type theory，HoTT）可以被看作是$\infty$-广群范畴的语言。它正在发展成为数学的一个新基础，并作为（初级）高等教育的内部语言。我们发展了同伦类型理论中的因子分解系统，反射子宇宙和模态的理论，包括它们使用“本地化”更高归纳类型的构造。这产生特别是（$n$-连接，$n$-截断）因式分解系统，以及内部介绍subtopose，通过lex模态。我们还开发了这些结构的语义。
Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a "localization" higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.
局部笛卡尔闭 â 范畴中的唯一性
影响因子：
0.8
作者：
D. Gepner;J. Kock
通讯作者：
J. Kock
重温偏爱：作为商归纳-归纳类型的偏爱 Monad
DOI：
10.48550/arxiv.1610.09254
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Altenkirch T
通讯作者：
Altenkirch T