The Theory of an Arbitrary Higher -Model

DOI10.18778/0138-0680.2023.11MaRDI QIDQ6119353zbMATH OpenOpenAlexFDO

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

Publication date 29 February 2024

Published in Bulletin of the Section of Logic (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://arxiv.org/abs/2111.07092

zbMATH Keywords

higher conversionhigher lambda calculushomotopic lambda modelhomotopy type-free theoryKan complex reflexive

Mathematics Subject Classification ID

Logic in computer science (03B70)

Abstract: One takes advantage of some basic properties of every homotopic $lambda$-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 $lambda$-terms, whose equality rules would be contained in the theory of any $lambda$-homotopic model.

Cites work

• -groupoid generated by an arbitrary topological -model
• Higher Topos Theory (AM-170)
• Towards a homotopy domain theory

Cited in

(2)

• Computational paths -- a weak groupoid
• The K_ homotopy -model

This page was built for publication: The Theory of an Arbitrary Higher \(\lambda\)-Model

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6119353)