2025/12/18 by Kapulkin, Chris, Li, Yufeng
#Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2512.16697
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.