Hofmann-Streicher lifting of fibred categories : Dedicated to the memory of Thomas Streicher (1958-2025)
Andrew Slattery, Jonathan Sterling
Abstract
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.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 7b6907ca-ee48-4165-9975-64e6d31a8dc0Related papers
- 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 citation
- 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 citations
- The Smash Product of Monoidal TheoriesAmar HadzihasanovicLICS 2021 · 5 citations
- Fully abstract models for effectful λ-calculi via category-theoretic logical relationsOhad Kammar, Shin-ya Katsumata, Philip SavillePOPL 2022 · 3 citations
