Induction-recursion in models other than $\mathbf{Set}$

Question

It is well-known that various flavors of induction-recursion are consistent*. Typically, this is proven by showing that the standard model of type theory in sets can be extended to include induction-recursion. I'm interested in what is known about modeling induction-recursion in settings other than $\mathbf{Set}$.

To be more concrete: is it known whether every Grothendieck topos models induction-recursion? I'm perfectly happy to ignore questions of strictness in these models, so that this can be rephrased as asking whether the strictly positive functors one uses to model IR admit initial algebras in all Grothendieck topoi.

If it helps to clarify this question: in recent work Fiore, Pitts, and Steenkamp 2021 have shown that it is possible to construct QWI types in a wide class of models, including all Grothendieck topoi. I'm hoping for a similar result applied to some form of induction-recursion.

In my (cursory) literature survey, it appears that this question is nearly addressed by Ghani, Malatesta, Nordval Forsberg, and Setzer 2013. They provide a model of their "fibred data types" (which subsume IR) in a split fibration satisfying several conditions regarding presentable objects. They do not, however, make any comment on whether these assumptions are satisfied in a category other than $\mathbf{Set}$, and their assumption of working only with the morphisms defining a splitting makes it difficult to compute whether their assumptions are validated for the (splitting, I suppose) of a the codomain fibration of a Grothendieck topos. It also appears that this question is settled for small induction-recursion, which Malatesta, Altenkirch, Ghani, Hancock, and McBride 2013 seem to have reduced to indexed inductive types, which can be modeled in a Grothendieck topos.

(*) Assuming a suitable large cardinal axiom I'm accepting without comment for the remainder of this question.

Bibliography:

• N. Ghani, L. Malatesta, F. N. Forsberg and A. Setzer, "Fibred Data Types," 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013, pp. 243-252, https://doi.org/10.1109/LICS.2013.30.

• Hancock, P., McBride, C., Ghani, N., Malatesta, L., & Altenkirch, T. (2013). Small induction recursion. Typed Lambda Calculus and Applications: 11th International Conference. https://doi.org/10.1007/978-3-642-38946-7_13

• Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp. Quotients, inductive types, and quotient inductive types. Available on arxiv https://arxiv.org/abs/2101.02994

Answer 1

1. Define an IR system be a family $U \in \mathrm{Set}$ and a function $\phi \in U \to \mathrm{Set}$.

   IR systems form a domain. The least element is $\bot = (\emptyset, !)$. The order relationship $(U, \phi) \leq (U', \phi')$ holds when $U \subseteq U'$, and for all $c \in U$, we have $\phi(c) = \phi'(c)$. (Limits are computed in the obvious way, by union.)

2. Pataraia's Theorem: Suppose $D$ is a domain, and $f : D \to D$ is a monotone function on $D$. Then $f$ has a least fixed point.

So for any monotone function on IR systems (i.e., basically any sensible inductive-recursive definition), it has a least fixed point.

Pataraia's theorem is provable in the internal language of any topos, since it is a proof in intuitionistic bounded ZF. (I reproduce the proof below.)

However, the definition of IR system uses a function $\phi : U \to \mathrm{Set}$, so we need a well-behaved universe of small sets to interpret this.

In his 2004 paper, Universes in Toposes, Thomas Streicher says that not all topoi have such a universe (in particular, the free topos doesn't). but he says that Set, realisability models, and Grothendieck topoi all have universes. (Fair warning: I've read this paper, but haven't tried to reproduce his proofs!)

---

Proof of Pataraia's theorem

Define an $f$-inflationary set to be be a set $U \subseteq D$ which contains $\bot$, is closed under $f$ (i.e., if $x \in U$, then $f(x) \in S$), and contains joins of directed sets in $U$.

Let $S$ be the intersection of all $f$-inflationary sets (i.e, the least $f$-inflationary set). Now, note that:

1. $S$ itself a domain, since $\bot \in S$, and it contains directed joins by definition.
2. The restriction $f : S \to S$ is inflationary (i.e., for all $x \in S$, $x \leq f(x)$).

Next, let $E(S)$ to be the set of inflationary, monotone maps $S \to S$.

Now, $E(S)$ is a domain. Its least element is the identity function $\mathit{id}_S$, and the order and joins are computed pointwise.

$E(S)$ is also a directed set itself. Suppose you have $f$ and $g$ in $E(S)$. Then, it is clear that $f \circ g \in E(S)$, and because both $f$ and $g$ are increasing, $f \leq f \circ g$ and $g \leq f \circ g$.

Hence, the lub (call it $m$) of $E(C)$ is itself an element of $E(C)$. So $m$ is itself an inflationary, monotone map. Since $f$ is an element of $E(C)$, we know that $f \circ m \in E(C)$, and so $f \circ m \leq m$. Since $f$ is inflationary, we also have that $m \leq f\circ m$.

So for every element $s \in S$, we have $f(m(s)) = m(s)$.

So $m(\bot)$ is the least fixed point of $f$.

Answer 2

This is mostly a reaction to the questions posed in the comments to Neel's answer.

Partial maps $A \rightharpoonup B$ between sets $A$ and $B$ form a domain, where we view such maps as single-valued relations. Given a transitive universe of sets $U$ (which is a set) and any $I \in U$, we have $I \subseteq U$. Therefore, maps $I \to U$ where $I \in U$ are just partial maps $U \rightharpoonup U$, so they form a domain.

If we want to use a domain-theoretic argument to establish that a semantic model has inductive-recursive (IR) types, as sketched by Neel, then the model has to contain a universe that plays the role of $U$ above. But the type theory being modeled need not have a universe. I believe this is where some of the confusion might be coming from.

A type theory with inductive-recursive types but without a universe carries a lot less punch than one with an additional universe. For instance, consider MLTT (something like $\Pi$, $\Sigma$, $\mathrm{Id}$, $0$, $1$, $+$, $\mathbb{N}$). It is modeled by $V_\kappa$ where $\kappa$ is strongly inaccessible. If we take $\kappa$ to be the least strongly inaccessible cardinal, then $V_\kappa$ contains no inaccessibles, so no MLTT universes. By the above arguments such $V_\kappa$ still models inductive-recursive types. The conclusion is that IR types alone do not beget a universe.

But now consider MLTT with a universe $U_0$ and IR types. The IR types allow us to define an inductively generated type of codes (a universe) and a decoding function from codes to types, closed under any operations that are already known to exist, and in particular $\Pi$ and $\Sigma$.

So we can construct a universe $U_1$ which contains $U_0$ (all universes in this discussion are also closed under $\mathbb{N}$, $\Sigma$ and $\Pi$). And then we can construct $U_2$ which contains $U_1$, and so on.

More generally, given any type $A$, we may construct a universe $\mathsf{Univ}(A)$ which contains $A$. Then we may define a family $n : \mathbb{N} \vdash U(n) \; \mathsf{type}$ by $U_{n+1} = \mathsf{Univ}(U_n)$. So we have a hierarchy of universes, indexed internally by $\mathbb{N}$.

But that's nothing. With a slight improvement, we may construct a universe $\mathsf{Univ}(I, A)$ which contains any type family $i : I \vdash A(i) \, \mathsf{type}$. This allows us to generate a universe above any sequence of universes, so we have uncountably many universes.

But that is nothing. We may construct a universe $\mathcal{U}$ which is closed under $\mathsf{Univ}$, i.e., given any $A : I \to \mathcal{U}$, there will be a universe $\mathsf{Univ}(I, A)$ in $\mathcal{U}$ which exceeds $A$. So not only does $\mathcal{U}$ contain very many universes, they are also unbounded.

I recommend reading Eric Palmgren's On universes in type theory and Anton Setzer's Extending Martin-Löf Type Theory by one Mahlo-universe.