Anders Mörtberg: The Category of Iterative Sets in Univalent Foundations

Abstract

When working in HoTT/UF the category of h-sets is traditionally used as a univalent version of the category of sets. One consequence of this is that one gets a 1-type of objects instead of an h-set. This is often what one wants in univalent mathematics, but for some applications it is better to give up univalence in favor of an h-set of objects. There are many constructions of such set universes in HoTT/UF and a particularly elegant one is Gylterud's refinement of Aczel's 1978 universe of sets V which is based on W-types. In the talk I will report on ongoing work with Bonnevier, Gratzer and Gylterud to analyze Gylterud's universe from a category theoretic perspective, with the aim of formalizing models of type theory inside of HoTT/UF.