An E-bicategory of E-categories, exemplifying a type-theoretic approach to bicategories
An E-bicategory of E-categories, exemplifying a type-theoretic approach to bicategories
复制标题
E 类别的 E 双类别，举例说明了双类别的类型理论方法
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
O. Wilander
中科院分区：
文献类型：
--
作者：
O. Wilander
在这篇论文中的前三篇论文研究了在类型论中作为一个具有等价关系的数据类型的集合的形式化-一个通常被称为setoid的对象。局部小范畴的相应形式化称为E-范畴。在论文I中，我们证明了没有宇宙的类型论不足以证明setoids的E-范畴的某些预期性质成立，但一个极小宇宙是足够的。在论文II中，我们证明了虽然所有E-范畴的集合不能形成一个范畴，但我们可以引入一个类型论版本的双范畴，并且E-范畴形成这样一个E-双范畴。在论文III中，我们考虑了类型论宇宙中的setoids。唯一替换公理的提出和使用表明，这些形式的一个小范畴（即，一个类别与setoid的对象和一个单一的setoid的所有箭头）。我们证明，这种建设不能进行，而不增加一些新的公理类型论。我们还表明，公理的唯一替换严格弱于公理的唯一身份证明。在论文IV中，我们调查部分等价关系，也被称为部分setoids，在海廷算术在所有有限类型，并适应的结果，外延公理的选择是等价的组合的内涵公理的选择，经典逻辑，和外延公理。在第五篇中，我们研究了部分项逻辑PHL，并证明了它和一个相关演算的割消定理。
The first three papers in this thesis study the formalisation of a set in type theory as a data type with an equivalence relation – an object usually known as a setoid. The corresponding formalisation of a locally small category is called an E-category. In Paper I, we show that type theory without universes is insufficient for proving that some expected properties hold of the E-category of setoids, but that a minimal universe is sufficient. In Paper II, we show that although the collection of all E-categories does not form a category, we can introduce a type-theoretic version of bicategories, and the E-categories form such an E-bicategory. In Paper III, we consider the setoids inside a type-theoretic universe. The axiom of unique substitutions is proposed and used to show that these form a small category (that is, a category witha setoid of objects and a single setoid of all arrows). We demonstrate that this construction can not be carried out without adding some new axiom to type theory. We also show that the axiom of unique substitutions is strictly weaker than the axiom of unique identity proofs. In Paper IV, we investigate partial equivalence relations, also known as partial setoids, in Heyting arithmetic in all finite types, and adapt the result that the extensional axiom of choice is equivalent to the combination of the intensional axiom of choice, classical logic, and an extensionality axiom. In Paper V, we investigate PHL, a logic of partial terms, and prove a cut elimination theorem for it and for a related calculus.