Philosophy - Homotopy Type Theory Seminar September 4, 2024 9:00am — 11:00am Location: In Person - Baker Hall 150 (special date/time) Speaker: JON STERLING, Associate Professor in Logical Foundations and Formal Methods, Department of Computer Science and Technology, University of Cambridge, and, Bye-Fellow, Clare College https://www.jonmsterling.com/ In 1997, Hofmann and Streicher introduced an explicit technique to lift a Grothendieck universe ๐ค from ๐๐๐ญ into the category of ๐๐๐ญ-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, applying the categorical nerve to the universal ๐ค-small discrete fibration gives the generic family of ๐คโs HofmannโStreicher lifting. Although Awodey has investigated HofmannโStreicher lifting in terms of a 1-functor ๐๐๐ญโ๐๐ซ(๐), his analysis can be extended to a 2-functor ๐๐๐ญโ๐ ๐ข๐(๐) that is observed by Weber to be right 2-adjoint to the 2-functor that takes a fibred category to its total category (i.e. the oplax colimit of the corresponding diagram of categories under straightening). A generalised form of HofmannโStreicher lifting that can be applied to categories other than universes is then obtained by conjugating this right 2-adjoint with duality involutions. In joint work with Daniel Gratzer and Andrew Slattery, we have constructed a relative version of the 2-functorial HofmannโStreicher lifting: given a fibration p:๐โ๐, we have a 2-functor ฮ[p]:๐ ๐ข๐(๐)โ๐ ๐ข๐(๐) which is not base change but rather (we conjecture) right pseudo-adjoint to the 2-functor ฮฃ[p]:๐ ๐ข๐(๐)โ๐ ๐ข๐(๐) that sends a fibration q:๐โ๐ to the composite fibration pโq:๐โ๐. A relative version of HofmannโStreicher lifting could give a more regular theory to the practice of computing internal liftings of lifted universes. Event Website: https://www.cmu.edu/dietrich/philosophy/hott/seminars/index.html Add event to Google Add event to iCal
