Geodesic
The Theory of an Arbitrary Higher λ-Model
Bulletin of the Section of Logic, Tome 52 (2023) no. 1, pp. 39-58.

Voir la notice de l'article provenant de la source Library of Science

One takes advantage of some basic properties of every homotopic λ-model (e.g. extensional Kan complex) to explore the higher βη-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 λ-terms, whose equality rules would be contained in the theory of any λ-homotopic model.
Keywords: higher lambda calculus, homotopic lambda model, Kan complex reflexive, higher conversion, homotopy type-free theory 
@article{BSL_2023_52_1_a2,
     author = {Mart{\'\i}nez-Rivillas, Daniel O. and de Queiroz, Ruy J. G. B.},
     title = {The {Theory} of an {Arbitrary} {Higher} {\ensuremath{\lambda}-Model}},
     journal = {Bulletin of the Section of Logic},
     pages = {39--58},
     publisher = {mathdoc},
     volume = {52},
     number = {1},
     year = {2023},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2023_52_1_a2/}
}
TY  - JOUR
AU  - Martínez-Rivillas, Daniel O.
AU  - de Queiroz, Ruy J. G. B.
TI  - The Theory of an Arbitrary Higher λ-Model
JO  - Bulletin of the Section of Logic
PY  - 2023
SP  - 39
EP  - 58
VL  - 52
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2023_52_1_a2/
LA  - en
ID  - BSL_2023_52_1_a2
ER  - 
%0 Journal Article
%A Martínez-Rivillas, Daniel O.
%A de Queiroz, Ruy J. G. B.
%T The Theory of an Arbitrary Higher λ-Model
%J Bulletin of the Section of Logic
%D 2023
%P 39-58
%V 52
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2023_52_1_a2/
%G en
%F BSL_2023_52_1_a2
Martínez-Rivillas, Daniel O.; de Queiroz, Ruy J. G. B. The Theory of an Arbitrary Higher λ-Model. Bulletin of the Section of Logic, Tome 52 (2023) no. 1, pp. 39-58. http://geodesic.mathdoc.fr/item/BSL_2023_52_1_a2/

[1] 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.

[2] J. Lurie, Higher Topos Theory, Princeton University Press, Princeton and Oxford (2009) | DOI

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

[4] 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

[5] 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

[6] 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