类型论宇宙模型中的（指向）单一性

我们给出一种在依赖类型论的宇宙范畴模型中形式化单一性公理的方法，这在同伦论设置下较易验证。我们进一步发展了一种称为指向单一性的单一性公理的强化版本，该版本在计算上具有良好性质且在语义上自然，并且验证了其在 Artin-Wraith 嵌套和逆图构成下的闭合性。