(Pointed) Univalence in Universe Category Models of Type Theory

TL;DR

This paper formulates a version of the univalence axiom within universe category models of dependent type theory, introduces a strengthened pointed univalence axiom, and verifies its properties in homotopy-theoretic contexts.

Contribution

It develops a new formulation of univalence suitable for homotopy-theoretic models and introduces pointed univalence with desirable computational and semantic features.

Findings

Pointed univalence is verified to be closed under Artin-Wraith gluing.

The strengthened univalence axiom is both computationally desirable and semantically natural.

The formulation facilitates verification in homotopy-theoretic settings.

Abstract

We provide a formulation of the univalence axiom in a universe category model of dependent type theory that is convenient to verify in homotopy-theoretic settings. We further develop a strengthening of the univalence axiom, called pointed univalence, that is both computationally desirable and semantically natural, and verify its closure under Artin-Wraith gluing and formation of inverse diagrams.