同伦类型论的 2-连贯内部模型

内部类型理论的研究纲领旨在使用依值类型理论自身的语言来发展依值类型理论的范畴模型论。在本研究中，我们通过将带族范畴（cwf）的概念放宽为野生或预连贯高阶 cwf 的概念来研究内部同伦类型论，并确定足以恢复依值类型理论模型所期望性质的连贯条件。其结果是分裂 2-连贯野生 cwf 的定义，它以语法和由宇宙类型给出的“标准模型”作为实例。这将允许我们直接将同伦类型论中 2-连贯自反的概念内部化：即作为从语法到标准模型的 2-连贯野生 cwf 态射。我们的理论也很容易特化以给出“低维”高阶 cwf 的定义，并推测性地将容器高阶模型作为另一个实例包含在内。