Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Arrow algebras

Benno van den Berg, Marcus Briet

TL;DR

Arrow algebras provide a flexible algebraic framework that generalises locales and realizability structures to support topos construction via triposes. By weakening the implicative axiom and introducing a strong separation by a nucleus, they yield a robust path from algebraic data to arrow triposes and toposes, including subtriposes through nuclei. The paper establishes Lambda-term interpretation in strong arrow algebras, derives preHeyting and tripos structures, and demonstrates practical applications to modified realizability and related topos constructions. This unifies and extends prior work on implicative algebras, pcas, and PERs, offering a versatile toolkit for generating toposes and exploring realizability-like phenomena within a coherent algebraic setting.

Abstract

In this paper we introduce arrow algebras, simple algebraic structures which induce elementary toposes through the tripos-to-topos construction. This includes localic toposes as well as various realizability toposes, in particular, those realizability toposes which are obtained from partial combinatory algebras. Since there are many examples of arrow algebras and arrow algebras have a number of closure properties, including a notion of subalgebra given by a nucleus, arrow algebras provide a flexible tool for constructing toposes; we illustrate this by providing some general tools for creating toposes for Kreisel's modified realizability.

Arrow algebras

TL;DR

Arrow algebras provide a flexible algebraic framework that generalises locales and realizability structures to support topos construction via triposes. By weakening the implicative axiom and introducing a strong separation by a nucleus, they yield a robust path from algebraic data to arrow triposes and toposes, including subtriposes through nuclei. The paper establishes Lambda-term interpretation in strong arrow algebras, derives preHeyting and tripos structures, and demonstrates practical applications to modified realizability and related topos constructions. This unifies and extends prior work on implicative algebras, pcas, and PERs, offering a versatile toolkit for generating toposes and exploring realizability-like phenomena within a coherent algebraic setting.

Abstract

In this paper we introduce arrow algebras, simple algebraic structures which induce elementary toposes through the tripos-to-topos construction. This includes localic toposes as well as various realizability toposes, in particular, those realizability toposes which are obtained from partial combinatory algebras. Since there are many examples of arrow algebras and arrow algebras have a number of closure properties, including a notion of subalgebra given by a nucleus, arrow algebras provide a flexible tool for constructing toposes; we illustrate this by providing some general tools for creating toposes for Kreisel's modified realizability.
Paper Structure (32 sections, 43 theorems, 127 equations)

This paper contains 32 sections, 43 theorems, 127 equations.

Table of Contents

  1. Introduction
  2. Contributions
  3. Related work
  4. Contents.
  5. Acknowledgements.
  6. Implicative algebras
  7. Definition
  8. Examples
  9. Locales
  10. Total combinary algebras
  11. Implicative triposes
  12. Arrow algebras
  13. Definition
  14. Examples
  15. Implicative algebras
  16. ...and 17 more sections

Key Result

Theorem 2.11

(Combinatory completeness) Let $P$ be a pca. There exists an operation which given a non-empty sequence of distinct variables $\overline{x} = x_1,\ldots,x_n$, a variable $y$ and a term $t(\overline{x}, y)$ over $P$ with all free variables among $\overline{x}, y$, produces an element $\lambda^* \over

Theorems & Definitions (131)

  • Definition 2.1
  • Remark 2.2
  • Definition 2.3
  • Definition 2.4
  • Remark 2.5
  • Definition 2.6
  • Remark 2.7
  • Definition 2.8
  • Definition 2.9
  • Definition 2.10
  • ...and 121 more