论文标题
基本纤维的表征
A characterisation of elementary fibrations
论文作者
论文摘要
Grothendieck纤维提供了一个统一的代数框架，该框架是对各种逻辑的处理，例如一阶逻辑，高阶逻辑和依赖类型的理论。在系统地使用伴随来描述逻辑操作的逻辑方法的分类方法中，以左伴随的形式呈现平等，以沿着基部的对角线箭头重新索引。利用类别理论提供的模块化观点，可以查看那些仅维持平等结构，所谓的基本纤维的结构，又称平等纤维的纤维。本文提供了基于纤维中特定结构（称为转运蛋白的特定结构）的基本振动的表征。该表征是对已经用于忠实振动的元素的实质性概括。转运蛋白与Martin-Löf类型理论的身份类型的语义中使用的结构之间存在非常相似的相似之处。我们通过比较两者结束纸张。
Grothendieck fibrations provide a unifying algebraic framework that underlies the treatment of various form of logics, such as first order logic, higher order logics and dependent type theories. In the categorical approach to logic proposed by Lawvere, which systematically uses adjoints to describe the logical operations, equality is presented in the form of a left adjoint to reindexing along a diagonal arrows in the base. Taking advantage of the modular perspective provided by category theory, one can look at those Grothendieck fibrations which sustain just the structure of equality, the so-called elementary fibrations, aka fibrations with equality. The present paper provides a characterisation of elementary fibrations based on particular structures in the fibres, called transporters. The characterisation is a substantial generalisation of the one already available for faithful fibrations. There is a close resemblance between transporters and the structures used in the semantics of the identity type of Martin-Löf type theory. We close the paper by comparing the two.
