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/

Hofmann–Streicher lifting of fibred categories

  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