局部宇宙模型：依赖类型论中一种被忽视的连贯性构造

我们为理解范畴提出了一个新的连贯性定理，提供了依赖类型论的严格模型，该模型包含所有标准构造子，包括依赖积、依赖和、恒等类型及其他归纳类型。确切地说，我们以一个“弱模型”作为输入：一个理解范畴，配备有对应于所需逻辑构造的结构。我们始终假设基范畴接近局部笛卡尔闭：具体而言，积和某些指数存在。除此之外，我们仅要求逻辑结构应是“弱稳定的”——这是一个纯粹的存在性陈述，不涉及任何特定的结构选择，弱于标准的范畴贝克-切瓦利条件，并且在当前标准的类型论同伦论模型中成立。给定这样一个理解范畴，我们构造一个等价的分裂范畴，其逻辑结构在重新索引下是严格稳定的。这产生了具有所选构造子的类型论的一个解释。该模型改编自沃沃德斯基使用宇宙进行连贯性构造的方法，在纤维化层面是吉罗的一个经典构造。它可以从局部宇宙或延迟替换的角度来理解。