Implicative Assemblies
From MaRDI portal
Publication:6433776
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)
