- 一般代数学 ： ローヴェアセオリー ＝ 型理論 ： C-システム
その状況証拠は：
- [Voe15]
- Title: Lawvere theories and C-systems
- Author: Vladimir Voevodsky
- Submitted: 26 Dec 2015
- Pages: 15p
- URL: https://arxiv.org/abs/1512.08104
長さ双射〈l-bijective〉なC-システムが同じものである、と。
- ローヴェアセオリー ： デカルト圏 ＝ C-システム ： 包括圏
- デカルト圏 ： 集合圏 ＝ 包括圏 ： パルムグレン包括圏
固有名：
- $`\mathbf{ComhenCAT}`$ ： 包括圏達の2-圏、デカルト関手とデカルト自然変換かな（https://ncatlab.org/nlab/show/cartesian+natural+transformation）
- $`\mathbf{Palmg}`$ ： パルムグレン包括圏、複前層の圏の脱カートメル化
対応表：
| $`\mathbf{LawTh}`$ | $`\mathbf{CSys}`$ |
| $`\mathcal{L}`$ | $`\mathcal{C}`$ |
| $`\mathbf{CartCAT}`$ | $`\mathbf{ComhenCAT}`$ |
| $`\mathbf{Set}\text{ as CartCAT}`$ | $`\mathbf{Plmgr}`$ |
パルムグレンモデル
- $`\mathrm{Model}(\mathcal{C}) := \mathbf{ComhenCAT}(\mathrm{J}(\mathcal{C}), \mathbf{Palmgr})`$
コンテキストの圏〈C-システム〉 $`\mathcal{C}`$ 上のひとつのモデル $`M`$ は $`\mathcal{C}^\mathrm{op} = \mathcal{S}`$ 上のモデルを定義する。それはインスティチューションになる。
- パルムグレンモデル ＝ インスティチューション
- パルムグレンモデル達の圏 ＝ インスティチューション達の圏
参考：
- [Voe14-15]
- Title: A C-system defined by a universe category
- Author: Vladimir Voevodsky
- Submitted: 28 Sep 2014 (v1), 29 Jul 2015 (v3)
- Pages: 33p
- URL: https://arxiv.org/abs/1409.7925
- [Pal13-16]
- Title: The Grothendieck construction and models for dependent types
- Author: Erik Palmgren
- Date: March 8, 2013; minor editing May 28, 2016
- Pages: 23p
- URL: https://staff.math.su.se/palmgren/iterated_presheaves_and_dependent_types_v8.pdf
- [Abb03]
- Title: Categories of Containers
- Author: Michael Abbott
- Date: August 2003
- Pages: 122p
- URL: https://www.cs.le.ac.uk/people/ma139/docs/thesis.pdf
- [BCDE20-21]
- Title: A Note on Generalized Algebraic Theories and Categories with Families
- Authors: Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
- Submitted: 15 Dec 2020 (v1), 16 Mar 2021 (v2)
- Pages: 17p
- URL: https://arxiv.org/abs/2012.08370
