On lifting univalence to the equivariant setting

Abstract

This PhD thesis deals with some new models of intensional type theory and the Univalence Axiom introduced by Vladimir Voevodsky. Our work takes place in the framework of the definitions of type-theoretic fibration categories (the notion of model under consideration in this thesis) and universe in a type-theoretic fibration category, definitions due to Michael Shulman. The goal of this thesis consists mainly in the exploration of the stability of the univalence axiom, in particular in the following sense: being given a type-theoretic fibration category C equipped with a univalent universe U, we are eager to endow the functor category [D,C], where D is a small category, with the structure of a type-theoretic fibration category plus a univalent universe.

130 pages

References in corpus (2)

• Higher Topos Theory
• Univalence in locally cartesian closed infinity-categories

Cited by in corpus (2)

• All $(\infty ,1)$-toposes have strict univalent universes
• On the Inadequacy of the Projective Structure with Respect to the Univalence Axiom