Advertisement

On a Model Invariance Problem in Homotopy Type Theory

  • Anthony BordgEmail author
Open Access
Article

Abstract

In this article, the author endows the functor category \([\mathbf {B}(\mathbb {Z}_2),\mathbf {Gpd}]\) with the structure of a type-theoretic fibration category with a univalent universe, using the so-called injective model structure. This gives a new model of Martin-Löf type theory with dependent sums, dependent products, identity types and a univalent universe. This model, together with the model (developed by the author in another work) in the same underlying category and with the same universe, which turns out to be provably not univalent with respect to projective fibrations, provide an example of two Quillen equivalent model categories that host different models of type theory. Thus, we provide a counterexample to the model invariance problem formulated by Michael Shulman.

Keywords

Univalent Foundations Homotopy Type Theory Univalence Axiom Type-theoretic fibration category Quillen model category Injective model structure Groupoid Groupoid model Universe Model invariance problem 

Notes

References

  1. 1.
    Bordg, A.: On lifting univalence to the equivariant setting. Ph.D. Thesis, Université Nice Sophia Antipolis (2015). arXiv:1512.04083
  2. 2.
    Bordg, A.: On the inadequacy of the projective structure with respect to the Univalence Axiom (2017). arXiv:1712.02652
  3. 3.
    Bordg, A.: Univalent foundations and the UniMath library (2017). arXiv:1710.02723
  4. 4.
    Hirschhorn, P.S.: Model Categories and Their Localizations, Volume 99 of Mathematical Surveys and Monographs. American Mathematical Society, Providence (2003)Google Scholar
  5. 5.
    Lurie, J.: Higher Topos Theory. Number 170 in Annals of Mathematics Studies. Princeton University Press, Princeton (2009)Google Scholar
  6. 6.
    Shulman, M.: The univalence axiom for elegant Reedy presheaves. Homol. Homotopy Appl. 17(2), 81–106 (2015). arXiv:1307.6248
  7. 7.
    Shulman, M.: Univalence for inverse diagrams and homotopy canonicity. Math Struct Comput Sci. 25, 1203–1277 (2015). arXiv:1203.3253
  8. 8.
    Shulman, M.: The univalence axiom for EI diagrams. Homol. Homotopy Appl. 19(2), 219–249 (2017). arXiv:1508.02410

Copyright information

© The Author(s) 2019

OpenAccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

Authors and Affiliations

  1. 1.Department of Computer Science and TechnologyUniversity of CambridgeCambridgeUK

Personalised recommendations