Implicative Assemblies
From MaRDI portal
Publication:6433776
arXiv2304.10429MaRDI QIDQ6433776FDOQ6433776
Authors: Félix Castro, Alexandre Miquel, Krzysztof Worytkiewicz
Publication date: 20 April 2023
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.
This page was built for publication: Implicative Assemblies
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6433776)