(Pointed) Univalence in Universe Category Models of Type Theory
Logic in Computer Science
2025-12-19 v1 Category Theory
Logic
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.
Keywords
Cite
@article{arxiv.2512.16697,
title = {(Pointed) Univalence in Universe Category Models of Type Theory},
author = {Chris Kapulkin and Yufeng Li},
journal= {arXiv preprint arXiv:2512.16697},
year = {2025}
}
Comments
73 pages; comments welcome