基本纤维化的表征
A characterisation of elementary fibrations
摘要：
Grothendieck纤维化提供了一个统一的代数框架，它是处理各种形式的逻辑，如一阶逻辑，高阶逻辑和依赖类型理论的基础。在Lawvere提出的范畴逻辑方法中，系统地使用伴随来描述逻辑运算，等式以左伴随的形式沿着基中的对角箭头重新索引。利用范畴论提供的模的观点，我们可以观察那些只维持相等结构的格罗滕迪克纤维化，即所谓的基本纤维化，也就是具有相等性的纤维化。本文提供了一个表征的基础上的纤维中的特定结构的纤维，称为运输。该表征是对已经可用于忠实纤维化的表征的实质性概括。在马丁-洛夫类型理论的同一性类型的语义学中，运输者和使用的结构之间有着密切的相似性。我们通过比较两者来结束本文。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
