朴素类型论中的同构

摘要：

我们提供了一个治疗的同构内的一套理论制定的依赖类型论。类型表达式被赋予其自然的集合论组合意义。类型分为小类型和大类型-分别是集合和真类。每一个真类，如“群”或“拓扑空间”，都有一个与标准定义相对应的同构概念。同构是通过在所有可定义值的空间上定义一个广群结构来处理的。这些值同时是对象（oid）和态射-它们是“形态体”。合理性，然后可以证明简单和自然的推理规则，推导同构和同构的替代。

英文摘要：

We provide a treatment of isomorphism within a set-theoretic formulation of dependent type theory. Type expressions are assigned their natural set-theoretic compositional meaning. Types are divided into small and large types --- sets and proper classes respectively. Each proper class, such as "group" or "topological space", has an associated notion of isomorphism in correspondence with standard definitions. Isomorphism is handled by definging a groupoid structure on the space of all definable values. The values are simultaneously objects (oids) and morphism --- they are "morphoids". Soundness can then be proved for simple and natural inference rules deriving isomorphisms and for the substitution of isomorphics.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。