Completions of Implicative Assemblies

Abstract

We continue our work on implicative assemblies by investigating under which circumstances a subset $M\subseteq \mathcal{S}$ gives rise to a lex full subcategory ${\mathbf{Asm}}_M$ of the quasitopos ${\mathbf{Asm}}_{\mathcal{A}}$ of all assemblies such that $({\mathbf{Asm}}_M{)}_{reg/lex}\simeq {\mathbf{Asm}}_{\mathcal{A}}$. We establish a characterisation. Furthermore, this latter is relevant to the study of ${\mathbf{Asm}}_M$'s ex/lex-completion.