Till innehåll på sidan

# Steve Awodey: A remark on Hofmann-Streicher universes

Tid: To 2022-05-19 kl 10.00 - 12.00

Plats: Kräftriket, House 5, Room 31

Föreläsare: Steve Awodey (Carnegie Mellon University)

### Abstract

We have another look at the construction by Hofmann and Streicher [1] of a semantic universe $$El \rightarrow U$$ for the interpretation of Martin-Löf type theory in a presheaf category $$[C^{op}, Set].$$  It turns out that $$El \rightarrow U$$ can be described as the “categorical nerve” of the classifier $$Set^* \rightarrow Set$$  for discrete fibrations in Cat, where the nerve is the right adjoint in an apparently unnoticed adjunction, $$\int\dashv \text{nerve} : Cat —> [C^{op}, Set]$$, the left adjoint of which is the well-known “Grothendieck construction” taking a presheaf $$P : C^{op} —> Set$$ to its category of elements $$\int_C P$$ . [1] Lifting Grothendieck Universes, Martin Hofmann and Thomas Streicher, 1997 (unpublished).