Hofmann-Streicher lifting of fibred categories : Dedicated to the memory of Thomas Streicher (1958-2025)
Andrew Slattery, Jonathan Sterling
摘要
In 1997, Hofmann and Streicher introduced an explicit construction to lift a Grothendieck universe from the category of sets into the category of set-valued presheaves on a small category. More recently, Awodey presented an elegant functorial analysis of this construction in terms of the categorical nerve, the right adjoint to the functor that takes a presheaf to its category of elements; in particular, the categorical nerve's functorial action on the universal small discrete fibration gives the generic family of the universe's Hofmann-Streicher lifting. Inspired by Awodey's analysis, we define a relative version of Hofmann-Streicher lifting in terms of the right pseudo-adjoint to the 2-functor given by postcomposition with a fibration. Finally, we construct a new 2-bifibration of fibrations in which the opcartesian and cartesian lifts arise from these pseudo-adjunctions.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
相关 Paper
- Logical relations for call-by-push-value models, via internal fibrations in a 2-categoryPedro H. Azevedo de Amorim, Satoshi Kura, Philip SavilleLICS 2025 · 被引用 1 次
- A Cartesian Closed Fibration of Higher-Order Regular LanguagesPaul-André Melliès, Vincent MoreauLICS 2026
- A Constructive Model of Directed Univalence in Bicubical SetsMatthew Z. Weaver, Daniel R. LicataLICS 2020 · 被引用 15 次
- The Smash Product of Monoidal TheoriesAmar HadzihasanovicLICS 2021 · 被引用 5 次
- Fully abstract models for effectful λ-calculi via category-theoretic logical relationsOhad Kammar, Shin-ya Katsumata, Philip SavillePOPL 2022 · 被引用 3 次
