Implicative Assemblies

TL;DR

This paper introduces implicative assemblies, a new categorical structure based on implicative algebras, unifying various logical frameworks and demonstrating that the resulting category is a quasitopos with NNO.

Contribution

It defines implicative assemblies over implicative algebras and proves that their category forms a quasitopos with a natural number object.

Findings

Asm is a quasitopos with NNO

Implicative assemblies unify classical and intuitionistic realizability and forcing

The category Asm has tracked set-theoretical functions as morphisms

Abstract

Implicative algebras, recently discovered by Miquel, are combinatorial structures unifying classical and intuitionistic realizability as well as forcing. In this paper we introduce implicative assemblies as sets valued in the separator of an underlying implicative algebra. Given a fixed implicative algebra A, implicative assemblies over A organise themselves in a category Asm with tracked set-theoretical functions as morphisms. We show that Asm is a quasitopos with NNO.