HEXAGONbeta

Isomorphism Loci and Coherence in Equivalence Extension

Primarily human-written textHuman understanding: all partsmath.CT — Category Theorymath.AT — Algebraic Topologymath.LO — Logic

Contributed by Zhenyu Sun ↗

Version 1 / Nov 12, 2026 / CC BY 4.0

Abstract

We study the restriction data carried by dependent-product extension along a monomorphism. In a locally cartesian closed category, the extended map is an isomorphism after a change of base if and only if the input map is an isomorphism on the restricted base. In a topos, its isomorphism locus is therefore the universal quantification of the input locus. A terminal characterization gives coherent comparisons for base change and successive extension, together with formulas for intersections and unions. Under explicit homotopical, cartesian, and universe hypotheses, this construction gives equivalence extension and preserves the boundary identifications used to prove fibrancy of a universe. Graph comparisons and strict fillers of a fixed universe boundary are represented by trivially fibrant objects. A single realignment over the comparison object induces a weak equivalence between these parameter objects, and both admit extensions of every finite cubical boundary. A finite-groupoid example shows that graph comparisons cannot be selected naturally under all isomorphisms of unstructured input.

Provenance statement

AI assistance was used for manuscript review, language polishing, and LaTeX typesetting. The author has checked and understood the entire contribution.

References

  1. Steve Awodey, Evan Cavallo, Thierry Coquand, Emily Riehl, and Christian Sattler. The equivariant model structure on Cartesian cubical sets. Advances in Mathematics , 495:110965, 2026. Numbered statements are cited from arXiv:2406.18497v3 (https://arxiv.org/abs/2406.18497v3), 20 April 2026.arXiv
  2. Steve Awodey. Cartesian cubical model categories, 2023. Version 2, 14 July 2023. arXiv:2305.00893v2 (https://arxiv.org/abs/2305.00893v2).arXiv
  3. Steve Awodey. Cartesian Cubical Model Categories , volume 2385 of Lecture Notes in Mathematics . Springer, Cham, 2026. https://doi.org/10.1007/978-3-032-08730-0.DOI
  4. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M ö rtberg. Cubical type theory: A constructive interpretation of the univalence axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015) , volume 69 of Leibniz International Proceedings in Informatics , pages 5:1--5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl--Leibniz-Zentrum f ü r Informatik. https://doi.org/10.4230/LIPIcs.TYPES.2015.5.DOI
  5. Nicola Gambino and Christian Sattler. The Frobenius condition, right properness, and uniform fibrations. Journal of Pure and Applied Algebra , 221(12):3027--3068, 2017. https://doi.org/10.1016/j.jpaa.2017.02.013.DOI
  6. Daniel Gratzer, Michael Shulman, and Jonathan Sterling. Strict universes for Grothendieck topoi. Theory and Applications of Categories , 45(30):1227--1279, 2026. https://tac.mta.ca/tac/volumes/45/30/45-30abs.html.link
  7. Peter T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium , volume 43--44 of Oxford Logic Guides . Oxford University Press, Oxford, 2002. Volumes 1 and 2.
  8. Peter LeFanu Lumsdaine and Michael A. Warren. The local universes model: An overlooked coherence construction for dependent type theories. ACM Transactions on Computational Logic , 16(3):23:1--23:31, 2015. https://doi.org/10.1145/2754931.DOI
  9. Christian Sattler. The equivalence extension property and model structures, 2017. Version 4, 26 August 2017. arXiv:1704.06911v4 (https://arxiv.org/abs/1704.06911v4).arXiv
  10. Michael Shulman. The univalence axiom for elegant Reedy presheaves. Homology, Homotopy and Applications , 17(2):81--106, 2015. https://doi.org/10.4310/HHA.2015.v17.n2.a6.DOI

Version history

  1. v1 · 24 pagesSubmitted by Zhenyu SunInitial depositCurrentNov 12, 2026