Philosophy - Homotopy Type Theory Seminar
โ 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