pith. machine review for the scientific record. sign in

arxiv: 1512.04083 · v3 · submitted 2015-12-13 · 🧮 math.CT · math.AT· math.LO

Recognition: unknown

On lifting univalence to the equivariant setting

Authors on Pith no claims yet
classification 🧮 math.CT math.ATmath.LO
keywords categoryfibrationtype-theoreticthesisunivalenceuniverseaxiomdefinitions
0
0 comments X
read the original 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.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Univalence without function extensionality

    cs.LO 2026-05 unverdicted novelty 8.0

    Categorical univalence of a universe does not entail function extensionality, as shown by polynomial models of type theory that refute the latter while satisfying the former.