PreprintCC BY 4.0arXiv
Univalence without function extensionality
Abstract
It is a well-known theorem of homotopy type theory, originally due to Voevodsky, that function extensionality holds inside any univalent universe. We consider a weaker variant of the univalence axiom, asserting that the wild category formed by the universe is univalent, which we call categorical univalence. We show that categorical univalence does not imply function extensionality by an analysis of Von Glehn's polynomial model construction, which produces models of Martin-Löf type theory that always refute function extensionality. We find in particular that when the base model has a univalent universe, its polynomial model has a universe that is categorically univalent but lacks function extensionality.
Related
- Exact Thresholds for Global Univalence, Convexity, and Positive Real Part of a Modified Second Einstein Function
- The Schwarzian derivative in several complex variables univalence and geometry
- Guaranteed Relative Accuracy Around a Real or Complex Zero without Extended Precision
- Global dynamics of Vlasov--wave systems without the null condition under exponential momentum decay
- Maximum principle for quasilinear SPDE’s on a bounded domain without regularity assumptions
BibTeX
@misc{cavallo2026univalence,
title = {{Univalence without function extensionality}},
author = {Evan Cavallo and Jonas Höfer},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2605.00812},
eprint = {2605.00812},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2605.00812},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Univalence without function extensionality
AU - Evan Cavallo
AU - Jonas Höfer
PY - 2026
DA - 2026/09/03
PB - arXiv
DO - 10.48550/arxiv.2605.00812
UR - https://arxiv.org/abs/2605.00812
AB - It is a well-known theorem of homotopy type theory, originally due to Voevodsky, that function extensionality holds inside any univalent universe. We consider a weaker variant of the univalence axiom, asserting that the wild category formed by the universe is univalent, which we call categorical univalence. We show that categorical univalence does not imply function extensionality by an analysis of Von Glehn's polynomial model construction, which produces models of Martin-Löf type theory that always refute function extensionality. We find in particular that when the base model has a univalent universe, its polynomial model has a universe that is categorically univalent but lacks function extensionality.
ER -