4 papers
A Theory of a Two-Dimensional Typed Lambda Calculus
Daniel O. Martínez-Rivillas, Arthur F. Ramos, Ruy J. G. B. de Queiroz
We present a typed two-dimensional -calculus whose equality evidence is \emph{computational}: a path between two terms is an explicit finite sequence of one-step conversions (th…
Recursive Completion in Higher K-Models: Front-Seed Semantics, Proof-Relevant Witnesses, and the K-Infinity Model
Daniel O. Martinez-Rivillas, Arthur F. Ramos, Ruy J. G. B. de Queiroz
Martinez-Rivillas and de Queiroz gave extensional Kan semantics for the untyped lambda-calculus and later constructed the concrete K-infinity homotopy-model. The two main mathemati…
The Homotopy -Model
Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz
We extend the complete ordered set Dana Scott's to a complete weakly ordered Kan complex , with properties that guarantee the non-equivalence of the interpreta…
The Theory of an Arbitrary Higher -Model
Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz
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 o…