The Theory of an Arbitrary Higher \(\lambda\)-Model

Daniel O. Martínez-Rivillas; Ruy J. G. B. de Queiroz

doi:10.18778/0138-0680.2023.11

Authors

Daniel O. Martínez-Rivillas Universidade Federal de Pernambuco, Centro de Informática, Av. Jornalista Aníbal Fernandes, s/n Recife, Pernambuco, Brazil
Ruy J. G. B. de Queiroz Universidade Federal de Pernambuco, Centro de Informática, Av. Jornalista Aníbal Fernandes, s/n Recife, Pernambuco, Brazil

DOI:

https://doi.org/10.18778/0138-0680.2023.11

Keywords:

higher lambda calculus, homotopic lambda model, Kan complex reflexive, higher conversion, homotopy type-free theory

Abstract

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.
Google Scholar

J. Lurie, Higher Topos Theory, Princeton University Press, Princeton and Oxford (2009), DOI: https://doi.org/10.1515/9781400830558
Google Scholar DOI: https://doi.org/10.1515/9781400830558

D. Martínez-Rivillas, R. de Queiroz, Solving Homotopy Domain Equations, arXiv:2104.01195, (2021).
Google Scholar

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
Google Scholar 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
Google Scholar 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
Google Scholar