The Theory of an Arbitrary Higher λ-Model

2021/11/13 by Martínez-Rivillas, Daniel O., de Queiroz, Ruy J. G. B. · 1 citation
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2111.07092

Abstract

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.

Cited by

• The K_∞ Homotopy λ-Model

Related

• The ∞-groupoid generated by an arbitrary topological λ-model
• Towards a Homotopy Domain Theory
• The K_∞ Homotopy λ-Model
• Solving Homotopy Domain Equations
• Homotopy Type Theory: A synthetic approach to higher equalities