Categorical Realizability

First, we define map between assemblies.

Definition assembly map [local-0]

An assembly map from an assembly $X$ to an assembly $Y$ is a function $f : |X| \to |Y|$ that is tracked by some element.

Definition Track [math-GM4F]

2024-04-20

For assemblies $X$ and $Y$ , we say that an element $t \in \mathcal{A}$ tracks a function $f : |X| \to |Y|$ if for all $x \in |X|$ and $a \in \mathcal{A}$ , if $a \Vdash_X x$ , then $t\ a$ is defined and $t\ a \Vdash_Y f(x)$ .

Then, we check assemblies and assembly maps form a category.

Proposition assemblies and assembly maps form a category [local-2]

Proof [local-1]

If $f : X \to Y$ and $g : Y \to Z$ are assembly maps, then $g \circ f : |X| \to |Z|$ is tracked. Let $t_f$ and $t_g$ track $f$ and $g$ respectively. We claim that $\langle x \rangle.\ t_g(t_f(x))$ tracks $g \circ f$ , the closed term $\langle x \rangle.\ t_g(t_f(x))$ is defined by construction, and if $a \Vdash_X x$ then

(\langle x \rangle.\ t_g(t_f(x)))\ a = t_g(t_f(a)) \Vdash_Z g(f(x))

by choice of $t_f$ and $t_g$ . Then we need identity, for each assembly $X$ , $I$ tracks any identity on $|X|$ , so assemblies and assembly maps form a category.

Notation $\text{Asm}_{\mathcal{A}}$ [local-3]

We denote $\text{Asm}_{\mathcal{A}}$ for the category of assemblies over a pca $\mathcal{A}$ .

Example [local-4]

The trivial pca has $\text{Asm}_{\{ \star \}} = \text{Set}$ .

Proposition terminal object [local-5]

The terminal object $1$ in $\text{Asm}_{\mathcal{A}}$ is given by

|1| \doteq \{ \star \} \quad\text{and}\quad a\Vdash_1 \star\ \text{for all}\ a \in \mathcal{A}

Proposition products [local-6]

The product $X \times Y$ of two assemblies is given by

|X \times Y| \doteq |X| \times |Y| \quad\text{and}\quad \bold{pair}\ a\ b \Vdash_{X \times Y} (x, y) \ \text{for all}\ a \Vdash_X x \ \text{and}\ b \Vdash_Y y

Proposition exponentials [local-8]

The exponential $Y^X$ of two assemblies is given by

|Y^X| \doteq \text{the set of assembly maps from}\ X\ \text{to}\ Y \quad\text{and}\quad t \Vdash_{Y^X} f\ \text{if}\ t\ \text{tracks}\ f

Proof [local-7]

The evaluation morphism $ev : Y^X \times X \to Y$ is given by $(f,x) \mapsto f(x)$ is tracked by $\langle x \rangle.\ \bold{fst}\ u(\bold{snd}\ u)$ . Every $g : Z \times X \to Y$ induces a unique assembly map $\bar{g} : Z \to Y^X$ making the commute diagram:

Since there is a unique assignment $\bar{g}(z) \doteq (x \mapsto g(z, x))$ and the assignment is tracked by $\langle u \rangle.\ (\langle v \rangle.\ t_g(\bold{pair}\ u\ v))$ when $t_g$ tracks $g$ .

Proposition equalizers [local-9]

The equalizer $E$ of two assembly maps $f,g : X \to Y$ is given by

|E| \doteq \{ x \in |X| \mid f(x) = g(x) \} \quad\text{and}\quad a \Vdash_E x\ \text{if}\ a \Vdash_X x

Proposition initial object [local-10]

The initial object $0$ is given by $|0| \doteq \varnothing$ with empty realizability relation (no element so empty realizability is fine).

Proposition coproducts [local-11]

The coproduct $X + Y$ is defined by

\begin{aligned} |X + Y| \doteq |X| + |Y| \quad\text{and}\quad \bold{left}\ &a \Vdash_{X+Y} \text{inl}(x)\ \text{for}\ a \Vdash_X x \\ \bold{right}\ &b \Vdash_{X+Y} \text{inr}(y)\ \text{for}\ b \Vdash_Y y \end{aligned}

where

\bold{left} \doteq \bold{pair}\ \bold{false} \ \text{and}\ \bold{right} \doteq \bold{pair}\ \bold{true}

Proposition coequalizers [local-12]

The coequalizer $C$ of assembly maps $f,g : X \to Y$ is given by

|C| \doteq |Y|/\sim \quad\text{and}\quad a \Vdash_C [y] \ \text{if}\ a \Vdash_Y y' \ \text{for some}\ y' \sim y

where $\sim$ is the least equivalence relation on $|Y|$ generated by $f(x) \sim g(x)$ for all $x \in |X|$ .

Definition. The category of assemblies over a pca [math-I7R9]