Univalence without function extensionality
Publish this paper in The AIPR Journal
Are you an author? Turn this AI review into a permanent, citable journal entry with a cover, open comments, and Scholar metadata.
AIPR assessment
Problem difficulty: high. The paper addresses an active foundational question in homotopy type theory, where small changes in axioms often have subtle semantic consequences. Strengths reinforce each other well: the decomposition of univalence is clean, the polynomial-model argument is explicit, and the final separation theorem is sharp. Weaknesses also compound, but mostly in the expected way for a pure theory paper: no implementation artifact, no empirical validation, and several strong semanti
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.
Score Breakdown
More from this week
- Beyond Visual Fidelity: Benchmarking Super-Resolution Models for Large-Scale Remote Sensing Imagery via Downstream Task Integration
- Eliminating Hidden Serialization in Multi-Node Megakernel Communication
- Succinct Graph Representations and Algorithmic Applications
- A Faster Deterministic Algorithm for Fully Dynamic Maximal Matching
- Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs