文献

J-GLOBAL ID：202102227765508004   整理番号：21A2678118

インデックス型理論【JST・京大機械翻訳】

Indexed type theories

著者 (1件)： Isaev Valery (JetBrains Research and National Research University Higher School of Economics, St. Petersburg, Russia)
資料名： Mathematical Structures in Computer Science  (Mathematical Structures in Computer Science)
巻： 31  号： 1  ページ： 3-63  発行年： 2020年 
JST資料番号： W2200A  ISSN： 0960-1295  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： イギリス (GBR)  言語： 英語 (EN)

抄録/ポイント： 本論文では,(ホモトピー)型理論が(∞-)カテゴリーに関係するように,索引付き(∞-)カテゴリーに関連する指数型理論を定義した。有限(共)限界,任意(共)製品,指数,物体分類器および直交因数分解システムを含むそのような理論に対するいくつかの標準構成を定義した。また,これらの構築は,Σ型,単位型,同一性型,有限高誘導型,Π型,一価宇宙,およびより高い様式のような,それらのタイプ理論対応物と等価であることも証明した。Please refer to the publisher for the copyright holders. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 因数分解 ,  ホモトピー ,  宇宙空間 ,  直交性 ,  カテゴリー理論 ,  *型理論

著者キーワード (2件)： ホモトピー型理論 ,  カテゴリー理論

分類 (1件)： システム・制御理論一般  (IA02010H)

タイトルに関連する用語 (2件)： インデックス ,  型理論