2 Our predicative foundational theory

3 The starting structure of realized collections, sets, and propositions

From [Reference Maietti and Maschio27], we recall here the definition of the category of realized collections called $\boldsymbol {\mathcal {C}}_r$ together with four indexed categories defined over it: that of realized collections and its sub-indexed category of realized sets

and the doctrine of realized proposition and its sub-doctrine of small propositions

Then, we consider the predicative effective topos $\textbf {pEff}$ in [Reference Maietti and Maschio27] defined as the base $\mathcal {Q}_{\overline {\mathbf {Prop}^r}}$ of the elementary quotient completion of $\overline {{\mathbf {Prop}^r}} $ :

$$ \begin{align*}\textbf{pEff} :\equiv \mathcal{Q}_{\overline{\mathbf{Prop}^r}}.\end{align*} $$

The key point of this article is to show how to lift the indexed category $ \mathbf {Set}^r $ , and consequently also $\overline {{\mathbf {Prop}^r_{\mathbf {s}}}}$ , on the predicative effective topos $\textbf {pEff}$ to the aim of investigating their categorical properties. We will do this by switching from indexed categories to fibrations.

3.2 Families of realized collections of $\mathcal {T}$

Here, we provide a functorial account of the slice pseudofunctor over the category of collections $\boldsymbol {\mathcal {C}}_{r}$ by defining an indexed category

(1) $$ \begin{align} \mathbf{Col}^{r}:\boldsymbol{\mathcal{C}}_{r}^{\mathrm{op}}\rightarrow \mathbf{Cat} \end{align} $$

as follows.

Suppose $\textsf {A}$ is an object of $\boldsymbol {\mathcal {C}}_{r}$ . A family of realized collections $\textsf {C}$ on $\textsf {A}$ is a formal expression $\{x'|\,\varphi _{\textsf {C}}\}$ representing a subclass of natural numbers depending on natural numbers in $\mathcal {T}$ where $\varphi _{\textsf {C}}$ is a formula of $\mathcal {T}$ with at most x and $x'$ as free variablesFootnote ² (we write $x'\,\varepsilon \, \textsf {C}$ as an abbreviation for $\varphi _{\textsf {C}}$ ) for which $x'\,\varepsilon \,\textsf {C}\,\vdash \,x\,\varepsilon \, \textsf {A}$ in $\mathcal {T}$ . Families of realized collections on $\textsf {A}$ with provably (in $\mathcal {T}$ ) equivalent membership relations are identified.

An operation from a family of realized collections $\textsf {C}$ on $\textsf {A}$ to another $\textsf {D}$ is given by an equivalence class $[\mathbf {n}]_{\approx _{\textsf {C},\textsf {D}}}$ of numerals such that in $\mathcal {T}$ we have $x'\,\varepsilon \,\textsf {C}\,\vdash \,\{\mathbf {n}\}(x,x')\,\varepsilon \,\textsf {D}$ with respect to the equivalence relation defined as follows: $\mathbf {n}\approx _{\textsf {C},\textsf {D}} \mathbf {m}$ if and only if $x'\,\varepsilon \, \textsf {C}\,\vdash _{\mathcal {T}}\,\{\mathbf {n}\}(x,x')=\{\mathbf {m}\}(x,x')$ .

If $\textsf {f}=[\mathbf {n}]_{\approx _{\textsf {C},\textsf {D}}}:\textsf {C}\rightarrow \textsf {D}$ and $\textsf {g}=[\mathbf {m}]_{\approx _{\textsf {D},\textsf {E}}}:\textsf {D}\rightarrow \textsf {E}$ are operations between families of realized collection on $\textsf {A}$ , then their composition is defined as

$$ \begin{align*}\textsf{g}\circ \textsf{f}:=[\Lambda x.\Lambda x'.\{\mathbf{m}\}(x,\{\mathbf{n}\}(x,x'))]_{\approx_{\textsf{C},\textsf{E}}}:\textsf{C}\rightarrow\textsf{E}.\end{align*} $$

IfFootnote ³ $\textsf {C}$ is a family of realized collections on $\textsf {A}$ , then its identity operation is defined by $\textsf {id}_{\textsf {C}}:=[\Lambda x.\Lambda x'.x']_{\approx _{\textsf {C},\textsf {C}}}: \textsf {C}\rightarrow \textsf {C}$ .

As discussed in [Reference Maietti and Maschio27, Theorem 4.6], for every object $\textsf {A}$ of $\boldsymbol {\mathcal {C}}_{r}$ , families of realized collections on $\textsf {A}$ and operations between them together with their composition and identity operations define a category denoted with $\mathbf {Col}^{r}(\textsf {A})$ .

If $\textsf {f}:=[\mathbf {n}]_{\approx }:\textsf {A}\rightarrow \textsf {B}$ , then the following assignments give rise to a functor $\mathbf {Col}^{r}_{\textsf {f}}$ from $\mathbf {Col}^{r}(\textsf {B})$ to $\mathbf {Col}^{r}(\textsf {A})$ :

1. 1. for every object $\textsf {C}$ of $\mathbf {Col}^{r}(\textsf {B})$ , $\mathbf {Col}^{r}_{\textsf {f}}(\textsf {C}):=\{x'|\,x\,\varepsilon \, \textsf {A}\ \wedge \ x'\,\varepsilon \, \textsf {C}[\{\mathbf {n}\}(x)/x] \}$ ;

2. 2. for every arrow $\textsf {g}:=[\mathbf {k}]_{\approx }:\textsf {C}\rightarrow \textsf {D}$ of $\mathbf {Col}^{r}(\textsf {B})$ ,

   $$ \begin{align*}\mathbf{Col}^{r}_{\textsf{f}}(\textsf{g}):=[\Lambda x.\Lambda x'. \{\mathbf{k}\}(\{\mathbf{n}\}(x),x')]_{\approx}:{\mathbf{Col}^{r}_{\textsf{f}}(\textsf{C})\rightarrow \mathbf{Col}^{r}_{\textsf{f}}(\textsf{D})}.\end{align*} $$

Moreover, the assignments $\textsf {A}\mapsto \mathbf {Col}^{r}(\textsf {A})$ and $\textsf {f}\mapsto \mathbf {Col}^{r}_{\textsf {f}}$ define an indexed category

(2) $$ \begin{align} \mathbf{Col}^{r}:\boldsymbol{\mathcal{C}}_{r}^{\mathrm{op}}\rightarrow \mathbf{Cat}. \end{align} $$

The functors $\mathbf {Col}^{r}_{\textsf {f}}$ are also called substitution functors and, as proven in [Reference Maietti and Maschio27, Theorem 4.8], these functors have left adjoints

(3) $$ \begin{align} \Sigma_{\textsf{f}}:\mathbf{Col}^{r}(\textsf{A})\rightarrow \mathbf{Col}^{r}(\textsf{B}) \end{align} $$

which sends an object $\textsf {C}\in \mathbf {Col}^r(\textsf {A})$ to

$$ \begin{align*}\Sigma_{\textsf{f}}(\textsf{C}):=\{x'|x=\{\mathbf{n}\}(p_1(x')) \wedge \ p_2(x')\ \varepsilon\ \textsf{C}[p_1(x')/x]\}\end{align*} $$

and an arrow $\textsf {g}:=[\mathbf {m}]_{\approx }:\textsf {C}\to \textsf {D}$ to

$$ \begin{align*}\Sigma_{\textsf{f}}(\textsf{g}):=[\Lambda x.\Lambda x'. \{\mathbf{pair}\}(\{\mathbf{p}_1\}(x'),\{\mathbf{m}\}(\{\mathbf{p}_1\}(x'),\{\mathbf{p}_2\}(x')))]_{\approx}.\end{align*} $$

Furthermore, in [Reference Maietti and Maschio27, Theorem 4.9] the authors provide also a weak versions of right adjoints

(4) $$ \begin{align} \Pi_{\textsf{f}}:\mathbf{Col}^{r}(\textsf{A})\rightarrow \mathbf{Col}^{r}(\textsf{B}). \end{align} $$

Now we recall an equivalent presentation of families of realized collections. We start by reminding the following result which appears as [Reference Maietti and Maschio27, Theorem 4.12].

Theorem 3.3. For every $\textsf {A}$ in $\boldsymbol {\mathcal {C}}_{r}$ , $\boldsymbol {\mathcal {C}}_{r}/\textsf {A}$ and $\mathbf {Col}^{r}(\textsf {A})$ are equivalent.

Therefore $\mathbf {Col}^{r}$ is a functorial account of the slice pseudofunctor on $\boldsymbol {\mathcal {C}}_{r}$ and hence it provides a split fibration

$$\begin{align*}\pi:\textsf{Gr}(\mathbf{Col}^r)\to \boldsymbol{\mathcal{C}}_{r}.\end{align*}$$

3.3 Families of realized sets

We recall from [Reference Maietti and Maschio27, Section 4.3] that internally in $\boldsymbol {\mathcal {C}}_{r}$ it is possible to define a universe of sets as a fixpoint of a suitable admissible formula of $\mathcal {T}$ . The universe of sets in $\boldsymbol {\mathcal {C}}_{r}$ is defined as $\textsf {U}_{\textsf {S}}:=\{x|\;\textsf {Set}(x) \}$ following [Reference Maietti, Maschio and Rathjen28, Reference Maietti, Maschio and Rathjen29] when the foundational theory $\mathcal {T}$ is an extension of $\mathbf {CZF}$ . Instead, when $\mathcal {T}$ is ${\widehat {ID_1}}$ , following [Reference Ishihara, Maietti, Maschio and Streicher20], the universe of sets is defined in a more complex way as $\textsf {U}_{\textsf {S}}:=\{x|\;\textsf {Set}(x)\,\wedge \,\forall t\,(t\,\overline {\varepsilon }\,x\leftrightarrow \neg \, t {\not {\overline {\varepsilon }}} x)\}$ with the help of a membership relation $t \,\overline {\varepsilon }\,x$ (which is defined also in the extensions of $\mathbf {CZF}$ ) and its negation $ t {\not {\overline {\varepsilon }}} \ x$ defined simultaneously all together (recall that ${\widehat {ID_1}} $ is an arithmetical theory).

Definition 3.4. Let $\textsf {A}$ be an object of $\boldsymbol {\mathcal {C}}_{r}$ . The category $\mathbf {Set}^{r}(\textsf {A})$ is the full subcategory of $\mathbf {Col}^{r}(\textsf {A})$

whose objects, called families of realized sets on $\textsf {A}$ , are families of realized collections on $\textsf {A}$ of the form

$$ \begin{align*}\tau_{\textsf{A}}(\mathbf{n}):=\{x'|\,x'\,\overline{\varepsilon}\, \{\mathbf{n}\}(x)\,\wedge\, x\,\varepsilon \,\textsf{A}\}\end{align*} $$

for a numeral $\mathbf {n}$ defining an operation $[\mathbf {n}]_{\approx }:\textsf {A}\rightarrow \textsf {U}_{\textsf {S}}$ in $\boldsymbol {\mathcal {C}}_{r}$ .

Applying the Grothendieck construction, we obtain the diagram

3.4 Categorical properties of realized collections and sets

We recall the properties of the categories of families of realized collections $\mathbf {Col}^r(\textsf {A})$ . The following result appears as [Reference Maietti and Maschio27, Theorem 4.7].

Theorem 3.5. For every object $\textsf {A}$ of $\boldsymbol {\mathcal {C}}_{r}$ , the fibre $\mathbf {Col}^{r}(\textsf {A})$ is a finitely complete category with parameterized list objects, finite coproducts, and weak exponentials. Moreover for every arrow $\textsf {f}:\textsf {A}\rightarrow \textsf {B}$ in $\boldsymbol {\mathcal {C}}_{r}$ , the functor $\mathbf {Col}^{r}_{\textsf {f}}$ preserves this structure.

We recall the main ingredients of the proof of Theorem 3.3 which will be used in the rest of the article. The proof of the above result relies on the definition of the following functors. The first one is

(5) $$ \begin{align} \mathbf{J}_{\textsf{A}}:\boldsymbol{\mathcal{C}}_{r}/\textsf{A}\rightarrow \mathbf{Col}^{r}(\textsf{A}) \end{align} $$

defined by the assignments

$$ \begin{align*}\begin{array}{rcl} [\mathbf{b}]_{\approx}:\textsf{B}\rightarrow \textsf{A} & \mapsto\ & \{x'|\,x'\,\varepsilon\, \textsf{B}\wedge x=\{\mathbf{b}\}(x')\}\\[3pt] [\mathbf{n}]_{\approx}\ \ &\ \mapsto\ &\ [\Lambda x.\Lambda x'.\{\mathbf{n}\}(x')]_{\approx}. \end{array}\end{align*} $$

The second is the functor

(6) $$ \begin{align} \mathbf{I}_{\textsf{A}}:\mathbf{Col}^{r}(\textsf{A})\rightarrow\boldsymbol{\mathcal{C}}_{r}/\textsf{A} \end{align} $$

defined by the assignments

$$ \begin{align*}\begin{array}{rcl}\textsf{B}\ \ & \mapsto\ & \ \textsf{p}_{1}^{\Sigma}:=[\mathbf{p}_{1}]_{\approx}:\Sigma(\textsf{A},\textsf{B})\rightarrow \textsf{A}\\[3pt] [\mathbf{n}]_{\approx}\ \ & \mapsto\ & \ [\Lambda x.\{\mathbf{pair}\}(\{\mathbf{p}_{1}\}(x),\{\mathbf{n}\}(\{\mathbf{p}_{1}\}(x),\{\mathbf{p}_{2}\}(x)))]_{\approx}, \end{array}\end{align*} $$

where $\Sigma (\textsf {A},\textsf {B})$ is the object defined as

(7) $$ \begin{align} \Sigma(\textsf{A},\textsf{B}):= \{x|\,p_{1}(x)\,\varepsilon\, \textsf{A}\wedge p_{2}(x)\,\varepsilon\, \textsf{B}[p_{1}(x)/x])\}. \end{align} $$

The above theorem implies the following result which appears as [Reference Maietti and Maschio27, Corollary 4.13].

Corollary 3.6. $\boldsymbol {\mathcal {C}}_r$ is weakly locally cartesian closed.

Observe that, since every arrow in $\boldsymbol {\mathcal {C}}_r$ can be represented by many different numerals, the category $\boldsymbol {\mathcal {C}}_r$ is weakly locally cartesian closed but not cartesian closed.

Now we recall the properties of the category of families of realized sets.

Definition 3.7. An arrow $\textsf {f}:\textsf {A}\rightarrow \textsf {B}$ in $\boldsymbol {\mathcal {C}}_{r}$ is set-fibred if there exists an object $\textsf {C}$ in $\mathbf {Set}^{r}(\textsf {B})$ for which $\textsf {f}$ is isomorphic in $\boldsymbol {\mathcal {C}}_{r}/\textsf {B}$ to $\mathbf {I}_{\textsf {B}}(\textsf {C})$ .

Lemma 3.8. If $\textsf {f}:\textsf {B}\rightarrow \textsf {C}$ is an arrow in $ \mathbf {Set}^r(\textsf {A})$ , then $\mathbf {I}_{\textsf {A}}(\textsf {f})$ is a set-fibred arrow.

Proof. Let $\mathbf {n}_{\textsf {f}}$ a numeral associated with $\textsf {f}$ and take the object $\textsf {D}$ in $\mathbf {Col}^r( \Sigma (\textsf {A},\textsf {C}))$ defined as

$$\begin{align*}\textsf{D}:=\{ y\ |\ p_1(y)\ \varepsilon\ \textsf{B}[p_1(x)/x]\ \wedge \ ( p_2(y)=p_2(x) \ \wedge \ p_2(y)=\{\mathbf{n}_{\textsf{f}}\}(p_1(x),p_1(y)))\}, \end{align*}$$

which is in fact in $\mathbf {Set}^r(\Sigma (\textsf {A},\textsf {C}))$ since it is defined by means of operations on which the universe $\textsf {U}_{\textsf {S}}$ of sets is closed. Then $\mathbf {I}_{\textsf {A}}(\textsf {f})$ , seen as an object in $\boldsymbol {\mathcal {C}}_r/(\Sigma (\textsf {A},\textsf {C})$ , is isomorphic to $\mathbf {I}_{\Sigma (\textsf {A},\textsf {C})}(\textsf {D})$ .

Using the encodings of $\Sigma $ and $\Pi $ , we obtain the following properties for substitution along set-fibred maps.

Lemma 3.9. If $\textsf {f}:\textsf {A}\to \textsf {B}$ is set-fibred then $\mathbf {Set}^r_{\textsf {f}}$ has a left adjoint.

Proof. Since ${\textsf {f}}$ is set-fibred, we can assume

$$ \begin{align*}\textsf {f}=\textsf{p}_{1}^{\Sigma}=[\mathbf{p}_{1}]_{\approx}:\Sigma(\textsf{B},\tau_{\textsf{B}}(\mathbf{n}))\rightarrow \textsf{B}\end{align*} $$

for some numeral $\mathbf {n}$ defining an operation $[\mathbf {n}]_{\approx }:\textsf {A}\rightarrow \textsf {U}_{\textsf {S}}$ in $\boldsymbol {\mathcal {C}}_{r}$ .

If $[\mathbf {m}]_{\approx }:\Sigma (\textsf {B},\tau _{\textsf {B}}(\mathbf {n}))\rightarrow \textsf {U}_{\textsf {S}}$ in $\boldsymbol {\mathcal {C}}_{r}$ , then

$$ \begin{align*}\Sigma_{\textsf{p}_{1}^{\Sigma}}(\tau_{\Sigma(\textsf{B},\tau_{\textsf{B}}(\mathbf{n}))}(\mathbf{m}))\simeq \tau_{\textsf{B}}(\Lambda x. \{\boldsymbol{\sigma}\}( \{\mathbf{n}\}(x),\Lambda y. \{\mathbf{m}\}(\{\mathbf{pair}\}(x,y)))),\end{align*} $$

where $\boldsymbol {\sigma }$ is a numeral representing the construction of codes of $\Sigma $ -types in the universe of realized sets [Reference Ishihara, Maietti, Maschio and Streicher20].

Lemma 3.10. If $\textsf {f}:\textsf {A}\rightarrow \textsf {B}$ in $\boldsymbol {\mathcal {C}}_{r}$ is set-fibred, for every object $\textsf {C}$ in $\mathbf {Set}^{r}(\textsf {A})$ the object $\Pi ^{r}_{\textsf {f}}(\textsf {C})$ is isomorphic in $\mathbf {Col}^{r}(\textsf {B})$ to an object of $\mathbf {Set}^{r}(\textsf {B})$ .

Proof. Since $\textsf {f}$ is set-fibred, we can assume

$$ \begin{align*}\textsf {f}=\textsf{p}_{1}^{\Sigma}=[\mathbf{p}_{1}]_{\approx}:\Sigma(\textsf{B},\tau_{\textsf{B}}(\mathbf{n}))\rightarrow \textsf{B}\end{align*} $$

for some numeral $\mathbf {n}$ defining an operation $[\mathbf {n}]_{\approx }:\textsf {A}\rightarrow \textsf {U}_{\textsf {S}}$ in $\boldsymbol {\mathcal {C}}_{r}$ .

If $[\mathbf {m}]_{\approx }:\Sigma (\textsf {B},\tau _{\textsf {B}}(\mathbf {n}))\rightarrow \textsf {U}_{\textsf {S}}$ in $\boldsymbol {\mathcal {C}}_{r}$ , then, considering the definition of $\Pi ^r_{\textsf {f}}$ in [Reference Maietti and Maschio27, Theorem 4.9], we get that

$$ \begin{align*}\Pi_{\textsf{p}_{1}^{\Sigma}}(\tau_{\Sigma(\textsf{B},\tau_{\textsf{B}}(\mathbf{n}))}(\mathbf{m}))\simeq \tau_{\textsf{B}}(\Lambda x. \{\boldsymbol{\pi}\}( \{\mathbf{n}\}(x),\Lambda y. \{\mathbf{m}\}(\{\mathbf{pair}\}(x,y)))),\end{align*} $$

where $\boldsymbol {\pi }$ is a numeral representing the construction of codes of $\Pi $ -types in the universe of realized sets [Reference Ishihara, Maietti, Maschio and Streicher20].

Using set-fibred arrows, we obtain the following extension of [Reference Maietti and Maschio27, Theorem 4.24].

Theorem 3.11. For every $\textsf {A}$ in $\boldsymbol {\mathcal {C}}_{r}$ , $\mathbf {Set}^{r}(\textsf {A})$ is a finitely complete category with disjoint stable finite coproducts, parameterized list objects, and weak exponentials. Moreover, if $\textsf {f}:\textsf {A}\rightarrow \textsf {B}$ is set-fibred, then $\mathbf {Set}^{r}_{\textsf {f}}$ has a left adjoint and for every object $\textsf {C}$ in $\mathbf {Set}^{r}(\textsf {A})$ the object $\Pi ^{r}_{\textsf {f}}(\textsf {C})$ is isomorphic in $\mathbf {Col}^{r}(\textsf {B})$ to an object of $\mathbf {Set}^{r}(\textsf {B})$ .

The embedding of $\mathbf {Set}^{r}$ in $\mathbf {Col}^{r}$ preserves finite limits, finite coproducts, parameterized list objects, and weak exponentials.

3.7 Further notation

For every $\textsf {f}:=[\mathbf {n}]_{\approx }:\textsf {A}\rightarrow \textsf {B}$ in $\boldsymbol {\mathcal {C}}_{r}$ and every $\textsf {C}$ in $\mathbf {Col}^{r}(\textsf {B})$ , we denote with $\Sigma (\textsf {f},\textsf {C})$ the arrow $[\Lambda x. \{\mathbf {pair}\}(\{\mathbf {n}\}(\{\mathbf {p}_{1}\}(x)),\{\mathbf {p}_{2}\}(x))\, ]_{\approx }$ from $\Sigma (\textsf {A},\mathbf {Col}_{\textsf {f}}^r(\textsf {C}))$ to $\Sigma (\textsf {B},\textsf {C})$ . This arrow makes the following diagram a pullback in  $\boldsymbol {\mathcal {C}}_{r}$ :

(for details see [Reference Maietti and Maschio27, Lemma 4.11].

Now let $\textsf {A}$ be an object in $\boldsymbol {\mathcal {C}}_r$ and let $\textsf {B}$ be an object of $\mathbf {Col}^r(\textsf {A})$ . If $\textsf {C}$ is an object in $\mathbf {Col}^r(\Sigma (\textsf {A}, \textsf {B}))$ , then we define $\Sigma ^{\textsf {A}}(\textsf {B},\textsf {C})$ as the object in $\mathbf {Col}^r(\textsf {A})$ given by $\Sigma _{\textsf {p}^\Sigma _1}(\textsf {C})$ .

Moreover, for every arrow $\textsf {f}: \textsf {B}'\to \textsf {B}$ in $\textbf {Col}^r(\textsf {A})$ , we define $\Sigma ^{\textsf {A}}(\textsf {f}, \textsf {C})$ as the arrow

$$ \begin{align*}\Lambda x. \Lambda x'. \{\mathbf{pair}\} (\{\mathbf{pair}\}(x,\{\mathbf{n}_{\textsf{f}}\}(x,\{\mathbf{p_2}\}(\{\mathbf{p}_1\}(x'))),\{\mathbf{p_2}\}(x') )\end{align*} $$

which makes the following diagram a pullback in $\mathbf {Col}^r(\textsf {A})$ :

where $\textsf {p}_1^{\textsf {A},\Sigma }:=[\Lambda x.\Lambda x'. \{\mathbf {p_2}\}(\{\mathbf {p_1}\}(x'))]_\approx $ .

We now define a currying isomorphism in $\boldsymbol {\mathcal {C}}_r$ for every object $\textsf {A}\in \boldsymbol {\mathcal {C}}_r$ , $\textsf {B}\in \mathbf {Col}^r(\textsf {A})$ and $\textsf {C}\in \mathbf {Col}^r(\Sigma (\textsf {A}, \textsf {B}))$ :

$$\begin{align*}\textsf{cur}: \Sigma(\Sigma (\textsf{A}, \textsf{B}), \textsf{C})\to \Sigma(\textsf{A},\Sigma^{\textsf{A}}(\textsf{B},\textsf{C}))\end{align*}$$

given by

(8) $$ \begin{align} \Lambda x. \{\mathbf{pair}\}(\{\mathbf{p}_1\}(\{\mathbf{p}_1\}(x)),x). \end{align} $$

4 An internal language for ${\mathbf {Prop}^r}$ and $\mathbf {Col}^r$

As done in [Reference van Oosten42], we consider the internal language of the functors ${\mathbf {Prop}^r}$ and $\mathbf {Col}^r$ . The former is in the form of a first-order typed language with equality, and the latter is in the form of one with dependent types.

A context $\Gamma $ stands for an expression of the form $[x_0:\textsf {A}_0, \dots , x_n:\textsf {A}_n(x_1,\dots , x_{n-1})]$ . A context substitution $\bar {t}:\Gamma \to \Delta $ , where $\Delta :=[y_0:\textsf {B}_0, \dots , y_m:\textsf {B}_m(y_0,\dots ,y_{m-1})]$ is a list of terms $\bar {t}:=[t_0, \dots , t_m]$ such that $t_i:\textsf {B}_i(t_0,\dots ,t_{i-1})$ is in context $[\Gamma ]$ for $0\le i\le m$ .

We will adopt the notation $\textsf {C}_x(y)$ for a type in context $x:\textsf {A}, y:\textsf {B}(x)$ and $\textsf {f}_x:\textsf {B}(x)\to \textsf {B}'(x)$ for a term of type $\textsf {B}'(x)$ in context $x:\textsf {A}, y:\textsf {B}(x)$ .

Recall from [Reference Maietti and Maschio27], that contexts $\Gamma $ are interpreted as objects $\|\Gamma \|$ of the category $\boldsymbol {\mathcal {C}}_r$ and substitutions of contexts as arrows of $\boldsymbol {\mathcal {C}}_r$ . A formula $\psi [\Gamma ]$ in context $\Gamma $ is interpreted as an element of ${\mathbf {Prop}^r}(\|\Gamma \|)$ , while a dependent type $\textsf {A}[\Gamma ]$ in context $\Gamma $ is interpreted as an object of $\mathbf {Col}^r(\|\Gamma \|)$ . Given the interpretations $\|\bar {t}\|:\|\Gamma \|\to \|\Delta \|$ and $\|\psi [\Delta ]\|\in {\mathbf {Prop}^r}(\|\Delta \|)$ , or $\|\textsf {A}[\Delta ]\|\in \mathbf {Col}^r(\|\Delta \|)$ , then the interpretation of $\psi (\bar {t})[\Gamma ]$ , or $\textsf {A}(\bar {t})[\Gamma ]$ , is, respectively, given by ${\mathbf {Prop}^r}_{\|t\|}(\|\psi \|)$ , or $\mathbf {Col}^r_{\|t\|}(\|\textsf {A}\|)$ .

Furthermore, we assume that given an interpretation of $\textsf {A}[\Gamma ]$ as an object $\|\textsf {A}\|\in \mathbf {Col}^r(\|\Gamma \|)$ , then the interpretation of the context $[\Gamma , x:\textsf {A}]$ is given by the object $\Sigma (\|\Gamma \|,\|\textsf {A}\|)$ of $\boldsymbol {\mathcal {C}}_r$ . In particular, given a substitution $\bar {t}:\Gamma \to \Delta $ and a type in context $\textsf {A}[\Delta ]$ , then the substitution $[\bar {t},y]:[\Gamma ,y:\textsf {A}(\bar {t})]\to [\Delta , z:\textsf {A}]$ is interpreted as the arrow

$$\begin{align*}\Sigma(\|\bar{t}\|, \|\textsf{A}\|):\Sigma(\|\Gamma\|, \mathbf{Col}^r_{\|\bar{t}\|}(\|\textsf{A}\|))\to \Sigma(\|\Delta\|,\|\textsf{A}\|).\end{align*}$$

If $\textsf {A}[\Gamma ]$ and $\textsf {B}[\Gamma ]$ are types in the same context and $f: \textsf {B}$ is a term in context $[\Gamma , x:\textsf {A}]$ , then f is interpreted as an arrow $\|f\|:\|\textsf {A}\|\to \|\textsf {B}\|$ in $\mathbf {Col}^r(\|\Gamma \|)$ and the substitution $[id_\Gamma ,f]:[\Gamma ,x:\textsf {A}]\to [\Gamma ,y:\textsf {B}]$ is interpreted as the arrow

$$\begin{align*}\mathbf{I}_{\|\Gamma\|}(\|f\|):\Sigma(\|\Gamma\|,\|\textsf{A}\|)\to \Sigma(\|\Gamma\|,\|\textsf{B}\|).\end{align*}$$

If $\psi [\Gamma ]$ is a formula in context, we define its validity ${\mathbf {Prop}^r}\vdash \psi [\Gamma ]$ if and only if $\top _{\|\Gamma \|}\le _{\|\Gamma \|}\|\psi [\Gamma ]\|$ . Similarly, for a type $\textsf {A}[\Gamma ]$ in context, we define $\mathbf {Col}^r\vdash \textsf {A}[\Gamma ] $ if and only if there exists an arrow $1_{\|\Gamma \|}\to \|\textsf {A}[\Gamma ]\|$ .

Since, the interpretation of the internal language of ${\mathbf {Prop}^r}$ extends Kleene realizability interpretation $\Vdash $ of $\textsf {HA}$ (see [Reference Maietti and Maschio27, Lemma 4.32]), and the elements of ${\mathbf {Prop}^r}(\|\Gamma \|)$ are equivalence classes of those in $\mathbf {Col}^r(\|\Gamma \|)$ , we shall adopt the notation $t\Vdash \textsf {A}$ for a term $t:\textsf {A}$ in context $\Gamma $ of a representative $\textsf {A}$ of some proposition in ${\mathbf {Prop}^r}(\|\Gamma \|)$ , while we shall adopt the notation $t\varepsilon \textsf {A}$ for a term $t:\textsf {A}$ in context $\Gamma $ when we see $\textsf {A}$ as a collection.

5 The predicative effective topos $\textbf {pEff}$

In [Reference Maietti and Maschio27], the predicative effective topos $\textbf {pEff}$ is defined as the base category $\mathcal {Q}_{\overline {\mathbf {Prop}^r}}$ of the elementary quotient completion of the elementary doctrine $\overline {\mathbf {Prop}^r}$ . It is the category whose objects are the pairs $(\textsf {A},[\textsf {R}])$ where $\textsf {A}$ is an object of the category $\boldsymbol {\mathcal {C}}_{r}$ and $[\textsf {R}]$ is an object of $\overline {\mathbf {Prop}^{r}}(\textsf {A}\times \textsf {A})$ such that

1. 1. $\top _{\textsf {A}}\le _{\textsf {A}}\overline {\mathbf {Prop}^{r}}_{\Delta _{\textsf {A}}}([\textsf {R}])$ ;

2. 2. $[\textsf {R}]\le _{\textsf {A}\times \textsf {A}}\overline {\mathbf {Prop}^{r}}_{\langle p_2,p_1\rangle }([\textsf {R}])$ , where $p_1,p_2:\textsf {A}\times \textsf {A}\to \textsf {A}$ are the projections;

3. 3. $\overline {\mathbf {Prop}^{r}}_{\langle p_1,p_2\rangle }([\textsf {R}]) \wedge \overline {\mathbf {Prop}^{r}}_{\langle p_2,p_3\rangle }([\textsf {R}])\le _{\textsf {A}\times \textsf {A}\times \textsf {A}}\overline {\mathbf {Prop}^{r}}_{\langle p_1,p_3\rangle }([\textsf {R}])$ , where $p_1,p_2, p_3:\textsf {A}\times \textsf {A}\times \textsf {A}\to \textsf {A}$ are the corresponding projections.

Equivalently, the above conditions state that $[\textsf {R}]$ is an equivalence relation for the internal logic of the doctrine $\overline {\mathbf {Prop}^{r}}$ (see [Reference Maietti and Maschio27, Definition 5.1]).

An arrow from $(\textsf {A},[\textsf {R}])$ to $(\textsf {B},[\textsf {S}])$ is an equivalence class $[\textsf {f}]$ of arrows $\textsf {f}:\textsf {A}\rightarrow \textsf {B}$ in $\boldsymbol {\mathcal {C}}_{r}$ such that $[\textsf {R}]\le _{\textsf {A}\times \textsf {A}}\overline {\mathbf {Prop}^{r}}_{\textsf {f}\times \textsf {f}}([\textsf {S}])$ , where $\textsf {f}\sim \textsf {g}$ if and only if $\top _{\textsf {A}}\le _{\textsf {A}}\overline {\mathbf {Prop}^{r}}_{\langle \textsf {f},\textsf {g}\rangle } ([\textsf {S}])$ .

Moreover, we recall from [Reference Maietti and Maschio27, Theorem 5.2] that $\textbf {pEff}$ is equivalent to the exact completion $(\boldsymbol {\mathcal {C}}_r)_{ex/lex}$ of the left exact category $\boldsymbol {\mathcal {C}}_r$ . Indeed, this follows from Theorem 3.14 and the fact that the elementary quotient completion of a weak subobject doctrine on a lex category ${C}$ is equivalent to the exact on lex completion of ${C}$ (see [Reference Maietti and Rosolini31, Reference Maietti and Rosolini32]).

The following appears as [Reference Maietti and Maschio27, Theorem 5.5].

6 Families of collections and sets over $\textbf {pEff}$

In this section, we define suitable categories for every object $(\textsf {A},[\textsf {R}]) \in \textbf {pEff}$ that are apt to interpret the notions of families of collections and sets in $\textbf {pEff}$ . Slice categories provide a natural account of the notion of families of collections over an object $(\textsf {A},[\textsf {R}]) \in \textbf {pEff}$ ; however, families of sets require additional considerations to be defined. To do that, by analogy with [Reference Maietti25], we define for every representative of $[\textsf {R}]$ a category of extensional dependent collections $Dep_{\textbf {pEff}}(\textsf {A},{\textsf {R}})$ and show that it is equivalent to the category of suitable internal groupoid actions $\mathcal {Des}(p,{\textsf {R}})$ . Since the objects of $Dep_{\textbf {pEff}}(\textsf {A},{\textsf {R}})$ are defined through the indexed categories $\mathbf {Col}^r$ and ${\mathbf {Prop}^r}$ , we can easily define a notion of extensional dependent sets and equivalently obtain a subcategory of $\textbf {pEff}/(\textsf {A},[\textsf {R}])$ , independently of the representative ${\textsf {R}}$ .

The intuitive idea behind the definition of a family of collections over $(\textsf {A},\textsf {R})$ is the following:

• • first we take a family of realized collections $\textsf {B}(a)$ over $\textsf {A}$ in $\boldsymbol {\mathcal {C}}_{r}$ ;

• • then, we take an equivalence relation $\textsf {S}_{a}(b,b')$ on each $\textsf {B}(a)$ (depending on $\textsf {A}$ );

• • furthermore, we take a family of transport maps $b\mapsto \sigma _{a,a'}(r,b)$ for $a,a'\,\varepsilon \, \textsf {A}$ , $b\,\varepsilon \, B(a)$ , and $r\Vdash \textsf {R}(a,a')$ such that $\sigma _{a,a'}(r,b)\,\varepsilon \, \textsf {B}(a')$ ;

• • finally, we ask $\sigma $ to satisfy the following conditions, which make it a sort of action:

  1. 1. if $S_{a}(b,b')$ and $r\Vdash \textsf {R}(a,a')$ , then $\textsf {S}_{a'}(\sigma _{a,a'}(r,b),\sigma _{a,a'}(r,b'))$ , that is, $\sigma $ respects $\textsf {S}$ ;

  2. 2. if $r\Vdash \textsf {R}(a,a)$ and $b\,\varepsilon \, \textsf {B}(a)$ , then $\textsf {S}_{a}(b,\sigma _{a,a}(r,b)))$ , that is, $\sigma $ is well-behaved with respect to identities;

  3. 3. if $r\Vdash \textsf {R}(a,a")$ , $r'\Vdash \textsf {R}(a,a')$ , $r"\Vdash \textsf {R}(a',a")$ , and $b\,\varepsilon \, \textsf {B}(a)$ , then

     $$ \begin{align*}\textsf{S}_{a"}(\ \sigma_{a,a"}(r,b)\ ,\ \sigma_{a',a"}(r", \sigma_{a,a'}(r',b))\ ),\end{align*} $$

     that is, $\sigma $ is well-behaved with respect to composition.

  Observe that, taking $a'=a"$ and a witness for the reflexivity of $\textsf {R}$ , conditions 2. and 3. above imply the following condition stating that $\sigma $ , once we fix two related objects $a,a'$ , does not depend on the particular realizer of $\textsf {R}(a,a')$ :

  1. 4. ${\textsf {S}}_{a'}(\sigma _{a,a'}(r,b),\sigma _{a,a'}(r',b))$ for every $b\,\varepsilon \, \textsf {B}(a)$ , $a,a'\varepsilon \textsf {A}$ , $r,r'\Vdash \textsf {R}(a,a')$ ;

To formulate in a precise way this idea we need first to introduce the notion of fibered ${\overline {\textbf {Prop}^r}}$ -equivalence relation.

Definition 6.2. Let $(\textsf {{A},[{R}]})$ be an object of $\textbf {pEff}$ . An extensional dependent collection on $(\textsf {{A} , [ {R}]})$ , with respect to ${\textsf {R}}$ , is a triple $(\textsf {B},[\textsf {S}],\sigma )$ where $\textsf {B}\in \textbf {Col}^r(\textsf {A})$ , $[\textsf {S}]$ is a dependent ${\overline {\textbf {Prop}^r}}$ -equivalence relation on $\textsf {B}$ and

$$ \begin{align*}\sigma: \textsf{R}\times \textbf{Col}^r_{p_1}(\textsf{B}) \to \textbf{Col}^r_{p_2}(\textsf{B})\end{align*} $$

is an arrow in $\textbf {Col}^r(\textsf {A}\times \textsf {A})$ satisfying

1. 1. $\sigma $ preserves $[\textsf {S}]$ , that is, for the arrow

   

   it holds

   $$ \begin{align*}\overline{\textbf{Prop}^r}_{{\Sigma(p_1,\textsf{B}\times\textsf{B})\circ\textbf{I}(p_1)}}[\textsf{S}]\le \overline{\textbf{Prop}^r}_{\Sigma(p_2,\textsf{B}\times\textsf{B})\circ {\textbf{I}((\sigma\circ \langle p_1, p_2\rangle)\times (\sigma\circ\langle p_1,p_3\rangle))}}[\textsf{S}],\end{align*} $$

   where $\Sigma (p_i,\textsf {B}\times \textsf {B}):\Sigma (\textsf {A}\times \textsf {A},\textbf {Col}^r_{p_1}(\textsf {B}\times \textsf {B}) )\to {\Sigma (\textsf {A},\textsf {B}\times \textsf {B})}$ , for $i=1,2$ assuming that $\textbf {Col}^r_{p_1}(\textsf {B}\times \textsf {B}) $ is exactly $\textbf {Col}^r_{p_1}(\textsf {B})\times \textbf {Col}^r_{p_1}(\textsf {B})$ .

2. 2. $\sigma $ preserves the identities, that is, for the unique arrow $\rho $ making the following diagram commute:

   

   then $\top \le {\overline {\textbf {Prop}^r}}_{\rho }([\textsf {S}])$ .

3. 3. $\sigma $ preserves the composition, that is, for the unique arrow $\tau $ Footnote ⁵

   

   such that

   • • $\mathbf {I}(p_1)\circ \tau = \mathbf {I}(\mathbf {Col}^r_{\langle p_1,p_3\rangle }(\sigma )\circ \langle p_1,p_4\rangle )$ ;

   • • $\mathbf {I}(p_2)\circ \tau =\mathbf {I}(p_1)\circ \mathbf {I}( id \times ( \mathbf {Col}^r_{\langle p_2,p_3\rangle }(\sigma )\circ ( id\times \mathbf {Col}^r_{\langle p_1,p_2\rangle }(\sigma )) ))$ ;

   it holds that $\top \le {\overline {\textbf {Prop}^r}}_{\Sigma (p_3, \textsf {B}\times \textsf {B})\circ \tau }([\textsf {S}])$ .

Lemma 6.7. Let $(\textsf {A},[\textsf {R}])$ be an object in $\mathbf {pEff}$ and let $\textsf {R},\textsf {R}'$ be two representatives of $[\textsf {R}]$ . The categories $Dep_{\mathbf {pEff}}(\textsf {A},{\textsf {R}})$ and $Dep_{\mathbf {pEff}}(\textsf {A},{\textsf {R}}')$ are equivalent. The same holds for extensional dependent sets.

Proof. The fact that $\textsf {R}$ and $\textsf {R}'$ are in $[\textsf {R}]\in \overline {{\mathbf {Prop}^r}}(\textsf {A}\times \textsf {A})$ imply that there exist two arrows $h:\textsf {R}\to \textsf {R}'$ and $k:\textsf {R}'\to \textsf {R}$ in $\mathbf {Col}^r(\textsf {A}\times \textsf {A})$ . We can construct the functor

$$\begin{align*}-\circ k:Dep_{\textbf{pEff}}({\textsf{A}}, {\textsf{R}})\to Dep_{\textbf{pEff}}({\textsf{A}}, {\textsf{R}}') \end{align*}$$

that sends an extensional dependent collection $(\textsf {B},[\textsf {S}],\sigma )$ to $(\textsf {B},[\textsf {S}],\sigma \circ (id \times k))$ and every arrow into itself. It is straightforward to prove this functor is an equivalence considering the similar functor

$$\begin{align*}-\circ h:Dep_{\textbf{pEff}}({\textsf{A}}, {\textsf{R}}')\to Dep_{\textbf{pEff}}({\textsf{A}}, {\textsf{R}}).\\[-30pt] \end{align*}$$

In the following proposition, we show directly that extensional dependent collections induce objects in the slice categories of $\textbf {pEff}$ .

Proposition 6.8. Let $(\textsf {A},[\textsf {R}])$ be an object in $\mathbf {pEff}$ . There exists a full and faithful essentially surjective functor

$$ \begin{align*}\mathbf{K}:Dep_{\mathbf{pEff}}(\textsf{A}, {\textsf{R}})\to \mathbf{pEff}/(\textsf{A},{[\textsf{R}]}).\end{align*} $$

Proof. For every object $(\textsf {B},\textsf {S},\sigma )$ we define

(9) $$ \begin{align}\mathbf{K}(\textsf{B},[\textsf{S}],\sigma):= [\textsf{p}_1^\Sigma]_{\cong} : (\Sigma(\textsf{A},\textsf{B}),\exists_{d_{{\textsf{R}}}}(\overline{\mathbf{Prop}^r}_{t_\sigma}([\textsf{S}])))\to (\textsf{A},[\textsf{R}]) \end{align} $$

for the commutative diagram

Where k is the isomorphism given by $\langle \Sigma (p_1, \textsf {B})\circ \mathbf {I}(p_1),\Sigma (p_2, \textsf {B})\circ \mathbf {I}(p_2)\rangle $ .

Informally, the domain of the arrow above has pairs $(a,b)$ with $a\in \textsf {A}$ and $b\in \textsf {B}(a)$ as elements. A realizer for an equivalence of two such pairs $(a,b)$ and $(a',b')$ is a pair $(r,s)$ such that $r\Vdash \textsf {R}(a,a')$ and $s\Vdash \textsf {S}_{a'}(\sigma _{a,a'}(r,b),b')$ .

For $[\textsf {f}]:(\textsf {B},[\textsf {S}],\sigma )\rightarrow (\textsf {C},[\textsf {H}],\eta )$ we define $\mathbf {K}([\textsf {f}])$ as $[\mathbf {I}(\textsf {f})]$ . Such arrow preserves the equalities of the domains of $\mathbf {K}((\textsf {B},[\textsf {S}],\sigma ) )$ and $ \mathbf {K} ( (\textsf {C},[\textsf {H}],\eta ) )$ . Indeed, if there exists $r \Vdash \textsf {R}(a,a')$ such that $\textsf {S}_{a'}(\sigma _{a,a'}(r,b), b')$ , then one obtains that $\textsf {H}_{a'}(\textsf {f}(\sigma _{a,a'}(r,b)),\textsf {f}(b'))$ because $\textsf {f}$ preserves $\textsf {S}$ and $\textsf {H}$ . Now, since $\textsf {f}$ commutes with transport maps, then $\textsf {H}_{a'}(\textsf {f}(\sigma _{a,a'}(r,b)),\eta _{a,a'}(r,\textsf {f}(b)))$ . Hence, transitivity of $\textsf {H}$ implies $\textsf {H}_{a'}( \textsf {f}(b')\, ,\, \eta _{a,a'}(r,\textsf {f}(b)) )$ . Thus, $[\mathbf {I}(\textsf {f})]$ is well defined and the assignments define a functor.

To prove fullness we need to show that every arrow h in $\textbf {pEff}/(\textsf {A},[\textsf {R}])$ between objects in the image of $\mathbf {K}$ has the form $[\mathbf {I}(\widetilde {h})]$ . Assume now two objects $(\textsf {B},[\textsf {S}],\sigma )$ and $(\textsf {C},[\textsf {H}],\eta )$ in $Dep_{\textbf {pEff}}(\textsf {A}, {\textsf {R}})$ . Any arrow from $\mathbf {K}((\textsf {B},[\textsf {S}],\sigma ) )$ to $ \mathbf {K} ( (\textsf {C},[\textsf {H}],\eta ) )$ is given by an arrow h in $\boldsymbol {\mathcal {C}}_r$ from $\Sigma (\textsf {A},\textsf {B})$ to $\Sigma (\textsf {A},\textsf {C})$ such that $\textsf {p}_1^{\Sigma }\circ h=\textsf {p}_1^{\Sigma }$ in $\textbf {pEff}/(\textsf {A},[\textsf {R}])$ . To see how this h induces an arrow $\widetilde {h}: \textsf {B}\rightarrow \textsf {C}$ in $\mathbf {Col}^r(\textsf {A})$ for which $\mathbf {I}(\widetilde {h})=h$ in $\textbf {pEff}/(\textsf {A},[\textsf {R}])$ , assume that $r\Vdash \textsf {R}((p_1\circ h)(a,b), a)$ for $a\in A$ and $b\in \textsf {B}(a)$ . Then, denoting $(p_1\circ h)(a,b)$ by $a_p$ we can define $\widetilde {h} (b)$ as $\eta _{a_p,a} ( r,(p_2 \circ h) (a,b))$ which is an element of $\textsf {C}(a)$ . Such an arrow $\widetilde {h}$ determines in fact an arrow in $Dep_{\textbf {pEff}}(\textsf {A},\textsf {R})$ from $(\textsf {B},[\textsf {S}],\sigma )$ and $(\textsf {C},[\textsf {H}],\eta )$ using the properties of the original arrow h. Indeed, informally, if there is a realizer of $\textsf {S}_a(b,b')$ , then $(a,b)$ and $(a,b')$ are equivalent in the domain of $\mathbf {K}((\textsf {B},[\textsf {S}],\sigma ) ))$ . Hence $h(a,b)$ and $ h(a,b')$ are equivalent in the domain of $ \mathbf {K} (( \textsf {C},[\textsf {H}],\eta )) $ , namely there exists a realizer s satisfying $s\Vdash \textsf {R}( \, (p_1 \circ h) (a,b),(p_1 \circ h) (a,b'))$ and $\textsf {H}(\eta _{a_1,a_2}( s, (p_2 \circ h) (a,b)), (p_2 \circ h) (a,b') )$ after denoting $(p_1 \circ h) (a,b)$ by $a_1$ and $(p_1 \circ h) (a,b')$ by $a_2$ . Now, since there exist $r_1\Vdash \textsf {R} ((p_1 \circ h) (a,b),\, a) $ and $r_2\Vdash \textsf {R} ((p_1 \circ h) (a,b'),\, a)$ we get $\textsf {H} (\eta _{a_1,a}( \textsf {tra}(s,r_2), (p_2 \circ h) (a,b)), \, \eta _{a_2,a}( r_2, (p_2 \circ h) (a,b'))) $ because $\eta $ is well-behaved with respect to composition of realizers. Then, by the independence of realizers $\textsf {H}( \eta _{a_1,a}( \textsf {tra}(s,r_2),\, (p_2 \circ h) (a,b)),\,\,\eta _{a_1,a} ( r_1, (p_2 \circ h) (a,b) ))$ holds, from which by transitivity of $\textsf {H}$ we conclude $\textsf {H}(\widetilde {h}(b),\widetilde {h}(b'))$ and hence, $\widetilde {h}$ is well defined. To prove that $\widetilde {h}$ commutes with the transport maps, we have to show that for every $a,a'\in \textsf {A}$ and $s\Vdash \textsf {R}(a,a')$ and $b\in \textsf {B}(a)$ , then $\widetilde {h}(\sigma _{a,a'}(s,b))$ is equal to $\eta _{a,a'}(s, \widetilde {h}(b))$ . The former term is equal to $\eta _{a_2,a'} (r_2,(p_2\circ h)(a',\sigma _{a,a'}(s,b)))$ for $r_2\Vdash \textsf {R}(a_2,a')$ , where $a_2:=(p_1\circ h)(a',\sigma _{a,a'}(s,b))$ .

While the latter is equal to $\eta _{ a,a'}(s,\eta _{a_1,a}(r_1,(p_2\circ h)(a,b)))$ , for $r_1\Vdash \textsf {R}(a_1,a)$ with $a_1:=(p_1\circ h)(a,b)$ . Since h preserves equality and $(a,b)$ is equal to $(a',\sigma _{a,a'}(s,b))$ in the domain of $ \mathbf {K} (( \textsf {B},[\textsf {S}],\sigma )) $ , then there exists a term u for which $u\Vdash \textsf {R} ((p_1\circ h)(a,b),(p_1\circ h)(a',\sigma _{a,a'}(s,b)))$ for which we get the validity of $\textsf {H}_{a_1}(\eta _{a_2,a_1} (u, (p_2\circ h)(a,b)), (p_2\circ h)(a', \sigma _{a,a'}(s,b)))$ . Hence, the statement follows since $\eta $ preserve equalities and is well-behaved with respect to composition.

Faithfulness is immediate once one notices that the equivalence of arrows h’s in $\textbf {pEff}/(\textsf {A},[\textsf {R}])$ in the image of $\mathbf {K}$ corresponds exactly to the equivalence of the corresponding $\widetilde {h}$ ’s in $Dep_{\textbf {pEff}}(\textsf {A},\textsf {R})$ .

Now given an object $[\textsf {f}]_{\cong }:(\textsf {A}', [\textsf {R}']) \to (\textsf {A},[\textsf {R}])$ in $\textbf {pEff}/(\textsf {A},[\textsf {R}])$ , we build a triple $(\textsf {B}^{\textsf {f}}, [\textsf {S}]^{\textsf {f}}, \sigma ^{\textsf {f}})$ in $Dep_{\textbf {pEff}}(\textsf {A},{\textsf {R}})$ . In order to do that, we consider the arrow $p_1:\textsf {A}\times \textsf {A}'\to \textsf {A}$ and define $\textsf {B}^{\textsf {f}}:=\Sigma _{p_1}(\mathbf {Col}^r_{ (\textsf {id}_{\textsf {A}}\times \textsf {f})}(\textsf {R}))$ . Intuitively, $\textsf {B}^{\textsf {f}}(a)$ is given by pairs $(a', k)$ where $a'\in \textsf {A}'$ and $k \Vdash \textsf {R}(a, \textsf {f}(a')) $ . Then we define

$$ \begin{align*}[\textsf{S}]^{\textsf{f}}:=\overline{\mathbf{Prop}^r}_{(\textsf{snd}^{\textsf{f}}\times\textsf{snd}^{\textsf{f}})\circ\langle\mathbf{I}_{\textsf{A}}(p_1),\mathbf{I}_{\textsf{A}}(p_2)\rangle}([\textsf{R}'])\end{align*} $$

to be the relation $\textsf {R'}$ on the $\textsf {A}'$ components of $\textsf {B}^{\textsf {f}}$ where

$$ \begin{align*}\textsf{snd}^{\textsf{f}}:= [\Lambda x.\{\mathbf{p}_2\}(\{\mathbf{p}_1\}(\{\mathbf{p}_2\}(x)))]_\approx:\Sigma(\textsf{A},\Sigma_{p_1}(\mathbf{Col}^r_{ (\textsf{id}_{\textsf{A}}\times \textsf{f})}(\textsf{R})))\to \textsf{A}'\end{align*} $$

and $\mathbf {I}_{\textsf {A}}(p_i):\Sigma (\textsf {A},\Sigma _{p_1}(\mathbf {Col}^r_{ (\textsf {id}_{\textsf {A}}\times \textsf {f})}(\textsf {R})\times \mathbf {Col}^r_{ (\textsf {id}_{\textsf {A}}\times \textsf {f})}(\textsf {R})))\to \Sigma (\textsf {A},\Sigma _{p_1}(\mathbf {Col}^r_{ (\textsf {id}_{\textsf {A}}\times \textsf {f})}(\textsf {R})))$ , for $i=1,2$ .

Finally, we can define $\sigma ^{\textsf {f}}$ as the arrow which sends a triple $(r,(a', k))$ with $(a', k)\in \textsf {B}^{\textsf {f}}(a_1)$ and $r \Vdash \textsf {R}(a_1, a_2)$ to the pair $(a', \textsf {tr}(\textsf {sym}(r), k))\in \textsf {B}^{\textsf {f}}(a_2)$ where $\textsf {tr}(\textsf {sym}(r), k)\Vdash \textsf {R}(a_2, \textsf {f}(a'))$ and $\textsf {refl, sym}$ , and $\textsf {tr}$ are some chosen witnesses of the reflexivity, symmetry, and transitivity of $\textsf {R}$ . We leave this to the reader.

Now we can observe that $\mathbf {K}(\textsf {B}^{\textsf {f}}, [\textsf {S}]^{\textsf {f}}, \sigma ^{\textsf {f}})\cong [\textsf {f}]_{\cong }$ . Indeed, there is an obvious arrow from $\Sigma (\textsf {A},\textsf {B}^{\textsf {f}})$ to $\textsf {A}'$ which takes the $\textsf {A}'$ component of $\textsf {B}^{\textsf {f}}$ to itself. Vice versa, given an element $a'\in \textsf {A}'$ , we can consider the triple $(\textsf {f}(a'), (a', \textsf {refl}))\in \Sigma (\textsf {A},\textsf {B})$ . These arrows are inverse thanks to the relations $[\textsf {R}']$ and $\exists _{d_{{\textsf {R}}}}(\overline {\mathbf {Prop}^r}_{t_\sigma }([\textsf {S}]^{\textsf {f}}))$ .

Remark 6.10. If $(\textsf {A},[\textsf {R}])$ is an object in $\textbf {pEff}$ and $\textsf {R},\textsf {R}'$ are two representatives of $[\textsf {R}]$ as in Lemma 6.7, then the image through $\mathbf {K}$ of the categories $Dep_{\textbf {pEff}}(\textsf {A}, {\textsf {R}})$ and $Dep_{\textbf {pEff}}(\textsf {A}, {\textsf {R}}')$ is the same, that is, the following diagram commutes:

We conclude this section by providing a direct correspondence between extensional dependent collections and internal groupoid action (see [Reference Janelidze and Tholen22, Reference MacLane and Moerdijk23] for a precise definition) in $\textbf {pEff}$ . Indeed, for every object $(\textsf {A},[\textsf {R}])\in \textbf {pEff}$ , consider the object $(\textsf {A},[=_{\textsf {A}}])$ where $=_{\textsf {A}}$ is the equality of the $\boldsymbol {\mathcal {C}}_r$ -object $\textsf {A}$ in the first-order hyperdoctrine $\overline {{\mathbf {Prop}^r}}$ in Theorem 3.14. Then, the kernel pair of the quotient arrow

$$\begin{align*}p:= [id_{\textsf{A}}]:(\textsf{A},[=_{\textsf{A}}])\to(\textsf{A},[\textsf{R}])\end{align*}$$

induces an internal groupoid $\textsf {Ker}(p, {\textsf {R}})$ obtained through the kernel pair of p.

and for any other representative ${\textsf {R}}'\in [\textsf {R}]$ the two internal groupoids are isomorphic in the category of internal groupoids of $\textbf {pEff}$ .

Indeed, denoting with $\mathcal {Des}(p, {\textsf {R}})$ the category of the actions of $\textsf {Ker}(p, {\textsf {R}})$ in $\textbf {pEff}$ , we obtain the following result.

Proposition 6.11. Let $(\textsf {A},[\textsf {R}])$ be an object in $\mathbf {pEff}$ and

$$\begin{align*}p:= [id_{\textsf{A}}]:(\textsf{A},[=_{\textsf{A}}])\to(\textsf{A},[\textsf{R}])\end{align*}$$

the above mentioned quotient map. There exists a full and faithful essentially surjective functor

$$ \begin{align*}F:Dep_{\mathbf{pEff}}(\textsf{A}, {\textsf{R}})\to \mathcal{Des}(p, {\textsf{R}}).\end{align*} $$

Proof. By general descent theory, there exists a canonical comparison functor (see [Reference Janelidze and Tholen22, Section 2.2])

$$\begin{align*}\Phi^{p,{\textsf{R}}}: \textbf{pEff}/(\textsf{A},[\textsf{R}])\to \mathcal{Des}(p, {\textsf{R}}).\end{align*}$$

Since p is a regular epimorphism and $\textbf {pEff}$ is exact, then we obtain that p is an effective descent morphism, that is, the functor $\Phi ^{p, {\textsf {R}}}$ is full, faithful, and essentially surjective (see [Reference Janelidze and Tholen22, Section 2.4]). The functor F is defined as the composition of $\mathbf {K}$ and $\Phi ^{p,\textsf {R}}$ .

7 The structure of fibred extensional sets on $\textbf {pEff}$

We study the categorical structure of extensional dependent sets, introduced in Definition 6.6, as a subfibration of the codomain fibration of $\textbf {pEff}$ denoted with

$$\begin{align*}\textsf{cod}_{set}:\textbf{pEff}^\to_{set}\to\textbf{pEff}.\end{align*}$$

Fibrations are needed because families of collections and sets lose functoriality under substitution when lifted to extensional objects over $\textbf {pEff}$ . Since slice categories naturally represent families of collections over an object of $\textbf {pEff}$ , we work inside the codomain fibration over $\textbf {pEff}$ .

To this end, we exploit the functor $\mathbf {K}$ of Proposition 6.8 and first prove the following result.

Lemma 7.1. Let $[p]:(\textsf {A}',[\textsf {R}'])\to (\textsf {A},[\textsf {R}]),$ be an arrow in $\mathbf {pEff}$ . If $[f]\in \mathbf {pEff}/(\textsf {A},[\textsf {R}])$ is isomorphic to the image through $\mathbf {K}$ of an extensional dependent set $(\textsf {B},[\textsf {S}],\sigma )\in Dep_{\mathbf {pEff}_{set}}(\textsf {A}, {\textsf {R}}) $ , then $[p]^*[f]$ is isomorphic to the image through $\mathbf {K}$ of an element in $Dep_{\mathbf {pEff}_{set}}(\textsf {A}, {\textsf {R}'}) $ .

Proof. We assume that $[f]$ is isomorphic to $\mathbf {K}((\textsf {B},[\textsf {S}],\sigma ))$ , then we can choose two representatives $f:\textsf {A}'\to \textsf {A}$ in $\boldsymbol {\mathcal {C}}_r$ and $g:\textsf {R}'\to \mathbf {Prop}^r_f(\textsf {R})$ in $\overline {{\mathbf {Prop}^r_{\mathbf {s}}}}(\textsf {A}\times \textsf {A})$ (recall that $\overline {{\mathbf {Prop}^r_{\mathbf {s}}}}(\textsf {A}\times \textsf {A})$ is the poset reflection of $\mathbf {Set}^r(\textsf {A}\times \textsf {A})$ ) for $[f]$ and consider the extensional dependent set

$$ \begin{align*}(\mathbf{Set}^r_{p}(\textsf{B}),(\overline{{\mathbf{Prop}^r_{\mathbf{s}}}})_{\Sigma(p,\textsf{B}\times \textsf{B})}([\textsf{S}]),\mathbf{Set}^r_{p\times p}(\sigma)\circ (\textsf{id}\times g))\end{align*} $$

in $Dep_{\textbf {pEff}_{set}}(\textsf {A}, {\textsf {R}'}) $ and observe that its image through $\mathbf {K}$ is isomorphic to the pullback $[p]^*[f]$ .

Definition 7.2. We denote by $\textbf {pEff}_{set}^\to $ the full subcategory of $\textbf {pEff}^\to $ whose objects are arrows isomorphic to arrows in $\mathbf {K}(Dep_{\textbf {pEff}_{set}}(\textsf {A}, {\textsf {R}}))$ for (any) representative $\textsf {R}$ of $[\textsf {R}]$ .

We denote with $\textsf {cod}_{set}$ the restriction of the codomain functor obtaining the following commutative diagram:

Lemma 7.1 implies the following result.

In the following, $\textsf {cod}_{set}^{-1}(\textsf {A},[\textsf {R}])$ denotes the fiber of $\textsf {cod}_{set}$ over the object $(\textsf {A},[\textsf {R}])$ .

Remark 7.4. Similar to Lemma 3.8, any arrow $[\textsf {h}]$ in $\textsf {cod}_{set}^{-1}(\textsf {A},[\textsf {R}])$ between two arrows isomorphic to the image through $\mathbf {K}$ of two objects $(\textsf {B},\textsf {S},\sigma )$ and $(\textsf {C},\textsf {H},\eta )$ in $Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$

$$\begin{align*}[\textsf{h}]:\mathrm{dom}(\mathbf{K}(\textsf{B},\textsf{S},\sigma)\to \mathrm{dom}(\mathbf{K}(\textsf{C},\textsf{H},\eta))\end{align*}$$

is itself in $\mathrm {cod}_{set}^{-1}(\textsf {dom}(\mathbf {K}(\textsf {C},\textsf {H},\eta ))$ .

We now study the categorical property of these fibrations.

To do that, instead of working with slice categories over $(\textsf {A},[\textsf {R}])\in \textbf {pEff}$ , we exploit the categories of extensional dependent collections and sets and prove their properties. This is enough thanks to Proposition 6.8 and Remark 6.9. Furthermore, the following results do not depend on the chosen representative of $[\textsf {R}]$ thanks to Lemma 6.7 and Remark 6.10.

Before moving to the main theorem of the section, we provide a characterization of monomorphisms for families of collections, which will be instrumental in proving part of the theorem.

To this end, we recall [Reference Maietti and Maschio27, Definition 5.6].

Definition 7.5. Let $\textbf {pEff}_{prop}:\textbf {pEff}^{\mathrm{op}}\to \mathbf {Pos}$ denote the elementary quotient completion of $\overline {{\mathbf {Prop}^r}}:\boldsymbol {\mathcal {C}}_r^{\mathrm {op}}\to \mathbf {Pos}$ whose value on an object $(\textsf {A},[\textsf {R}])$ is given by the descent data of $\overline {{\mathbf {Prop}^r}}(\textsf {A})$ , that is, it is the sub partial order $\textbf {pEff}_{prop}(\textsf {A},[\textsf {R}])$ of $\overline {{\mathbf {Prop}^r}} (\textsf {A})$ whose objects are those in

(10) $$ \begin{align} \left\{[\textsf{P}]\in\overline{{\mathbf{Prop}^r}}(\textsf{A})\ |\ \; \overline{{\mathbf{Prop}^r}}_{p_1}([\textsf{P}])\wedge [\textsf{R}] \le \overline{{\mathbf{Prop}^r}}_{p_2}([\textsf{P}])\right\},\end{align} $$

where $p_i:\textsf {A}\times \textsf {A}\to \textsf {A}$ are the projections for $i=1,2$ , and whose action on arrows is given by that of $\overline {{\mathbf {Prop}^r}}$ .

From [Reference Maietti and Maschio27] we recall the following result, which appears there as Theorem 5.7.

Now we are ready to provide a characterization of monomorphisms as a consequence of the general characterization established in [Reference Maietti, Pasquali and Rosolini30, Proposition 2.33], refining [Reference Maietti and Rosolini32, Corollary 4.8].

Lemma 7.7. Let $(\textsf {A},[\textsf {R}])$ be an object of $\mathbf {pEff}$ . An arrow $[\textsf {m}]:(\textsf {B},[\textsf {S}],\sigma )\rightarrow (\textsf {C},[\textsf {H}],\nu )$ in $Dep_{\mathbf {pEff}}(\textsf {A},{\textsf {R}})$ is a monomorphism if and only if

$$ \begin{align*}[\textsf{S}]=\overline{\mathbf{Prop}^r}_{\mathbf{I}(\textsf{m}\times \textsf{m})}([\textsf{H}]).\end{align*} $$

Proof. Let us consider the functor

$$\begin{align*}U:Dep_{\textbf{pEff}}(\textsf{A},\textsf{R})\to \textbf{pEff}\end{align*}$$

which “forgets” the $\sigma $ -component faithfully and is defined by composing the functor $\mathbf {K}$ with the domain functor $\textbf {pEff}/(\textsf {A},[\textsf {R}])\to \textbf {pEff}$ . Since U is faithful, it reflects monomorphisms. Hence, using [Reference Maietti, Pasquali and Rosolini30, Proposition 2.33] applied to the doctrine $\textbf {pEff}_{prop}$ , which has the necessary hypothesis thanks to Theorem 7.6, we obtain that the arrow

$$ \begin{align*}U([\textsf{m}])=[\mathbf{I}(\textsf{m})]:(\Sigma(\textsf{A},\textsf{B}),\exists_{d_{\textsf{R}}}\overline{{\mathbf{Prop}^r}}_{t_\sigma}[\textsf{S}])\to (\Sigma(\textsf{A},\textsf{C}),\exists_{d_{\textsf{R}}}\overline{{\mathbf{Prop}^r}}_{t_\nu}[\textsf{H}])\end{align*} $$

is a monomorphism in $\textbf {pEff}$ if and only if

$$\begin{align*}\exists_{d_{\textsf{R}}}\overline{{\mathbf{Prop}^r}}_{t_\sigma}[\textsf{S}]=\overline{{\mathbf{Prop}^r}}_{\mathbf{I}(\textsf{m})\times\mathbf{I}(\textsf{m})}(\exists_{d_{\textsf{R}}}\overline{{\mathbf{Prop}^r}}_{t_\nu}[\textsf{H}]),\end{align*}$$

which is equivalent to

$$ \begin{align*}[\textsf{S}]=\overline{\mathbf{Prop}^r}_{\mathbf{I}(\textsf{m}\times \textsf{m})}([\textsf{H}])\end{align*} $$

by definition of the arrows $d_{\textsf {R}}$ and $t_\sigma $ in the proof of Proposition 6.8 and the properties of $[\textsf{S}]$ and $[\textsf{H}]$ .

Remark 7.8. The same result can be obtained in this alternative way. Consider to lift the doctrine $\overline {{\mathbf {Prop}^r}}$ over the slice of $\boldsymbol {\mathcal {C}}_r$ over $\textsf {A}\in \boldsymbol {\mathcal {C}}_r$ as done in [Reference Cioffo11]:

$$ \begin{align*}(\overline{{\mathbf{Prop}^r}})_{/\textsf{A}}: (\boldsymbol{\mathcal{C}}_r/\textsf{A})^{\mathrm{op}}\rightarrow\mathbf{Pos},\end{align*} $$

the action on an object $\textsf {f}:\textsf {X}\to \textsf {A}$ of $\boldsymbol {\mathcal {C}}_r$ is given by ${\mathbf {Prop}^r}(\textsf {X})$ , and the action on an arrow from $\textsf {f}$ to $\textsf {g}:\textsf {Y}\to \textsf {A}$ (which is an arrow $\textsf {h}:\textsf {X}\to \textsf {Y}$ such that $\textsf {g}\circ \textsf {h}=\textsf {f}$ ) is given by ${\mathbf {Prop}^r}_{\textsf {f}}$ . Then, consider the elementary quotient completion of ${(\overline {{\mathbf {Prop}^r}})_{/\textsf {A}}}$ and observe that there exists a forgetful functor

$$\begin{align*}U:Dep_{\textbf{pEff}}(\textsf{A},\textsf{R})\to \mathcal{Q}_{(\overline{{\mathbf{Prop}^r}})_{/A}}\end{align*}$$

which “forgets” the $\sigma $ -component in a faithful way: it sends an object $(\textsf {B},\textsf {S},\sigma )$ to the pair $(\textsf {p}_1^\Sigma , \textsf {S})$ in $\mathcal {Q}_{(\overline {{\mathbf {Prop}^r}})_{/A}}$ , where $\textsf {p}_1^\Sigma :\Sigma (\textsf {A},\textsf {B})\to \textsf {A}$ . Since, as shown in [Reference Cioffo11], the elementary quotient completion of ${(\overline {{\mathbf {Prop}^r}})_{/A}}$ inherits some properties from $\overline {{\mathbf {Prop}^r}}$ , and in particular it has full strict comprehensions and comprehensive diagonals, [Reference Maietti and Rosolini32, Corollary 4.8] applied to it and faithfulness of U imply the same monomorphism characterization of Lemma 7.7.

Theorem 7.9. Let $(\textsf {A},[\textsf {R}])$ be an object of $\mathbf {pEff}$ . The categories $Dep_{\mathbf {pEff}}(\textsf {A},\textsf {R})$ and $Dep_{\mathbf {pEff}_{set}}(\textsf {A},\textsf {R})$ are locally cartesian closed list-arithmetic pretoposes.

Proof. Since, $\textbf {pEff}$ is equivalent to an exact completion of a lex category (see [Reference Maietti and Maschio27]) and $\mathbf {K}:Dep_{\textbf {pEff}}(\textsf {A}, {\textsf {R}})\rightarrow \textbf {pEff}/(\textsf {A},[\textsf {R}])$ preserves and reflects all limits, colimits, and exponentials, in the case of families of collection Theorem 7.9 follows from the properties of the exact completion. Indeed, exactness and local cartesian closure are preserved under slicing, such as extensivity (see [Reference Carboni, Lack and Walters8]) and parametrized list objects (see [Reference Maietti24]). However, when restricting to $\textsf {cod}_{set}^{-1}(\textsf {A},[\textsf {R}])$ we must check that the above properties restrict to a proper subcategory of $\textbf {pEff}/(\textsf {A},[\textsf {R}])$ . Hence, we provide directly a proof of the result for $Dep_{\textbf {pEff}}(\textsf {A},\textsf {R})$ to be able to restrict to $Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$ and hence to $\textsf {cod}_{set}^{-1}(\textsf {A},[\textsf {R}])$ .

Finite limits.

1. 1. A terminal object in $Dep_{\textbf {pEff}}(\textsf {A},\textsf {R})$ is given by $(1,\top ,!)$ . This is a terminal object also in $Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$ .

2. 2. A binary product of $(\textsf {B},[\textsf {S}],\sigma ) $ and $(\textsf {C},[\textsf {H}], \nu )$ is given by

   $$\begin{align*}(\textsf{B}\times \textsf{C}, \overline{\textbf{Prop}^r}_{\textbf{I}( p_1 \times p_1)}([\textsf{S}]) \wedge \overline{\textbf{Prop}^r}_{\textbf{I}( p_2 \times p_2)}([\textsf{H}]),\langle \sigma \circ (\textsf{id}_{\textsf{R}} \times p_1), \nu \circ(\textsf{id}_{\textsf{R}}\times p_2\rangle) \end{align*}$$

   with projections inherited by those of $\textsf {B}\times \textsf {C}$ . Since the product of two sets is a set and the conjunction of small propositions is a small proposition, the above construction restricts to $Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$ .

3. 3. An equalizer of two arrows $[\textsf {f}],[\textsf {g}]: (\textsf {B},[\textsf {S}],\sigma )\rightarrow (\textsf {C},[\textsf {H}],\nu )$ is given by

   $$\begin{align*}(\Sigma^{\textsf{A}}(\textsf{B}, \mathbf{Col}^r_{\mathbf{I}(\langle {\textsf{f}},\textsf{g} \rangle) }(\textsf{H})\, ), \overline{\textbf{Prop}^r}_{\textbf{I}(\textsf{p}_1^{\textsf{A},\Sigma}\times \textsf{p}_1^{\textsf{A},\Sigma})}([\textsf{S}]),\eta),\end{align*}$$

   where $\eta _{a,a'}$ acts as $\sigma _{a,a'}(r,b)$ on a realizer $r\Vdash \textsf {R}(a,a')$ , a term $b:\textsf {B}(a)$ and a realizer $q:\textsf {H}_a(\textsf {f}(a),\textsf {g}(a))$ since a realizer $q':\textsf {H}_{a'}(\textsf {f}(\sigma _{a,a'}(r,b)),\textsf {g}(\sigma _{a,a'}(r,b)))$ can be found by transitivity from the terms $q_\nu :\textsf {H}_{a'}(\nu _{a,a'}(r,\textsf {f}(b)),\nu _{a,a'}(r,\textsf {g}(b)))$ (from condition 1 of Definition 6.2 for $\nu $ ) and $u:\textsf {H}_{a'}(\textsf {f}(\sigma _{a,a'}(r,b)),\nu _{a,a'}(r,\textsf {f}(b)))$ , and $v:\textsf {H}_{a'}(\nu _{a,a'}(r,\textsf {g}(b)),\textsf {g}(\sigma _{a,a'}(r,b)))$ (from condition 2 of Definition 6.3 for $\textsf {f}$ and $\textsf {g}$ and symmetry). The same construction provides equalizers in $Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$ .

Stable finite coproducts. An initial object is given by $(0,\top , \sigma )$ where $\sigma $ is the unique possible one. A coproduct for $(\textsf {B},[\textsf {S}],\sigma )$ and $(\textsf {C},[\textsf {H}],\nu )$ is given by

$$ \begin{align*}(\textsf{B}+\textsf{C},[\textsf{S}]{+}[\textsf{H}],(\sigma{+}\nu)j),\end{align*} $$

where

1. 1. $[\textsf {S}]{+}[\textsf {H}]=\exists _{\mathbf {I}(i_1\times i_1)}([\textsf {S}])\vee \exists _{\mathbf {I}(i_2\times i_2)}([\textsf {H}])$ ;

2. 2. j is the canonical isomorphism from the object ${\textsf {R}}\times (\mathbf {Col}^r_{p_1}(\textsf {B})+\mathbf {Col}^r_{p_1}(\textsf {C}))$ to $ ({\textsf {R}}\times \mathbf {Col}^r_{p_1}(\textsf {B}))+({\textsf {R}}\times \mathbf {Col}^r_{p_1}(\textsf {B}))$ which exists since $\mathbf {Col}^{r}(\textsf {A}\times \textsf {A})$ is extensive.

Their injections are $[i_1]$ and $[i_2]$ for $i_1$ and $i_2$ injections of $\textsf {B}+\textsf {C} $ and they are monic thanks to [Reference Maietti, Pasquali and Rosolini30, Proposition 6.35]. One can check that coproducts are stable under pullbacks using pullbacks constructed through the finite limits of $Dep_{\textbf {pEff}}(\textsf {A},\textsf {R})$ and $Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$ described above. Initial objects are trivially stable, since they are stable in $\mathbf {Col}^{r}(\textsf {A})$ .

These constructions provide stable finite coproducts also in $Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$ using the same arguments together with Theorem 3.16 and Lemma 3.8.

List objects. A list object for $(\textsf {B},[\textsf {S}],\sigma _{\textsf {B}})$ is given by $(\textsf {List}(\textsf {B}),[\textsf {S}_{list}],\sigma _{list})$ where

1. 1. the relation $\textsf {S}_{list}$ holds on two lists $x,y$ if they have the same length $l(x)=_{\textsf {N}}l(y)$ and they have the same components:

   $\exists u'\varepsilon \ 1 \ \exists v'\varepsilon \ 1 \ (i_2(u')=_{B(a)+1}\textsf {comp}(x,n)\wedge i_2(v')=_{B(a)+1}\textsf {comp}(y,n)) )\ \vee \ \\ \forall n\ \varepsilon \ \textsf {N}(\exists u\ \varepsilon \ \textsf {B}(a) \ \exists v\ \varepsilon \ \textsf {B}(a)(\textsf {S}_a(u,v)\wedge i_1(u)=_{\textsf {B}(a)+1}\textsf {comp}(x,n)\wedge i_1(v)=_{\textsf {B}(a)+1}\textsf {comp}(y,n)) $ , thatis,

   $$ \begin{align*}\textsf{S}_{list}=\overline{{\mathbf{Prop}^r}}_{\mathbf{I}(\ell\times \ell)}(\exists_{\mathbf{I}(\Delta_{\textsf{N}})}(\top))\wedge\qquad\qquad\qquad\qquad\qquad\qquad\qquad\end{align*} $$
   $$ \begin{align*}\forall_{\mathbf{I}(p_1)}(\overline{{\mathbf{Prop}^r}}_{\mathbf{I}((\langle\textsf{comp}\circ (p_1\times \textsf{id}_{\textsf{N}}))\times (\langle\textsf{comp}\circ (p_2\times \textsf{id}_{\textsf{N}})))}(\exists_{\mathbf{I}(i_1\times i_1)}([\textsf{S}])\vee \exists_{\mathbf{I}(i_2\times i_2)}(\top) ))\end{align*} $$

   where $\ell $ is the length arrow from $\textsf {List}(\textsf {B})\rightarrow \textsf {N}$ in $\mathbf {Col}^r(\textsf {A})$ and $\textsf {comp}:\textsf {List}(\textsf {B})\times \textsf {N}\rightarrow \textsf {B}+1$ is the component arrow in $\mathbf {Col}^r(\textsf {A})$ which selects the n-component of a list.

2. 2. $\sigma _{list}$ is the unique arrow in $\mathbf {Col}^r(\textsf {A})$ making the following diagram commute:

   

These constructions can also be performed in $Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$ thanks to Theorem 3.16 and Lemma 3.8.

Exactness. Recall that $\textbf {pEff}$ is exact and that the slice categories of an exact category are also exact. Hence, exactness of $Dep_{\textbf {pEff}}(\textsf {A},\textsf {R})$ follows from the fact that $\mathbf {K}:Dep_{\textbf {pEff}}(\textsf {A},\textsf {R})\to \textbf {pEff}/(\textsf {A},[\textsf {R}])$ is a fully and faithful essentially surjective functor. To prove that $Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$ is also exact, observe that the coequalizer of an equivalence relation on $(\textsf {B},[\textsf {S}], \sigma )\in Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$ ,

$$ \begin{align*}[\textsf{c}]:(\textsf{C},[\textsf{H}],\nu)\to (\textsf{B},[\textsf{S}], \sigma)\times (\textsf{B},[\textsf{S}], \sigma)\end{align*} $$

is given by

$$ \begin{align*}[\textsf{id}_{\textsf{B}}]:(\textsf{B},[\textsf{S}], \sigma)\to(\textsf{B}, [\textsf{S}'], \sigma),\end{align*} $$

where

$$ \begin{align*}[\textsf{S}']:= \exists_{\mathbf{I}(\langle p_2,p_3\rangle)}(\overline{{\mathbf{Prop}^r}}_{\mathbf{I}(\textsf{c}_{\textsf{1}}\times p_1)}([\textsf{S}])\wedge \overline{{\mathbf{Prop}^r}}_{\mathbf{I}(\textsf{c}_{\textsf{2}}\times p_2)}([\textsf{S}]))\end{align*} $$

supposed $[\textsf {c}_1]=p_1\circ [\textsf {c}]$ and $[\textsf {c}_2]=p_2\circ [\textsf {c}]$ .

Applying the functor $\mathbf {K}$ defined in Proposition 6.8 to $[\textsf {id}_{\textsf {B}}]$ we get

$$\begin{align*}[\mathbf{I}(\textsf{id}_{\textsf{B}})]:(\Sigma(\textsf{A},\textsf{B}),\exists_{d_{\textsf{R}}}\overline{{\mathbf{Prop}^r}}_{t_\sigma}([\textsf{S}]))\to (\Sigma(\textsf{A},\textsf{B}),\exists_{d_{\textsf{R}}}\overline{{\mathbf{Prop}^r}}_{t_\sigma}([\textsf{S}']))\end{align*}$$

which is a coequalizer in $\textbf {pEff}/(\textsf {A},[\textsf {R}])$ of $\mathbf {K}([\textsf {c}])$ and hence in $\textsf {cod}_{set}^{-1}(\textsf {A},[\textsf {R}])$ by Remark 7.4. Stability and effectiveness follow from the pullback property in Lemma 7.1.

Local cartesian closure. For two objects $(\textsf {B},[\textsf {S}],\sigma )$ and $(\textsf {C},[\textsf {H}],\nu )$ in $Dep_{\textbf {pEff}}(\textsf {A},\textsf {R})$ consider the triple $( \textsf {C}^{\textsf {B}}, [\textsf {H}]^{[\textsf {S}]}, {\nu }^{\sigma })$ defined as follows. First, the object $\textsf {C}^{\textsf {B}}$ is defined as $\Sigma ^{\textsf {A}}(\textsf {B}\Rightarrow \textsf {C},\Pi _{p_1}({\mathbf {Col}^r}_{\mathbf {I}(p_2)}(\textsf {S})\to {\mathbf {Col}^r}_{\mathbf {I}(\langle \textsf {ev}\circ (\textsf {id}\times p_1),\textsf {ev}\circ (\textsf {id}\times p_2) \rangle )}(\textsf {H}))$ where $\textsf {B}\Rightarrow \textsf {C}$ and $\textsf {ev}$ denote the weak exponential and the corresponding evaluation in $\mathbf {Col}^r(\textsf {A})$ . Intuitively, we restrict to those arrows $f_a\in \textsf {B}(a) \Rightarrow \textsf {C}(a)$ whose evaluation preserves $\textsf {S}$ and $\textsf {H}$ , that is, there exists a realizer s for which we have $s\Vdash (\forall b,b'\in \textsf {B}(a))\ (\textsf {S}_a(b,b')\to \textsf {H}_a(f_a(b),f_a(b')))$ .

The relation $[\textsf {H}]^{[\textsf {S}]}$ is given by $\forall _{\mathbf {I}({p_1})}({\overline {{\mathbf {Prop}^r}}}_{\mathbf {I}(\langle \textsf {ev}\circ (p_1\times \textsf {id}),\textsf {ev}\circ (p_2\times \textsf {id}) \rangle )}([\textsf {H}]))$ . Intuitively, we relate two arrows $f_a, g_a\in \textsf {B}(a) \Rightarrow \textsf {C}(a)$ when there exists a realizer r for which we have $r\Vdash (\forall b\in \textsf {B}(a))\ \textsf {H}_a(f_a(b),g_a(b))$ .

The action $\sigma ^{\nu }_{a_1,a_2}$ is defined on a triple $(r,(f_{a_1}, s))$ , where $r\Vdash \textsf {R}(a_1, a_2)$ , as the pair with and is obtained through s and compatibility of $\sigma $ and $\nu $ with the corresponding equalities in condition (1) of Definition 6.2, and a witness $\textsf {sym}$ of the symmetry of $\textsf {R}$ .

We now observe that the evaluation arrow $\textsf {ev}: (\textsf {B}\Rightarrow \textsf {C})\times \textsf {B}\to \textsf {C}$ preserves $[\textsf {H}]^{[\textsf {S}]}$ , $[\textsf {H}]$ , and $[\textsf {S}]$ . In the sense that, if $((f_a,s),b)$ and $((f^{\prime }_a, s'),b')$ are such that $r\Vdash \textsf {H}_a(f_a(b),f^{\prime }_a(b))$ and $u\Vdash \textsf {S}(b, b')$ , then using $s'$ (applied to u), r, and the transitivity of $[\textsf {H}]$ we obtain a $q\Vdash \textsf {H}_a(f_a(b),f^{\prime }_a(b'))$ .

Hence, the evaluation arrow of $( \textsf {C}^{\textsf {B}}, [\textsf {H}]^{[\textsf {S}]}, {\nu }^{\sigma })$ is given by $[\textsf {ev}]$ and we get an exponential object instead of a weak exponential as it happened in $\mathbf {Col}^r$ .

Since weak exponentials of two sets are sets and small propositions are closed under connectives and quantification over sets, we obtain that the above construction restricts to $Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$ .

The local cartesian closure of $Dep_{\textbf {pEff}}(\textsf {A},\textsf {R})$ follows by observing that $\mathbf {K}:Dep_{\textbf {pEff}}(\textsf {A},\textsf {R})\rightarrow \textbf {pEff}/(\textsf {A},[\textsf {R}])$ induces a fully faithful and essentially surjective functor between the slice categories

$$ \begin{align*}\mathbf{K}/(\textsf{B},[ \textsf{S}], \sigma):Dep_{\textbf{pEff}}(\textsf{A},\textsf{R})/(\textsf{B}, [\textsf{S}], \sigma)\rightarrow(\textbf{pEff}/(\textsf{A},[\textsf{R}]))/\mathbf{K}(\textsf{B}, [\textsf{S}], \sigma)\end{align*} $$

for every object $(\textsf {B}, [\textsf {S}], \sigma )\in Dep_{\textbf {pEff}}(\textsf {A},\textsf {R})$ . Moreover, we have the isomorphism

$$ \begin{align*}(\textbf{pEff}/(\textsf{A},[\textsf{R}]))/\mathbf{K}(\textsf{B}, [\textsf{S}], \sigma)\cong\textbf{pEff}/\textsf{dom}(\mathbf{K}(\textsf{B}, [\textsf{S}], \sigma))\end{align*} $$

which, together with the fact that $\textbf {pEff}$ is locally cartesian closed, implies that $Dep_{\textbf {pEff}}(\textsf {A},\textsf {R})$ is locally cartesian closed by reflection of exponentials. To show that $Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$ is also locally cartesian closed, we observe that for every object $(\textsf {B}, [\textsf {S}], \sigma )\in Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$ , the functor $\mathbf {K}$ induces a fully faithful and essentially surjective functor

$$ \begin{align*}\mathbf{K}/(\textsf{B},[ \textsf{S}], \sigma):(Dep_{\textbf{pEff}_{set}}(\textsf{A},\textsf{R}))/(\textsf{B}, [\textsf{S}], \sigma)\rightarrow(\textsf{cod}_{set}^{-1}(\textsf{A},[\textsf{R}]))/\mathbf{K}(\textsf{B}, [\textsf{S}], \sigma).\end{align*} $$

By Remark 7.4 we also have the isomorphism

$$ \begin{align*}(\textsf{cod}_{set}^{-1}(\textsf{A},[\textsf{R}]))/\mathbf{K}(\textsf{B}, [\textsf{S}], \sigma)\cong\textsf{cod}_{set}^{-1}(\textsf{dom}(\mathbf{K}(\textsf{B}, [\textsf{S}], \sigma))).\end{align*} $$

Moreover, the functor $\mathbf {K}$ also induces a fully faithful essentially surjective functor

$$ \begin{align*}\mathbf{K}:Dep_{\textbf{pEff}_{set}}(\textsf{dom}(\mathbf{K}(\textsf{B}, [\textsf{S}], \sigma))\to\textsf{cod}_{set}^{-1}(\textsf{dom}(\mathbf{K}(\textsf{B}, [\textsf{S}], \sigma))).\end{align*} $$

Hence, by preservation and reflection of exponentials we conclude that $Dep_{\textbf {pEff}_{set}}(\textsf {A},\textsf {R})$ is also locally cartesian closed.

8 The “small subobjects” classifier

Let $\textbf {pEff}_{props}:\textbf {pEff}^{\mathrm {op}}\to \mathbf {Pos}$ denote the restriction of $\textbf {pEff}_{prop}$ on the fibers of $\overline {{\mathbf {Prop}^r_{\mathbf {s}}}}:\boldsymbol {\mathcal {C}}_r^{\mathrm {op}}\to \mathbf {Pos}$ . We now provide a similar correspondence for it to Theorem 7.6 regarding suitable subobjects.

Note that the above is a well-defined functor thanks to Lemma 7.1.

Applying the same argument in [Reference Maietti and Maschio27, Theorem 5.12], and combining it with the previous proposition, we obtain a classifier for small subobjects.

9 The fibred predicative topos structure of $\textbf {pEff}$ with its sets

We now summarize the main results obtained in this work.

Theorem 9.1. The category $\mathbf {pEff}$ is equipped with two fibrations

satisfying the following properties:

1. 1. $\mathbf {pEff}$ is a locally cartesian closed list arithmetic pretopos;

2. 2. for each $(\textsf {A},[\textsf {R}])\in \mathbf {pEff}$ the fiber $\textsf {cod}_{set}^{-1}(\textsf {A},[\textsf {R}])$

   is a locally cartesian closed list arithmetic pretopos;

3. 3. for every arrow $[f]:(\textsf {A},[\textsf {R}])\to (\textsf {A}',[\textsf {R}'])$ in $\mathbf {pEff}$ , the functor

   $$ \begin{align*}[f]^*:\textsf{cod}_{set}^{-1}(\textsf{A}',[\textsf{R}'])\to \textsf{cod}_{set}^{-1}(\textsf{A},[\textsf{R}])\end{align*} $$

   preserves the locally cartesian closed list-arithmetics pretopos structure;

4. 4. for each $(\textsf {A},[\textsf {R}])\in \mathbf {pEff}$ the inclusion $\textsf {cod}_{set}^{-1}(\textsf {A},[\textsf {R}])\to \mathbf {pEff}/(\textsf {A},[\textsf {R}])$ preserves the locally cartesian closed list-arithmetics pretopos structure;

5. 5. there exists an object $\Omega $ classifying $\mathbf {Sub}_{\mathbf {pEff}}^{\mathbf {s}}$ ;

6. 6. for every $[f]\in \textsf {cod}_{set}^{-1}(\textsf {A},[\textsf {R}])$ there exists an exponential object $(\pi _\Omega )^{[f]}$ in $\mathbf {pEff}/(\textsf {A},[\textsf {R}])$ where $\pi _{\Omega }:(\textsf {A},[\textsf {R}])\times \Omega \to (\textsf {A},[\textsf {R}])$ is the first projection;

7. 7. $\mathbf {pEff}$ satisfies the formal Church’s thesis (see [Reference Maietti and Maschio27, Theorem 5.8]).

Proof. 1. follows from Theorem 5.1 while 2. follows from Theorem 7.9 since $\textsf {cod}_{set}^{-1}(\textsf {A}',[\textsf {R}'])$ coincides with the replete image of $\mathbf {K}(Dep_{\textbf {pEff}_{set}}((\textsf {A}',[\textsf {R}']))$ . Then, 3. and 4. follow by the constructions in the proof of Theorem 7.9. Finally, 5. and 6. follows from Theorem 8.4 and Proposition 6.8.

The above properties testify that $\textbf {pEff}$ is a fibred predicative variant of Hyland’s Effective Topos. Indeed, the above properties are validated after substituting $\textbf {pEff}$ with ${\mathbf {Eff} }$ and identified fibred sets with all the objects of a slice category of ${\mathbf {Eff} }$ .

10 Towards a direct interpretation of $\mathbf {emTT}$ into $\textbf {pEff}$

The realizability interpretation for the intensional level of the Minimalist Foundation in [Reference Ishihara, Maietti, Maschio and Streicher20, Reference Maietti, Maschio and Rathjen28, Reference Maietti, Maschio and Rathjen29] can be turned into a morphism of doctrines from the syntactical doctrine $G^{{\mathbf {mTT}}}$ , arising from ${\mathbf {mTT}}$ (as introduced in [Reference Maietti and Rosolini32, Section 7.2]), to the doctrine $\overline {{\mathbf {Prop}^r}}$ , as illustrated on the left-hand side of the following diagram:

Such a morphism lifts to a morphism between the corresponding elementary quotient completions, as illustrated on the right-hand side of the diagram above. Now, observe that in the category $\mathcal {Q}_{G^{\mathbf {mTT}}}$ one can define an adequate notion of canonical isomorphisms, as done in [Reference Maietti25], thereby obtaining a model for $\mathbf {emTT}$ . Using this model together with the morphism on the right-hand side, and exploiting the fibered structure of $\textbf {pEff}$ developed in this article, we can construct a direct interpretation of $\mathbf {emTT}$ , also extended with inductive and coinductive predicates [Reference Maietti, Maschio and Rathjen28, Reference Maietti, Maschio and Rathjen29, Reference Maietti, Sabelli, Kerjean and Levy35, Reference Sabelli48], within $\textbf {pEff}$ .

11 Comparison with related works

In [Reference van den Berg and Moerdijk5], van den Berg and Moerdijk propose a construction of a predicative rendering of Hyland’s Effective Topos in the wider context of algebraic set theory. Starting from a category with small maps $(\mathcal {E},\mathcal {S})$ they first construct a category of assemblies $\mathcal {A}sm_{\mathcal {E}}$ endowed with a family of maps induced by $\mathcal {S}$ . Then, they identified its exact completion $(\mathcal {Eff}_{\mathcal {E}}, \mathcal {S}_{\mathcal {E}})$ as their notion of predicative realizability category, where $\mathcal {Eff}_{\mathcal {E}}$ is a suitable subcategory of the exact on regular completion of $\mathcal {A}sm_{\mathcal {E}}$ .

Our construction can be compared with theirs, as soon as we take for $\mathcal {E}$ , the category $\mathcal {E}[\mathbf {T}]$ of definable classes in an extension $\mathbf {T}$ of $\mathbf {CZF}$ having the numerical existence property, endowed with the collection $\mathcal {S}[\mathbf {T}]$ of set-fibered functional relations between them (see Section 8 of [Reference van den Berg and Moerdijk4]). Examples of such a theory $\mathbf {T}$ include $\mathbf {CZF}$ itself, $\mathbf {CZF}+\mathbf {REA}$ as proven in [Reference Rathjen44], and also $\mathbf {CZF}+\mathbf {RDC}+\bigcup -\mathbf {REA}$ (by adequately modifying the proof of Theorem 7.2 in [Reference Rathjen44] and combining it with Theorem 7.4 in [Reference Rathjen45]).

In such a category, assemblies are pairs $(A,\alpha )$ in which A is a definable class of $\mathbf {T}$ and $\alpha $ is a definable relation between elements of A and of the set of natural numbers $\mathbb {N}$ such that $\mathbf {T}\vdash \forall x\in A\, \exists y\in \mathbb {N} \ \alpha (x,y)$ . Arrows between assemblies $(A,\alpha )$ and $(B,\beta )$ are equivalence classes of functional relations F from A to B such that

$$ \begin{align*}\mathbf{T}\vdash \exists e\in \mathbb{N}\,\forall x\in A\,\forall y\in B\,\forall z\in \mathbb{N}\,(\alpha(x,z)\wedge F(x,y)\rightarrow \beta(y,\{e\}(z))).\end{align*} $$

The assemblies category is denoted by $\mathcal {Asm}_{\mathcal {E}[\mathbf {T}]}$ in [Reference van den Berg and Moerdijk5].

Now, consider our category $\boldsymbol {\mathcal {C}}_r$ of realized collections in Section 3.1 formalized in $ \mathbf {T}$ . Every object $\{x|\,\varphi (x)\}$ (for which $\mathbf {T}\vdash \forall x\,( \varphi (x)\rightarrow x\in \mathbb {N})$ always holds) can be mapped to the assembly $\mathbf {i}(\{x|\,\varphi (x)\}):=(\{x|\varphi (x)\},=_\varphi )$ where

$$ \begin{align*}x=_\varphi y\equiv^{def} x=y.\end{align*} $$

Arrows $[\mathbf {n}]_\approx $ in $\boldsymbol {\mathcal {C}}_{r}$ can be sent to the functional relations representing their graph, thus defining a functor $\mathbf {i}$ from $\boldsymbol {\mathcal {C}}_r$ to $\mathcal {Asm}_{\mathcal {E}[\mathbf {T}]}$ . Since the numerical existence property holds for $\mathbf {T}$ , the functor $\mathbf {i}$ is full and faithful, thus $\boldsymbol {\mathcal {C}}_r$ can be identified as a full subcategory of $\mathcal {Asm}_{\mathcal {E}[\mathbf {T}]}$ .

Now, let us call recursive objects those assemblies where A is a subclass of natural numbers satisfying

$$ \begin{align*}\mathbf{T}\vdash \forall x\in A\,\forall y\in \mathbb{N}\,(\alpha(x,y)\leftrightarrow x=y).\end{align*} $$

Let $\mathcal {Rec}_{\mathcal {E}[\mathbf {T}]}$ denote the full subcategory of assemblies with recursive objects. Then, $\boldsymbol {\mathcal {C}}_r$ can be seen as a full subcategory of $\mathcal {Rec}_{\mathcal {E}[\mathbf {T}]}$ :

Moreover, recalling that the ex/lex completion of the category of recursive objects turns out to be that of discrete objects in [Reference Hyland, Robinson and Rosolini19, Reference van Oosten43], we denote the ex/lex completion of $\mathcal {Rec}_{\mathcal {E}[\mathbf {T}]}$ by $\mathcal {Disc}_{\mathcal {E}[\mathbf {T}]}$ . Since $\boldsymbol {\mathcal {C}}_r$ is a full subcategory of recursive objects and $\textbf {pEff}$ is the ex/lex completion of $\boldsymbol {\mathcal {C}}_r$ we have an embedding of $\textbf {pEff}$ in $\mathcal {Disc}_{\mathcal {E}[\mathbf {T}]}$ that extends to fibers, trivially.

Additionally, recalling that $\mathcal {Disc}_{\mathcal {E}[\mathbf {T}]}$ is the ex/reg completion of the category of modest sets (see [Reference Rosolini47]), that is, the category of assemblies which satisfy

$$ \begin{align*}\mathbf{T}\vdash \forall x,y\in A\, \forall z\in \mathbb{N}\, (\alpha(x,z)\wedge \alpha(y,z)\rightarrow x=y)\end{align*} $$

and denoting by $\mathcal {Mod}_{\mathcal {E}[\mathbf {T}]}$ such a category within $\mathcal {Eff}_{\mathcal {E}[\mathbf {T}]}$ , we obtain the following result.

Proposition 11.1. Let $\mathbf {pEff}$ be the predicative effective topos built on an extension $\mathbf {T}$ of $\mathbf {CZF}$ having the numerical existence property; and let $\mathbf {pEff}_{sm.\Delta }$ be the full subcategory of $\mathbf {pEff}$ given by objects $(\textsf {A},[\textsf {R}])$ where $[\textsf {R}]\in \overline {{\mathbf {Prop}^r_{\mathbf {s}}}}(\textsf {A} \times \textsf {A})$ . Then, $\mathbf {pEff}_{sm.\Delta }$ is a full subcategory of the predicative realizability category $\mathcal {Eff}_{\mathcal {E}[\mathbf {T}]}$ defined as in [Reference van den Berg and Moerdijk5] from the syntactic category $\mathcal {E}[\mathbf {T}]$ of definable classes of $\mathbf {T}$ endowed with the family $\mathcal {S}[\mathbf {T}]$ cof arrows whose fibers are sets in $\mathbf {T}$ .

Proof. The category $\mathcal {Eff}_{\mathcal {E}[\mathbf {T}]}$ proposed in [Reference van den Berg and Moerdijk5] as a predicative version of Hyland’s Effective Topos ${\mathbf {Eff} }$ is the full subcategory of the ex/reg completion of $\mathcal {Asm}_{\mathcal {E}[\mathbf {T}]}$ , whose objects are separated in the sense of [Reference van den Berg and Moerdijk4, p. 141]. The statement follows observing that objects $(\textsf {A},[\textsf {R}])$ of $\textbf {pEff}_{sm.\Delta }$ , seen as objects in $(\mathcal {Asm}_{\mathcal {E[\mathbf {T}]}})_{ex/reg}$ , are separated in the above sense since $[\textsf {R}]\in \overline {{\mathbf {Prop}^r_{\mathbf {s}}}}(\textsf {A}\times \textsf {A})$ .

Note that, when we take $\mathbf {T}$ to be $\mathbf {ZFC}$ , although it does not satisfy the numerical existence property, we can still define a functor from $\textbf {pEff}$ to a version ${\mathbf {Eff} }_{def}$ of Hyland’s Effective Topos, constructed as the ex/reg completion of the full subcategory of $\mathcal {Asm}_{\mathcal {E}[\mathbf {ZFC}]}$ consisting of assemblies whose underlying classes are definable sets. Indeed, in $\mathbf {ZFC}$ all definable subclasses of $\mathbb {N}$ are in fact sets. In the same framework, one can see that this ${\mathbf {Eff} }_{def}$ is a full subcategory of $\mathcal {Eff}_{\mathcal {E}[\mathbf {ZFC}]}$ .

A comparison between $\textbf {pEff}$ formalized in ${\widehat {ID_1}}$ , and the usual Hyland’s Effective Topos ${\mathbf {Eff} }$ , viewed as an internal large category within ZFC, is induced by the standard interpretation of ${\widehat {ID_1}}$ in the ZFC set theory, as shown in [Reference Maietti and Maschio27].

All these observations concern only the base category $\textbf {pEff}$ . A comparison between their fibered structures is left to future work. Just observe that, while maps in van den Berg and Moerdijk’s approach are built on the notion of set in axiomatic set theory, in our approach the fibration of sets is defined mimicking the structure of sets within the language of dependent type theory, as that used in both levels of the Minimalist Foundation [Reference Maietti25].

Furthermore, we note a possible connection with [Reference van den Berg3, Reference Frey15], where the Effective Topos is characterised as the homotopy category of a suitable category. Since $\textbf {pEff}$ admits an equivalent presentation as an exact completion, which can itself be obtained as a homotopy category [Reference van den Berg and Moerdijk6], it is natural to consider, as future research, the application of similar techniques in our setting.

Nevertheless, our comparisons are sufficient to conclude that the full subcategory of discrete objects within Hyland’s Effective Topos, as well as within van den Berg and Moerdijk’s constructive setting, already contains a predicative version of $\mathbf {Eff}$ . In short, this confirms the claim made on p. 1140 of [Reference van Oosten43]: the discrete objects of $\mathbf {Eff}$ can be considered the realm of constructive predicative mathematics.