(Pointed) Univalence in Universe Category Models of Type Theory
Chris Kapulkin, Yufeng Li
TL;DR
The paper develops a semantic formulation of Voevodsky's univalence in universe-category models and strengthens it with pointed univalence, motivated by model-category semantics and computation. It constructs a generic object of homotopy isomorphisms and related Id-type structures to express univalence as a lifting property, and proves closure under Artin–Wraith gluing and inverse diagrams (assuming pointed functional extensionality). It also provides type-theoretic and CwR formulations and demonstrates stability of these notions under gluing and inverse diagram constructions, yielding a robust, model-friendly framework for univalent type theory. The results broaden the applicability of univalence to a wide class of semantic models and clarify the relationships between lifting properties, matching objects, and transport in universe-category 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.