nLab assembly

Idea

An assembly is a mathematical structure on a partial combinatory algebra used to construct realizability toposes and used for the categorical semantics of impredicative universes in type theory.

Definition

Given a partial combinatory algebra $A$, an $A$-valued assembly $X$ consists of a set ${|X|}$ and any one of these equivalent structures:

• a family of sets $(E_X(x))_{x \in |X|}$ such that each $E_X(x)$ is an inhabited subset of $A$ for all $x \in A$.

• a multivalued function $E_X \colon {|X|} \to P_{\ge 1}(A)$ from $|X|$ to $A$, where $P_{\ge 1}(A)$ denotes the set of inhabited subsets of $A$.

• an entire relation $E_X(x, a)$ indexed by $x \in |X|$ and $a \in A$.

Remark

The assemblies or $\omega$-sets of Uemura 2019 are precisely the $\mathbb{N}$-valued assemblies.

Given a partial combinatory algebra $A$, an assembly is partitioned if, for each definition above respectively,

• each $E_X(x)$ is a singleton for all $x \in |X|$,

• the multivalued function $E_X$ takes values in singletons, i.e. is a function ${|X|} \to A$.

• the entire relation $E_X$ is a functional relation.

The category of assemblies

Let $A$ be a partial combinatory algebra.

Definition

A morphism $X \to Y$ between $A$-valued assemblies is a function $f \colon {|X|} \to {|Y|}$ for which there exists $a \in A$ such that for all $x\in X$ and $b\in E_X(x)$, $a\cdot b$ is defined and belongs to $E_Y(f(x))$.

Definition

The category of $A$-valued assemblies is the category whose objects are $A$-valued assemblies, and whose morphisms are morphisms as defined above.

The category of $A$-valued assemblies is denoted $\mathrm{Asm}(A)$ (Maietti, Pasquali, & Rosolini 2019, Awodey & Emmenegger 2025) or $\mathrm{Ass}(A)$ (Vermeeren 2009). The category of partitioned $A$-valued assemblies is denoted $\mathrm{PAsm}(A)$ (Frey 2014) or $\mathbb{P}$ (Awodey & Emmenegger 2025) or $\mathrm{PAss}(A)$.

Theorem

$\mathrm{Asm}(A)$ and $\mathrm{PAsm}(A)$ are finitary lextensive. Moreover, $\mathrm{Asm}(A)$ is regular and locally cartesian closed.

Theorem

The realizability topos is the ex/reg completion of $\mathrm{Asm}(A)$.

Theorem

In the presence of the axiom of choice, $\mathrm{Asm}(A)$ is the reg/lex completion of $\mathrm{PAsm}(A)$ and the realizability topos is the ex/lex completion of $\mathrm{PAsm}(A)$.

Remark

A general result about the ex/lex completion $C_{ex/lex}$ of a left exact category $C$ is that it has enough regular projectives, meaning objects $P$ such that $\hom(P, -) \colon C_{ex/lex} \to Set$ preserves regular epis. In fact, the regular projective objects coincide with the objects of $C$ (as a subcategory of $C_{ex/lex}$). Of course, when $C_{ex/lex}$ is a topos, where every epi is regular, this means $C_{ex/lex}$ has enough projectives, or satisfies (external) COSHEP. It also satisfies internal COSHEP, since binary products of projectives, i.e., products of objects of $C$, are again objects of $C$ (see this result).

Remark

The fact that a realizability topos is an ex/lex completion depends on the axiom of choice for Set, since it requires the partitioned assemblies to be projective objects therein. In the absence of the axiom of choice, the projective objects in a realizability topos are the (isomorphs of) partitioned assemblies whose underlying set is projective in Set. Thus, if COSHEP holds in Set, then a realizability topos is the ex/wlex completion of the category of such “projective partitioned assemblies” (wlex because this category may not have finite limits, only weak finite limits). Without some choice principle, the realizability topos may not be an ex/wlex completion at all; but it is still an ex/reg completion of $\mathrm{Asm}(A)$.

Related concepts

• realizability

• realizability topos

• impredicative polymorphism

References

• Stijn Vermeeren, Realizability Toposes, 2009 (pdf)

• Jonas Frey, Characterizing partitioned assemblies and realizability toposes (arXiv:1404.6997)

• Taichi Uemura, Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing, in 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) (doi:10.4230/LIPIcs.TYPES.2018.7, arXiv:1803.06649)

• Maria Emilia Maietti, Fabio Pasquali, Giuseppe Rosolini, Elementary Quotient Completions, Church’s Thesis, and Partioned Assemblies, Logical Methods in Computer Science, Volume 15, Issue 2 (June 25, 2019). [doi:10.23638/LMCS-15(2:21)2019, arXiv:1802.06400]

• Steve Awodey, Jacopo Emmenegger, Toward the effective 2-topos [arXiv:2503.24279]