Univalence without function extensionality

Evan Cavallo; Jonas Höfer

Home/Archive/arXiv

arXiv · 2605.00812

Univalence without function extensionality

Evan Cavallo·Jonas Höfer

View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.LO math.LO

Keep this discovery

BibTeX RIS

Evan Cavallo, Jonas Höfer. 2026-09-03. Univalence without function extensionality. https://arxiv.org/abs/2605.00812

Cite the original work for its findings. Save a collection to share your selection of sources.

Discover connections

cs.LO subject math.LO subject

Connections use source metadata and explicit phrase matches, not verified experimental comparisons.

KEEP EXPLORING

Related papers

arXiv2026

A categorical formulation of Kraus' paradox

We give a categorical formulation of Kraus' "magic trick" for recovering information from truncated types. Rather than type theory, we work in Van den Berg-Moerdijk path categories with a univalent universe, and rather than propositional truncation we work with arbitrary cofibrations, which includes truncation as a special case. We show, using Kraus' argument that any cofibration with homogeneous domain is a monomorphism. We give some simple concrete examples in groupoids to illustrate the interaction between homogeneous types, cofibrations and univalent fibrations.

math.CT↗

arXiv2005

The maximum entropy state

We give an algorithm for calculating the maximum entropy state as the least fixed point of a Scott continuous mapping on the domain of classical states in their Bayesian order.

math.PR↗

arXiv2026

Coexact completion of profinite Heyting algebras and uniform interpolation

This paper shows that the sheaf representation of finitely generated free Heyting algebras constructed by Ghilardi and Zawadowski can be factored as the profinite completion of Heyting algebras, followed by identifying the dual category of profinite Heyting algebras as a full subcategory of a sheaf topos. We show that the dual category of profinite Heyting algebras is an infinitary extensive regular category, and its ex/reg-completion is exactly the aforementioned sheaf topos, which we refer to as the K-topos. We show how certain properties of uniform interpolation can be generalised to the context of arbitrary profinite Heyting algebras, and that they are consequences of the internal logic of the K-topos. Along the way we also establish various topos-theoretic properties of the K-topos.

math.LO↗