Ir al contenido

Documat

Kripke-Joyal forcing for type theory and uniform fibrations

  • Steve Awodey [3] ; Nicola Gambino [1] ; Sina Hazratpour [2]
    1. [1] University of Manchester

      University of Manchester

      Reino Unido

    2. [2] Johns Hopkins University

      Johns Hopkins University

      Estados Unidos

    3. [3] Departments of Philosophy and Mathematics, USA
    Mostrar afiliaciones +
  • Localización: Selecta Mathematica, New Series, ISSN 1022-1824, Vol. 30, Nº. 4, 2024, págs. 1-70
  • Idioma: inglés
  • DOI: 10.1007/s00029-024-00962-2
  • Enlaces
  • Resumen

    • We introduce a new method for precisely relating algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory

  • Referencias bibliográficas
    • Angiuli, C., Brunerie, G., Coquand, T., Harper, R., Hou, K., Licata, D.: Syntax and models of cartesian cubical type theory. Math. Struct....
    • Awodey, S.: A cubical model of homotopy type theory. Ann. Pure Appl. Log. 169(12), 1270–1294 (2018)
    • Awodey, S.: Natural models of homotopy type theory. Math. Struct. Comput. Sci. 28(2), 241–286 (2018)
    • Awodey, S.: Cartesian cubical model categories (2023). arXiv:2305.00893
    • Awodey, S., Bauer, A.: Propositions as [types]. J. Log. Comput. 14(4), 447–471 (2004)
    • Awodey, S., Rabe, F.: Kripke semantics for Martin-Löf’s extensional type theory. Log. Methods Comput. Sci. 7(3), 1–25 (2011)
    • Awodey, S., Warren, M.A.: Homotopy theoretic models of identity types. Math. Proc. Camb. Philos. Soc. 146, 45–55 (2009)
    • Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions, Morgan &...
    • Bezem, M., Coquand, T., Huber, S.: A model of type theory in cubical sets. In: Matthes, R., Schubert, A. (eds.) 19th International Conference...
    • Boileau, A., Joyal, A.: La logique des topos. J. Symb. Log. 45(1), 6–16 (1981)
    • Bourke, J., Garner, R.: Algebraic weak factorisation systems I: accessible AWFS. J. Pure Appl. Algebra 220, 108–147 (2016)
    • Bourke, J., Garner, R.: Algebraic weak factorisation systems II: categories of weak maps. J. Pure Appl. Algebra 220, 148–174 (2016)
    • Buchholtz, U., Morehouse, E.: Varieties of cubical sets. In: Höfner, P.P., Pous, D., Struth, G. (eds.) Relational and Algebraic Methods in...
    • Cisinski, D.-C.: Les préfaisceaux comme modèles des types d’homotopie. Astérisque 308, xxiv+392 (2006)
    • Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom. In Uustalu, T....
    • Coquand, T.: A cubical type theory, 2015. Slides of an invited lecture given at the Mathematical Foundations of Programming Semantics conference,...
    • Coquand, T.: Univalent type theory and modular formalization of mathematics, 2017. Slides of a talk given at the Big Proof conference, Isaac...
    • Gambino, N., Garner, R.: The identity type weak factorisation system. Theor. Comput. Sci. 409, 94–109 (2008)
    • Gambino, N., Henry, S.: Towards a constructive simplicial model of Univalent Foundation. J. Lond. Math. Soc. 105(2), 1073–1109 (2022)
    • Gambino, N., Kock, J.: Polynomial functors and polynomial monads. Math. Proc. Camb. Philos. Soc. 154(1), 153–192 (2013)
    • Gambino, N., Larrea, M.F.: Models of Martin-Löf type theory from algebraic weak factorisation systems. J. Symb. Log. 88(1), 242–289 (2023)
    • Gambino, N., Sattler, C.: The Frobenius condition, right properness, and uniform fibrations. J. Pure Appl. Algebra 221(12), 3027–3068 (2017)
    • Garner, R.: Understanding the small object argument. Appl. Categ. Struct. 17(3), 247–285 (2009)
    • Grandis, M., Tholen, W.: Natural weak factorisation systems. Arch. Math. 42, 397–408 (2006)
    • Henry, S.: A constructive account of the Kan–Quillen model structure and of Kan’s Ex∞ functor (2019). ArXiv:1905.06160
    • Hofmann, M.: On the interpretation of type theory in locally cartesian closed categories. In Computer Science Logic (CSL ’94), volume 933...
    • Hofmann, M.: Syntax and semantics of dependent types. In Dybjer, P., Pitts, A.M. (eds.) Semantics and Logics of Computation. Publications...
    • Hofmann, M., Streicher, T.: Lifting Grothendieck universes. Available from the second-named author’s web page here (1997)
    • Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium. Oxford University Press (2002)
    • Joyal, A., Moerdijk, I.: Algebraic Set Theory. London Mathematical Society Lecture Note Series, Cambridge University Press (1995)
    • Licata, D.R., Orton, I., Pitts, A.M., Spitters, B.: Internal universes in models of homotopy type theory. In Kirchner, H. (ed.) 3rd International...
    • Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic. A First Introduction to Topos Theory. Universitext, Springer-Verlag, New York (1994)
    • Maietti, M.E.: Modular correspondence between dependent type theories and categories including pretopoi and topoi. Math. Struct. Comput. Sci....
    • Nordström, B., Petersson, K., Smith, J.: Martin-Löf type theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic...
    • Norell, U.: Dependently typed programming in Agda. In Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) Advanced Functional Programming: 6th...
    • Orton, I., Pitts, A.M.: Axioms for modelling cubical type theory in a topos. Log. Methods Comput. Sci. 14(4), 1–33 (2018)
    • Osius, G.: A note on Kripke–Joyal semantics for the internal language of topoi. In Lawvere, F.W., Maurer, C., Wraith, G.C. (eds.) Model Theory...
    • Pitts, A.M.: Categorical logic. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 5, pp....
    • Quillen, D.G.: Homotopical Algebra. Lecture Notes in Mathematics, vol. 43. Springer, Cham (1967)
    • Riehl, E.: Categorical Homotopy Theory. Cambridge University Press, Cambridge (2014)
    • Rosolini, G.: Continuity and Effectiveness in Topoi. Ph.D. Thesis, University of Oxford (1986)
    • Sattler, C.: The equivalence extension property and model structures (2017). Available from arXiv:1704.06911
    • Seely, R.A.G.: Local cartesian closed categories and type theory. Math. Proc. Camb. Philos. Soc. 95, 33–48 (1984)
    • Shulman, M.: Stack semantics and the comparison of material and structural set theories (2010). arXiv:1004.3802
    • Shulman, M.: All (∞, 1)-toposes have strict univalent universes (2019). arXiv:1904.07004
    • Swan, A.: An algebraic weak factorisation system on 01-substitution sets: a constructive proof. J. Log. Anal. 8, 1–35 (2016)
    • Swan, A.: Identity types in algebraic model structures and cubical sets (2018). arXiv:1808.00915
    • Swan, A.: Some remarks on locally representable algebraic weak factorisation systems. Talk at the International Category Theory Conference...
    • Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics. North-Holland (1988)
    • The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book. Institute...
    • van den Berg, B., Faber, E.: Effective Kan fibrations in simplicial sets (2020). arXiv:2009.12670
    • Voevodsky, V.: An experimental library of formalized mathematics based on the univalent foundations. Math. Struct. Comput. Sci. 25(5), 1278–1294...
    • van den Berg, B., Garner, R.: Topological and simplicial models of identity types. ACM Trans. Comput. Log. 13(1), 1–44 (2012)
Fundación Dialnet

Mi Documat

Opciones de artículo

Opciones de compartir

Opciones de entorno