Skip to main content
To KTH's start page To KTH's start page

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)

Export to calendar


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).