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.


  • 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

  • 1
    $\begingroup$ Please can you include paper titles (and ideally also links) rather than just author names and years when referencing papers? $\endgroup$
    – varkor
    Commented Jan 24, 2022 at 12:44
  • 1
    $\begingroup$ @varkor I have added more precise references to the question. $\endgroup$ Commented Jan 24, 2022 at 12:50

2 Answers 2

  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$.

  • $\begingroup$ Hi Neel! Indeed, I was trying to sketch this argument since our discussion but got a bit turned around. Some of this is linguistic (categorical universes aren't exactly like sets internally, so they don't automatically have subset relation assigned to them and the obvious choice of requiring a monic el(A) >-> el(B) is sensible, but doesn't make them a partial order, merely a pre-order, etc). Some of my confusion was a bit more foundational though... $\endgroup$ Commented Jan 24, 2022 at 15:21
  • $\begingroup$ [sorry, character limit]... because the literature seems to claim that IR is equivalent to a very large large cardinal axiom (a Mahlo cardinal), but having a universe in a topos is "just" equivalent to a strongly inaccessible cardinal! Is the difference being made up for in the subobject classifier and does this in turn mean that IR is actually quite weak in classical ZFC, for instance? $\endgroup$ Commented Jan 24, 2022 at 15:21
  • 1
    $\begingroup$ Let me try and drag this out further. Let's say I have a universe in a topos which is big enough to classify the subobject classifier. This is true in $\mathbf{Set}$ if I have just one Grothendieck universe. I then can use IR to build a hierarchy of universes, each containing the subobject classifier. But now I seem to have gone from 1 universe + universe of propositions to a hierarchy + a universe of propositions which shouldn't be possible, should it? $\endgroup$ Commented Jan 24, 2022 at 15:31
  • $\begingroup$ Are IR systems actually a domain? Domains need to have joins of all directed sets, but maybe size limitations on the sort of unions a universe is closed under cause it to not quite be a domain? Something along those lines seem like a point where the proof might subtly fail. $\endgroup$
    – Dan Doel
    Commented Jan 24, 2022 at 17:38
  • 1
    $\begingroup$ Hi Neel, I am nearly certain that there must be some mistake somewhere. ZFC+U is consistent with "there does not exist a mahlo cardinal", so if this argument sufficed to show exhibit initial algebras for all IR functors, it would also prove that ZFC is inconsistent with one Grothendieck universe. $\endgroup$ Commented Jan 24, 2022 at 18:11

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.

  • $\begingroup$ Hello, this does indeed address some but not all of my confusion, since one can seemingly ask for 2 inaccessible cardinals such that $V \in U$ forms an internal universe. If we have IR for types which are $U$-small through Neel's construction, we can then kick off the universe hierarchy with $V$ and obtain a sequence of universes again. It seems like we must require some additional properties of $U$ for this to be sensible, right? $\endgroup$ Commented Jan 25, 2022 at 13:34
  • $\begingroup$ Also, I forgot to write this in my first comment: thank you for the response and references :) $\endgroup$ Commented Jan 25, 2022 at 13:40
  • $\begingroup$ This is very interesting, but I do not think it addresses the question at hand. I think a good first step would be for someone to explain why they believe that IR codes in the sense of Dybjer and Setzer are the same things as monotone maps in the domain of IR systems. Once that is explained, I think we will be able to narrow down an answer to this question. $\endgroup$ Commented Jan 25, 2022 at 14:19
  • $\begingroup$ I'm also not exactly clear on what sort of I-R definitions are being modeled. Does the domain construction only model "small" I-R, which is no stronger than more plain inductive types? I admittedly usually forget to think about that, because the "large" version is what people are wondering about. The "IR systems" naively look like the "large" version (to me), though. And one of the reasons for inventing the "large" version is that the MLTT universe is just another special case, and a theory can't have such I-R definitions and not have a universe. It can only lack an internal Mahlo universe. $\endgroup$
    – Dan Doel
    Commented Jan 25, 2022 at 16:47
  • 1
    $\begingroup$ I think you should say a little more --- there seems to be a pretty big distance between this setting where you have access to the material subset relation and monotone functions, and the logic of a topos where there is no subset relation between arbitrary objects. So while I grant that it may be possible to turn what you and Neel are suggesting into a topos-valid proof, it is currently not type-checking for me. $\endgroup$ Commented Jan 26, 2022 at 10:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.