Implicative models of intuitionistic set theory
Logic
2023-01-30 v1 Category Theory
Abstract
In this paper we will show that using implicative algebras one can produce models of intuitionistic set theory generalizing both realizability and Heyting-valued models. This has as consequence that if one assumes the inaccessible cardinal axiom, then every topos which is obtained from a Set-based tripos as the result of the tripos-to-topos construction hosts a model of intuitionistic set theory.
Keywords
Cite
@article{arxiv.2301.11740,
title = {Implicative models of intuitionistic set theory},
author = {Samuele Maschio},
journal= {arXiv preprint arXiv:2301.11740},
year = {2023}
}