论文标题
单价类型
Univalent typoids
论文作者
论文摘要
Typoid是具有等价关系的类型，因此相对于它们之间的给定等价关系，类型的术语之间的等价术语满足了某些条件，从而推广了平等项的属性。所得的弱2组结构可以扩展到每个有限水平。引入的Typoid和Typoid函数的概念推广了setoid和setoid函数的概念。单价键入是满足Univalence Axiom的一般版本的典型类型。我们证明了一些关于单价类型，其产品和指数的基本事实。作为推论，我们在类型理论中得到了命题截断的解释。这对夫妇打字和单价典型词是同型类型理论中对夫妇预定和类别的弱类动物。
A typoid is a type equipped with an equivalence relation, such that the terms of equivalence between the terms of the type satisfy certain conditions, with respect to a given equivalence relation between them, that generalise the properties of the equality terms. The resulting weak 2-groupoid structure can be extended to every finite level. The introduced notions of typoid and typoid function generalise the notions of setoid and setoid function. A univalent typoid is a typoid satisfying a general version of the univalence axiom. We prove some fundamental facts on univalent typoids, their product and exponential. As a corollary, we get an interpretation of propositional truncation within the theory of typoids. The couple typoid and univalent typoid is a weak groupoid-analogue to the couple precategory and category in homotopy type theory.
