pith. machine review for the scientific record. sign in

arxiv: 2605.00812 · v1 · submitted 2026-05-01 · 💻 cs.LO · math.LO

Recognition: unknown

Univalence without function extensionality

Evan Cavallo , Jonas H\"ofer
Authors on Pith no claims yet

Pith reviewed 2026-05-09 18:06 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords univalencefunction extensionalityMartin-Löf type theorypolynomial modelscategorical univalencehomotopy type theorymodel construction
0
0 comments X

The pith

Categorical univalence of the universe does not imply function extensionality.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that a weaker form of univalence, requiring only that the universe forms a univalent wild category, does not force function extensionality to hold in Martin-Löf type theory. This is shown by examining polynomial models constructed via Von Glehn's method, which always refute function extensionality. When the base model has a univalent universe, the polynomial model still yields a categorically univalent universe. A sympathetic reader would care because this cleanly separates two notions previously linked by Voevodsky's theorem that full univalence implies function extensionality.

Core claim

It is a well-known theorem of homotopy type theory that function extensionality holds inside any univalent universe. Categorical univalence is the weaker assertion that the wild category formed by the universe is univalent. An analysis of Von Glehn's polynomial model construction shows that these models always refute function extensionality. In particular, when the base model has a univalent universe, its polynomial model has a universe that is categorically univalent but lacks function extensionality.

What carries the argument

Von Glehn's polynomial model construction, which takes a base model of Martin-Löf type theory and produces a new model that refutes function extensionality while allowing the universe to remain categorically univalent if the base universe was univalent.

Load-bearing premise

Von Glehn's polynomial model construction yields valid models of Martin-Löf type theory in which function extensionality is refuted while the universe remains categorically univalent.

What would settle it

A concrete check would be to verify whether the identity types and equivalence data in the polynomial model satisfy the categorical univalence condition when the base model is univalent; failure of that condition or unexpected validity of function extensionality would refute the separation.

read the original 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\"of 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper claims that categorical univalence (the universe, viewed as a wild category, satisfies that identities coincide with equivalences) does not imply function extensionality. This separation is obtained by analyzing Von Glehn's polynomial model construction, which is known to refute function extensionality in models of Martin-Löf type theory; the central result is that if the base model has a univalent universe, then the induced polynomial model has a universe that remains categorically univalent.

Significance. If the central claim holds, the result cleanly separates two notions of univalence that are often conflated in the HoTT literature and supplies an explicit model witnessing the separation. The reliance on an existing, independently studied model construction (Von Glehn) rather than an ad-hoc construction is a methodological strength; the result would be useful for calibrating the strength of univalence axioms and for guiding the design of universes in proof assistants.

major comments (2)
  1. [analysis of Von Glehn's polynomial model construction] The transfer of categorical univalence through the polynomial model construction is the load-bearing step for the central claim. The manuscript states that an analysis of Von Glehn's construction establishes preservation when the base universe is univalent, but the interaction between the base univalence data (identity types coinciding with equivalences) and the higher structure of the polynomial interpretation (types reinterpreted as polynomials) is not automatic; a concrete lemma or proposition showing that the relevant equivalences lift is required.
  2. [polynomial model construction] It is asserted that the polynomial models always refute function extensionality. While this is attributed to Von Glehn, the manuscript must verify that the refutation survives the reinterpretation of the universe (i.e., that the function-extensionality failure is not accidentally restored by the categorical-univalence data).
minor comments (2)
  1. [introduction] The introduction should include a brief, self-contained definition of 'wild category' and 'categorical univalence' before the main theorem, rather than relying solely on the abstract.
  2. [Von Glehn's construction] Notation for the polynomial functor and the induced universe should be introduced with an explicit equation or diagram in the section describing the construction.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading, positive evaluation of the result's significance, and constructive suggestions for improving the clarity of the polynomial model analysis. We address the two major comments below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: [analysis of Von Glehn's polynomial model construction] The transfer of categorical univalence through the polynomial model construction is the load-bearing step for the central claim. The manuscript states that an analysis of Von Glehn's construction establishes preservation when the base universe is univalent, but the interaction between the base univalence data (identity types coinciding with equivalences) and the higher structure of the polynomial interpretation (types reinterpreted as polynomials) is not automatic; a concrete lemma or proposition showing that the relevant equivalences lift is required.

    Authors: We agree that an explicit lifting statement is needed to make the preservation of categorical univalence fully rigorous. In the revised manuscript we will insert a new lemma (placed immediately after the recall of Von Glehn's construction) that states: if the base model satisfies categorical univalence for its universe U, then for any two polynomials P and Q over U the induced map on polynomial interpretations preserves the identification of identity types with equivalences. The proof proceeds by transporting the base-level equivalence data along the polynomial functor and verifying that the higher-dimensional structure of the wild category is preserved; this is a direct but previously implicit calculation that we will now spell out. revision: yes

  2. Referee: [polynomial model construction] It is asserted that the polynomial models always refute function extensionality. While this is attributed to Von Glehn, the manuscript must verify that the refutation survives the reinterpretation of the universe (i.e., that the function-extensionality failure is not accidentally restored by the categorical-univalence data).

    Authors: The refutation of function extensionality arises from the polynomial interpretation of the function-space constructor itself and is therefore orthogonal to the univalence data carried by the universe. In the revised version we will add a short verification paragraph (in the subsection on the failure of function extensionality) that recalls Von Glehn's concrete counterexample and observes that the same witness remains a counterexample after the universe is reinterpreted as categorically univalent, because the additional univalence data only equates identities with equivalences inside the universe and does not alter the non-extensional behaviour of the function types. revision: yes

Circularity Check

0 steps flagged

No significant circularity; result rests on external Von Glehn construction

full rationale

The paper establishes its separation by analyzing Von Glehn's polynomial model construction, which is cited as prior independent work that refutes function extensionality in the resulting models. The claim that categorical univalence transfers from a univalent base universe is presented as following from this external analysis rather than from any self-definitional equation, fitted parameter renamed as prediction, or load-bearing self-citation chain internal to the paper. No equations or definitions in the provided abstract reduce the target property to the input by construction, and the derivation remains self-contained against the external benchmark of Von Glehn's models.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper rests on standard axioms of Martin-Löf type theory and the correctness of an external polynomial model construction; no free parameters or invented entities are introduced.

axioms (2)
  • standard math Martin-Löf type theory axioms
    The models constructed are models of MLTT.
  • domain assumption Von Glehn's polynomial model construction produces models refuting function extensionality
    Central to the separation argument.

pith-pipeline@v0.9.0 · 5404 in / 1171 out tokens · 31201 ms · 2026-05-09T18:06:45.245354+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

51 extracted references · 33 canonical work pages

  1. [1]

    Altenkirch and N

    Abbott, M., T. Altenkirch and N. Ghani,Categories of containers, in: A. D. Gordon, editor,Foundations of Software Science and Computation Structures (FoSSaCS 2003), volume 2620 ofLecture Notes in Computer Science, pages 23–38, Springer Berlin Heidelberg (2003). https://doi.org/10.1007/3-540-36576-1_2

    work page doi:10.1007/3-540-36576-1_2 2003

  2. [2]

    G.,Categories of Containers, Ph.D

    Abbott, M. G.,Categories of Containers, Ph.D. thesis, University of Leicester (2003). https://hdl.handle.net/2381/30102

    2003

  3. [3]

    Altenkirch, T. and A. Kaposi,A container model of type theory(2021). Abstract for a presentation at TYPES 2021. https://types21.liacs.nl/download/a-container-model-of-type-theory

    2021

  4. [4]

    Brunerie, T

    Angiuli, C., G. Brunerie, T. Coquand, R. Harper, K.-B. Hou (Favonia) and D. R. Licata,Syntax and models of cartesian cubical type theory, Mathematical Structures in Computer Science31, pages 424–468 (2021). https://doi.org/10.1017/S0960129521000347

    work page doi:10.1017/s0960129521000347 2021

  5. [5]

    Angiuli, C. and D. Gratzer,Principles of Dependent Type Theory(2025). Draft of a book to be published by Cambridge University Press. https://www.danielgratzer.com/papers/type-theory-book.pdf

    2025

  6. [6]

    Natural models of homotopy type theory

    Awodey, S.,Natural models of homotopy type theory, Mathematical Structures in Computer Science28, pages 241–286 (2016). https://doi.org/10.1017/s0960129516000268

    work page doi:10.1017/s0960129516000268 2016

  7. [7]

    Coquand and S

    Bezem, M., T. Coquand and S. Huber,A model of type theory in cubical sets, in: R. Matthes and A. Schubert, editors, 19th International Conference on Types for Proofs and Programs, TYPES 2013, Toulouse, France, April 22-26, 2013, volume 26 ofLIPIcs, pages 107–128, Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik (2014). https://doi.org/10.4230/LIPICS.TY...

    work page doi:10.4230/lipics.types.2013.107 2013

  8. [8]

    thesis, Universit´ e Nice Sophia Antipolis (2015)

    Bordg, A.,On lifting univalence to the equivariant setting, Ph.D. thesis, Universit´ e Nice Sophia Antipolis (2015). https://arxiv.org/abs/1512.04083

    work page arXiv 2015

  9. [9]

    Preprint

    Bordg, A.,On the inadequacy of the projective structure with respect to the univalence axiom(2020). Preprint. https://arxiv.org/abs/1712.02652

    work page arXiv 2020

  10. [10]

    A Coq formal proof of the Lax–Milgram theorem

    Boulier, S., P.-M. P´ edrot and N. Tabareau,The next 700 syntactical models of type theory, in:Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), pages 182–194, ACM (2017). https://doi.org/10.1145/3018610.3018620

    work page doi:10.1145/3018610.3018620 2017

  11. [11]

    Capriotti, P. and N. Kraus,Univalent higher categories via complete semi-Segal types, Proceedings of the ACM on Programming Languages2, pages 1–29 (2017). https://doi.org/10.1145/3158132

    work page doi:10.1145/3158132 2017

  12. [12]

    , copyright =

    Carboni, A., S. Lack and R. Walters,Introduction to extensive and distributive categories, Journal of Pure and Applied Algebra84, pages 145–158 (1993). https://doi.org/10.1016/0022-4049(93)90035-r

    work page doi:10.1016/0022-4049(93)90035-r 1993

  13. [13]

    W.,Generalised Algebraic Theories and Contextual Categories, Ph.D

    Cartmell, J. W.,Generalised Algebraic Theories and Contextual Categories, Ph.D. thesis, Oxford University (1978)

    1978

  14. [14]

    Clairambault, P. and P. Dybjer,The biequivalence of locally cartesian closed categories and Martin-L¨ of type theories, Mathematical Structures in Computer Science24, page e240606 (2014). https://doi.org/10.1017/S0960129513000881

    work page doi:10.1017/s0960129513000881 2014

  15. [15]

    Coquand, S

    Cohen, C., T. Coquand, S. Huber and A. M¨ ortberg,Cubical type theory: A constructive interpretation of the univalence axiom, in: T. Uustalu, editor,21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 5:1–5:34, Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Inf...

    work page doi:10.4230/lipics.types.2015.5 2015

  16. [16]

    Constructive sheaf models of type theory

    Coquand, T., F. Ruch and C. Sattler,Constructive sheaf models of type theory, Mathematical Structures in Computer Science31, pages 979–1002 (2021). https://doi.org/10.1017/S0960129521000359

    work page doi:10.1017/s0960129521000359 2021

  17. [17]

    thesis, University of Cambridge (1991)

    de Paiva, V.,The Dialectica Categories, Ph.D. thesis, University of Cambridge (1991). https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-213.pdf

    1991

  18. [18]

    G.,Equivalent form of the univalence axiom, MathOverflow (2013)

    Dorais, F. G.,Equivalent form of the univalence axiom, MathOverflow (2013). Version: 2013-06-22. https://mathoverflow.net/q/134449

    2013

  19. [19]

    https://doi.org/10.1007/3-540-61780-9_66

    Dybjer, P.,Internal type theory, in:Types for Proofs and Programs: International Workshop TYPES ’95, Torino, Italy, pages 120–134, Springer Berlin Heidelberg (1996). https://doi.org/10.1007/3-540-61780-9_66

    work page doi:10.1007/3-540-61780-9_66 1996

  20. [20]

    Frumin, D. and B. van den Berg,A homotopy-theoretic model of function extensionality in the effective topos, Mathematical Structures in Computer Science29, pages 588–614 (2018), ISSN 1469-8072. https://doi.org/10.1017/s0960129518000142

    work page doi:10.1017/s0960129518000142 2018

  21. [21]

    Gambino, N. and J. Kock,Polynomial functors and polynomial monads, Mathematical Proceedings of the Cambridge Philosophical Society154, pages 153–192 (2013). https://doi.org/10.1017/s0305004112000394

    work page doi:10.1017/s0305004112000394 2013

  22. [22]

    https://doi.org/10.1007/bfb0014052

    Ghani, N.,βη-Equality for coproducts, pages 171–185, Lecture Notes in Computer Science, Springer Berlin Heidelberg (1995). https://doi.org/10.1007/bfb0014052

    work page doi:10.1007/bfb0014052 1995

  23. [23]

    https://doi.org/10.1111/j.1746-8361.1958.tb01464.x

    G¨ odel, K.,¨Uber eine bisher noch nicht ben¨ utzte Erweiterung des finiten Standpunktes, Dialectica12, pages 280–287 (1958). https://doi.org/10.1111/j.1746-8361.1958.tb01464.x

    work page doi:10.1111/j.1746-8361.1958.tb01464.x 1958

  24. [24]

    thesis, Aarhus University (2023)

    Gratzer, D.,Syntax and semantics of modal type theory, Ph.D. thesis, Aarhus University (2023). https://pure.au.dk/portal/en/publications/syntax-and-semantics-of-modal-type-theory

    2023

  25. [25]

    Gratzer, D., G. A. Kavvos, A. Nuyts and L. Birkedal,Multimodal dependent type theory, Log. Methods Comput. Sci.17 (2021). https://doi.org/10.46298/LMCS-17(3:11)2021

    work page doi:10.46298/lmcs-17(3:11)2021 2021

  26. [26]

    Hofmann, M. and T. Streicher,The groupoid interpretation of type theory, in:Twenty-five years of constructive type theory (Venice, 1995), volume 36 ofOxford Logic Guides, pages 83–111, Oxford Univ. Press, New York (1998). https://doi.org/10.1093/oso/9780198501275.003.0008

    work page doi:10.1093/oso/9780198501275.003.0008 1995

  27. [27]

    Jacobs, B.,Categorical logic and type theory, volume 141 ofStudies in Logic and the Foundations of Mathematics, North- Holland Publishing Co., Amsterdam (1999), ISBN 0-444-50170-3

    1999

  28. [28]

    Gluing for Type Theory

    Kaposi, A., S. Huber and C. Sattler,Gluing for type theory, in:4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 25:1–25:19, Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik (2019). https://doi.org/10.4230/LIPICS.FSCD.2019.25

    work page doi:10.4230/lipics.fscd.2019.25 2019

  29. [29]

    Kapulkin, K. and P. L. Lumsdaine,The simplicial model of univalent foundations (after Voevodsky), J. Eur. Math. Soc. (JEMS)23, pages 2071–2126 (2021), ISSN 1435-9855,1435-9863. https://doi.org/10.4171/JEMS/1050

    work page doi:10.4171/jems/1050 2071

  30. [30]

    Agda formalization of construction by Von Glehn [50]

    Kov´ acs, A.,polynomial-model(2020). Agda formalization of construction by Von Glehn [50]. https://github.com/AndrasKovacs/polynomial-model

    2020

  31. [31]

    Agda formalization of construction by P´ edrot and Tabareau [35]

    Kov´ acs, A.,antifunext(2024). Agda formalization of construction by P´ edrot and Tabareau [35]. https://github.com/AndrasKovacs/antifunext

    2024

  32. [32]

    K.,The Dialectica Models of Type Theory, Ph.D

    Moss, S. K.,The Dialectica Models of Type Theory, Ph.D. thesis, University of Cambridge (2018). https://doi.org/10.17863/CAM.28036

    work page doi:10.17863/cam.28036 2018

  33. [33]

    Moss, S. K. and T. von Glehn,Dialectica models of type theory, in: A. Dawar and E. Gr¨ adel, editors,Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 739–748, ACM (2018). https://doi.org/10.1145/3209108.3209207

    work page doi:10.1145/3209108.3209207 2018

  34. [34]

    Orton, I. and A. M. Pitts,Axioms for modelling cubical type theory in a topos, Logical Methods in Computer Science14 (2018). https://doi.org/10.23638/lmcs-14(4:23)2018 19 Cavallo, H¨ofer

    work page doi:10.23638/lmcs-14(4:23)2018 2018

  35. [35]

    P´ edrot, P. and N. Tabareau,Failure is not an option: An exceptional type theory, in: A. Ahmed, editor,Programming Languages and Systems - 27th European Symposium on Programming (ESOP 2018), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2018), volume 10801 ofLecture Notes in Computer Science, pages 245–271, Spri...

    work page doi:10.1007/978-3-319-89884-1_9 2018

  36. [36]

    https://doi.org/10.1017/9781108933568

    Rijke, E.,Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (2025), ISBN 9781108933568. https://doi.org/10.1017/9781108933568

    work page doi:10.1017/9781108933568 2025

  37. [37]

    https://doi.org/10.1145/3009837.3009901

    Scherer, G.,Deciding equivalence with sums and the empty type, in:Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 374–386, Association for Computing Machinery (ACM) (2017). https://doi.org/10.1145/3009837.3009901

    work page doi:10.1145/3009837.3009901 2017

  38. [38]

    Blog post on the Homotopy Type Theory blog

    Shulman, M.,Universal properties without function extensionality(2014). Blog post on the Homotopy Type Theory blog. https://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/

    2014

  39. [39]

    All $(\infty,1)$-toposes have strict univalent universes

    Shulman, M.,All(∞,1)-toposes have strict univalent universes(2019). Preprint. https://arxiv.org/abs/1904.07004

    work page Pith review arXiv 2019

  40. [40]

    Kov´ acset al.,Strong eta-rules for functions on sum types, Proof Assistants StackExchange (2022)

    Shulman, M., A. Kov´ acset al.,Strong eta-rules for functions on sum types, Proof Assistants StackExchange (2022). Version: 2022-12-10. https://proofassistants.stackexchange.com/q/1885

    2022

  41. [41]

    L.,Groupoidal realizability for intensional type theory, Mathematical Structures in Computer Science34, pages 911–944 (2024)

    Speight, S. L.,Groupoidal realizability for intensional type theory, Mathematical Structures in Computer Science34, pages 911–944 (2024). https://doi.org/10.1017/s0960129524000343

    work page doi:10.1017/s0960129524000343 2024

  42. [42]

    https://www2.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf

    Streicher, T.,Investigations into Intensional Type Theory, Habilitation thesis, Ludwig-Maximilians-Universit¨ at M¨ unchen (1993). https://www2.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf

    1993

  43. [43]

    W.,A categorical formulation of Kraus’ paradox(2024)

    Swan, A. W.,A categorical formulation of Kraus’ paradox(2024). Preprint. https://arxiv.org/abs/2403.17961

    work page arXiv 2024

  44. [44]

    https://homotopytypetheory.org/book

    The Univalent Foundations Program,Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study (2013). https://homotopytypetheory.org/book

    2013

  45. [45]

    Dybjer, J

    Uemura, T.,Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing, in: P. Dybjer, J. E. Santo and L. Pinto, editors,24th International Conference on Types for Proofs and Programs (TYPES 2018), volume 130 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 7:1–7:20, Schloss Dagstuhl–Leibniz- Zentru...

    work page doi:10.4230/lipics.types.2018.7 2018

  46. [46]

    https://doi.org/10.1016/j.apal.2020.102793

    van den Berg, B.,Univalent polymorphism, Annals of Pure and Applied Logic171, page 102793 (2020). https://doi.org/10.1016/j.apal.2020.102793

    work page doi:10.1016/j.apal.2020.102793 2020

  47. [47]

    https://github.com/UniMath/Foundations/blob/master/Proof_of_Extensionality/funextfun.v

    Voevodsky, V.,Univalence axiom and functional extensionality. https://github.com/UniMath/Foundations/blob/master/Proof_of_Extensionality/funextfun.v

  48. [48]

    https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/univalent_foundations_project.pdf

    Voevodsky, V.,Univalent Foundations Project (a modified version of an NSF grant application)(2010). https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/univalent_foundations_project.pdf

    2010

  49. [49]

    Mailing list discussion

    Voevodsky, V.et al.,coinductives(2014). Mailing list discussion. https://groups.google.com/g/homotopytypetheory/c/tYRTcI2Opyo/m/PIrI6t5me-oJ

    2014

  50. [50]

    thesis, University of Cambridge (2015)

    Von Glehn, T.,Polynomials and models of type theory, Ph.D. thesis, University of Cambridge (2015). https://doi.org/10.17863/CAM.16245

    work page doi:10.17863/cam.16245 2015

  51. [51]

    thesis, Universit´ e de Nantes (2020)

    Winterhalter, T.,Formalisation and Meta-Theory of Type Theory, Ph.D. thesis, Universit´ e de Nantes (2020). https://theses.hal.science/tel-05425836 20

    2020