单向等价性在单纯同类型论中的实现

单纯同类型论扩展了同类型论，引入了具有单向路径类型的概念，以内部化类型内同态的概念。这一概念在数学领域具有重要应用——其中允许进行合成（更高阶）范畴论；以及在编程语言领域——其中导致单向结构同一原则的延伸。在本工作中，我们构造了单纯同类型论中第一个具有非平凡同态的类型。我们将单纯同类型论扩展引入单向模态和新的推理原则，以获得三角形同类型论，以构建离散类型的宇宙 $\mathcal{S}$。我们证明了该类型中的同态对应类型中的普通函数，即 $\mathcal{S}$ 是单向等价的。$\mathcal{S}$ 的构建是单纯同类型论这两个应用的基础。我们能够定义若干关键范畴的例子，并从范畴论中恢复重要结果。使用 $\mathcal{S}$，我们还能够定义各种类型，其用法保证是函子性的。这些提供了所提议的单向结构同一原则的第一个完整示例。