Categorical Realizability

An assembly over a pca $\mathcal{A}$ is a set $X$ together with a relation $\Vdash$ between $\mathcal{A}$ and $X$ such that for all $x \in X$ , there exists at least one element $a\in\mathcal{A}$ with $a\Vdash x$ .

The relation $a \Vdash x$ pronounced " $a$ realizes $x$ " or " $a$ is a realizer of $x$ ". $a$ can be thought as an implementation of $x \in X$ in the pca $\mathcal{A}$ .

Notation $(|X|,\Vdash_X)$ [local-0]

Given an assembly $X$ , we wrote $|X|$ for its underlying set and $\Vdash_X$ for its relation between $\mathcal{A}$ and $|X|$ .

Example encode booleans [local-1]

The assembly of booleans is defined as

|2| := \{ 0,1 \} \quad\text{with realizers}\quad \bold{false}\Vdash_2 0 \;\text{and}\; \bold{true}\Vdash_2 1

Example encode natural numbers [local-2]

The assembly of natural numbers is defined as

|N| := \N \quad\text{with realizers}\quad \bar{n}\Vdash_N n \;\text{for each}\;n\in\N

Example $\mathcal{K}_1$ model [local-3]

A $\mathcal{K}_1$ model as pca and the set of all Turing computable functions:

|X| := \{ f : \N \rightharpoonup \N \mid f\ \text{is Turing computable} \} \quad\text{and}\quad m \Vdash_X f \iff \varphi_m = f

Definition. Assembly over pca [math-YOTV]

Notation (∣X∣,⊩X)(|X|,\Vdash_X)(∣X∣,⊩X​) [local-0]

Example encode booleans [local-1]

Example encode natural numbers [local-2]

Example K1\mathcal{K}_1K1​ model [local-3]

Notation $(|X|,\Vdash_X)$ [local-0]

Example $\mathcal{K}_1$ model [local-3]