# Steve Awodey: A remark on Hofmann-Streicher universes

**Time: **
Thu 2022-05-19 10.00 - 12.00

**Location: **
Kräftriket, House 5, Room 31

**Participating: **
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).