The Theory of an Arbitrary Higher \(\lambda\)-Model
DOI:
https://doi.org/10.18778/0138-0680.2023.11Keywords:
higher lambda calculus, homotopic lambda model, Kan complex reflexive, higher conversion, homotopy type-free theoryAbstract
One takes advantage of some basic properties of every homotopic \(\lambda\)-model (e.g. extensional Kan complex) to explore the higher \(\beta\eta\)-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher \(\lambda\)-terms, whose equality rules would be contained in the theory of any \(\lambda\)-homotopic model.
References
R. de Queiroz, A. de Oliveira, A. Ramos, Propositional equality, identity types, and direct computational paths, South American Journal of Logic, vol. 2(2) (2016), pp. 245–296.
J. Lurie, Higher Topos Theory, Princeton University Press, Princeton and Oxford (2009), DOI: https://doi.org/10.1515/9781400830558 DOI: https://doi.org/10.1515/9781400830558
D. Martínez-Rivillas, R. de Queiroz, Solving Homotopy Domain Equations, arXiv:2104.01195, (2021).
D. Martínez-Rivillas, R. de Queiroz, The ∞-groupoid generated by an arbitrary topological λ-model, Logic Journal of the IGPL (also arXiv:1906.05729), vol. 30 (2022), pp. 465–488, URL: https://doi.org/10.1093/jigpal/jzab015 DOI: https://doi.org/10.1093/jigpal/jzab015
D. Martínez-Rivillas, R. de Queiroz, Towards a Homotopy Domain Theory, Archive for Mathematical Logic (also arXiv 2007.15082), (2022), URL: https://doi.org/10.1007/s00153-022-00856-0 DOI: https://doi.org/10.1007/s00153-022-00856-0
C. Rezk, Introduction to Quasicategories, Lecture Notes for course at University of Illinois at Urbana-Champaign (2022), URL: https://faculty.math.illinois.edu/~{}rezk/quasicats.pdf
Downloads
Published
Issue
Section
License
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
How to Cite
