{"id":"arxiv/2607.23430","url":"https://arxiv.org/abs/2607.23430","tags":["math.LO","cs.LO","math.CT"],"score":0,"title":"Dialectica Categories over Heyting Algebras","domain":"math.LO","source":"arxiv","authors":["Colin Bloomfield","Peter Jipsen","Valeria de Paiva"],"reviews":0,"subject":"math.LO","summary":"Categorification---the process of constructing a categorical model of a piece of mathematics---often identifies a common abstraction that connects formerly unrelated but known structures. In the case of de Paiva's categorification of Gödel's Dialectica interpretation, we find that its specialization to partial orders produces (functorial) embeddings of Heyting algebras into residuated lattices that appear to have been overlooked. For the non-categorical audience, we present this specialization and take care to reproduce the original proofs in the algebraic setting. Along the way we obtain…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-07-26","reactions":{}}