Implicative Assemblies
Algebraic Topology
2023-04-21 v1
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.
Cite
@article{arxiv.2304.10429,
title = {Implicative Assemblies},
author = {Félix Castro and Alexandre Miquel and Krzysztof Worytkiewicz},
journal= {arXiv preprint arXiv:2304.10429},
year = {2023}
}