关于名义立方集中一致 Kan 条件的注记

Bezem、Coquand 和 Huber 最近在满足一种称为一致 Kan 条件 (UKC) 的新颖条件的名义立方集范畴中，给出了高阶类型论的一个构造性有效模型，该条件推广了标准立方 Kan 条件（如 Williamson 在其组合同伦论综述中所考虑的那样），以允许在开盒中存在虚拟的“额外”维度。本注记代表了作者填补 UKC 细节的尝试，旨在为该领域的新手提供更明确的主要思想表述和发展。阐述的核心是针对余筛的 Yoneda 引理的类比，它将几何开盒与其代数对应物双射地联系起来，正如其在可表对象上的前身将几何立方体与其在立方集中的代数对应物联系起来一样。这一刻画被用于给出一致 Kan 纤维化的表述，其中一致性表现为额外维度中的自然性。