The category of implicative algebras and realizability
classification
🧮 math.LO
keywords
algebrascategoriesimplicativekrivinerealizabilityabstractadjunctionalgebraic
read the original abstract
In this paper we continue with the algebraic study of Krivine's realizability, refining some of the authors' previous constructions by introducing two categories, with objects the abstract Krivine structures and the implicative algebras respectively. These categories are related by an adjunction whose existence clarifies many aspects of the theory previously established.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.